RFC: GuessLex omit source pos from error message

[Seasawher]

RFC: GuessLex omit source pos from error message

[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.