RFC: GuessLex omit source pos from error message

[Seasawher]

Proposal

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

Community Feedback

see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/omit.20line.20number.20from.20message/near/445973308

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[nomeata]

I am unsure. If a user is faced with this error message they might really need this help to identify the respective calls, and so far I did not think of a better way. Do you?

I assume it bother you in the context of tests? Happy to accept a PR that adds an option to omit them, similar to pp.mvars, that people writing tests with these can turn on.

[Seasawher]

I assume it bother you in the context of tests?

Yes. When writing code to test output messages, the test code must be modified frequently each time the file is changed.

[nomeata]

Got it. What is your use case for testing failing function definitions? The lean test suite itself, or some other project?

You could also test it indirectly: use guard_msgs to hide the error text, and then afterwards check that the function is not fully constructed (e.g. no .eq_def lemma)

[Seasawher]

I'm writing Lean reference book (https://lean-ja.github.io/lean-by-example/, Japanese) and I use #guard_msgs to show examples including errors without actual error.

[Seasawher]

You could also test it indirectly: use guard_msgs to hide the error text, and then afterwards check that the function is not fully constructed (e.g. no .eq_def lemma)

oh nice! it is interesting

#guard_msgs (drop all) in
def alternate {α : Type} (xs ys : List α) : List α :=
  match xs, ys with
  | [], ys => ys
  | x :: xs, ys => x :: alternate ys xs

/-
alternate [1, 2] [3, 4]
-/
#reduce alternate [1, 2] [3, 4]

[nomeata]

I'm writing Lean reference book (https://lean-ja.github.io/lean-by-example/, Japanese) and I use #guard_msgs to show examples including errors without actual error.

That's great work, thanks! But hopefully you understand that this is a special case and shouldn't guide the error message phrasing.

Are you unblocked by the drop all trick? Can we close this then?

[Seasawher]

Are you unblocked by the drop all trick?

No. I would be happy to be able to display the error message itself, so I would still be happy if there was a way to remove the specific line number from the error message.

[Seasawher]

But hopefully you understand that this is a special case and shouldn't guide the error message phrasing.

Ok this is reasonable. You can close this as not planned.
I may be able to achieve what I want to do in the future by using verso or some other method.

[david-christiansen]

This is plausible - in Verso, it would be fairly easy to write a program that checked Lean messages for equality modulo substrings that look like source positions and/or metavariable names, so the error in the book matches what users will see but it doesn't need updating quite so often.