tactic to fail with error message

Stream: lean4

[Heather Macbeth]

I'd like to change the error message of a finishing tactic (for use in a macro which wraps that tactic). Is there a more idiomatic way to do it than (try ...) <;> fail "my error message"?

syntax "foo" : tactic

macro_rules | `(tactic| foo) => `(tactic| (try exact rfl) <;> fail "zz")

[Kyle Miller]

You can also do

syntax "foo" : tactic

macro_rules | `(tactic| foo) => `(tactic| fail "zz")
macro_rules | `(tactic| foo) => `(tactic| exact rfl)

Tactic macros do backtracking, and they are tried in reverse-definition order

[Kyle Miller]

If you want it as a single rule, then better than (try ...) <;> ... is first | exact rfl | fail "zz" (like this example)

[Heather Macbeth]

Those are two very nice solutions. Thanks!

[Damiano Testa]

Kyle, maybe I am misunderstanding your suggestion, but with macro_rules it seems that if all available choices fail, then the last-defined one is used:

syntax "foo" : tactic

macro_rules | `(tactic| foo) => `(tactic| fail "zz")
macro_rules | `(tactic| foo) => `(tactic| exact rfl)

example : False := by
  foo
/-
type mismatch
  rfl
has type
  ?m.3525 = ?m.3525 : Prop
but is expected to have type
  False : Prop
-/

You get zz if instead you do

syntax "foo" : tactic

macro_rules | `(tactic| foo) => `(tactic| exact rfl)
macro_rules | `(tactic| foo) => `(tactic| fail "zz")

example : False := by
  foo  -- zz

[Kyle Miller]

@Damiano Testa I'll admit I might have it backwards!

[Damiano Testa]

No, I think that what you said was correct, when one of the tactics succeeds: in this case, Lean chooses the top-mostlast successful tactic. If they all fail, then again Lean applies the top-mostlast tactic, and that is the error that you see.

[Damiano Testa]

So, if you want to replace the error message, you should make the error message that you want to display be the last-defined behaviour of the tactic.

[Kyle Miller]

If you want it to also be extensible, then something I've seen (like for the GetElem index bounds tactic) is a two-level system, where macro 1 has two expansions, macro 2 and an error message, and then macro 2 is the main implementation. That way you can create rules for macro 2 without changing that the error message is last for macro 1

[Damiano Testa]

Ah, nice!

Until now, I hadn't realized that if one of the steps of your macro is an error message, then all previously defined error messages will never display.