custom messages for tactic failure

Stream: new members

[Simon Daniel]

i was wondering, if in cases a tactic cannot close a proof like for example

def test : "a" == "b" := by decide

if you could supply a custom String for error output instead of "failed to reduce to 'true'" that might be more helpful to a user (like"a" is not equal to "b")

[Kevin Buzzard]

You could write your own tactic which did this, sure. You're unlikely to convince the core Lean developers to change the error messages.

[Eric Wieser]

Probably the tactic should print the context like rfl does

[Eric Wieser]

def test : "a" == "b" := by rfl

gives

tactic 'rfl' failed, equality lhs
  "a" == "b"
is not definitionally equal to rhs
  true
⊢ ("a" == "b") = true

[Eric Wieser]

I think that last line should probably appear after the decide error message too

[Patrick Massot]

Kevin Buzzard said:

You're unlikely to convince the core Lean developers to change the error messages.

I’m not sure. Improving error messages is the first item of the Lean FRO roadmap for its first year. What is unlikely is to convince them to spend a lot of time reviewing bad pull-requests about this.

[Kyle Miller]

Thanks for pointing out the message could be improved! I went and made a PR to try to address this: lean4#3422

[Kyle Miller]

With this change, the error message would look like

example : "a" == "b" := by decide
/-
tactic 'decide' proved that the proposition
  ("a" == "b") = true
is false
-/

[Eric Wieser]

I was under the impression that there was some central mechanism for printing the ⊢ part of the error message; if that's not the case, does every tactic have to remember to print its goal state now?

[Simon Daniel]

my original intent of this post was to supply a custom error message as a String to the tactic, not a general problem with the decide tactic error message itself.
where is the String

/-
tactic 'decide' proved that the proposition
  ("a" == "b") = true
is false
-/

being set?
@Kyle Miller that seems like an nice improvement to me!

[Kyle Miller]

It's an error that decide generates (in the PR, look for the throwError lines).

[Kyle Miller]

@Eric Wieser I think the central mechanism is that you put your cursor right before the tactic. In this case, I decided to insert the proposition since it helps with legibility of the error message.

[Kyle Miller]

@Simon Daniel You might be interested in the LSpec link in the PR comment. There's a separate version of Decidable in LSpec (Testable) that's for synthesizing a reason if possible, falling back on Decidable if not. You could make a version of decide that synthesizes a Testable instance on failure to try to come up with a reason for the user.

[Kyle Miller]

For your example in this thread, this is the instance that would apply: https://github.com/lurk-lab/LSpec/blob/1d3536f96e964bd57405f18c41c2adbaf4f257e0/LSpec/Instances.lean#L15

[Eric Wieser]

It would be nice if there were some UI mechanism to distinguish "this tactic failed" from "this tactic concluded your goal is unprovable

[Kyle Miller]

Yeah, though here I'd say the failure is inconclusive, since there might be a False hypothesis in the local context that decide isn't looking at.

[Yaël Dillies]

Kyle Miller said:

Eric Wieser I think the central mechanism is that you put your cursor right before the tactic. In this case, I decided to insert the proposition since it helps with legibility of the error message.

I see a big flaw in this argument: it doesn't work when the tactic runs on multiple goals, and this is the use case where I read the error messages most closely.

[Eric Wieser]

Does it not? Aren't all the goals shown?