omit line number from message

Stream: Is there code for X?

[Asei Inoue]

The following output message contains a line number in editor 26:24-39 ? ?. But this is quite fragile to change, so I want to remove the line numbering part.

/--
error: fail to show termination for
  alternate
with errors
argument #2 was not used for structural recursion
  failed to eliminate recursive application
    alternate ys xs

argument #3 was not used for structural recursion
  failed to eliminate recursive application
    alternate ys xs

structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            xs ys
1) 26:24-39  ?  ?
Please use `termination_by` to specify a decreasing measure.
-/
#guard_msgs (whitespace := lax) in
def alternate {α : Type} (xs ys : List α) : List α :=
  match xs, ys with
  | [], ys => ys
  | x :: xs, ys => x :: alternate ys xs

[Kim Morrison]

I think this is probably best achieved by an option that the termination solver looks at before deciding how to print the results. You'd need to open an issue.

[Kim Morrison]

#guard_msgs by itself doesn't have this sort of capability.

[Asei Inoue]

done! see: https://github.com/leanprover/lean4/issues/4519

[Eric Wieser]

I guess another direction you could go is having a richer message format that includes .posOf (s : Syntax) (which renders as 26:24-39 usually, is clickable, and can be filtered by guard_msgs), but then you also need some .table format to reflow the table columns