Tactic combinator showing all errors

Stream: mathlib4

[Patrick Massot]

If you do

import Mathlib.Tactic

example (x y : Nat): x = y := by
  first | rfl | aesop

then the error message you get comes from aesop. If you do

example (x y : Nat): x = y := by
  first | aesop | rfl

then you get the error message coming from rfl. Do we have a combinator that would show both error messages (with a clear indication that it is a list of error messages coming from trying various things, not a single error message)?

[Jireh Loreaux]

Could you just copy the first combinator with logError instead of throwError?

[Jireh Loreaux]

Ah, nevermind, you need it to accumulate the errors but only throw the list of them if the last tactic doesn't succeed.

[Kyle Miller]

Here's a possibility:

section
open Lean Elab Tactic
variable {α : Type}

def orElse' (xref : Syntax) (x : TacticM α) (y : Unit → TacticM α) : TacticM α := do
  try withoutRecover x catch e =>
    try y () catch e' =>
      if (← read).recover then
        logErrorAt xref e.toMessageData
      throw e'

partial def firstLoop (tacs : Array Syntax) (i : Nat) :=
  if i == tacs.size - 1 then
    evalTactic (tacs[i]!)[1]
  else
    let tac := (tacs[i]!)[1]
    orElse' tac (evalTactic tac) (fun _ => firstLoop tacs (i+1))

elab "first' " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic => do
  let stx ← getRef
  let tacs := stx[1].getArgs
  if tacs.isEmpty then throwUnsupportedSyntax
  firstLoop tacs 0

end

example (x y : Nat): x = y := by
  first' | rfl | aesop

[Kyle Miller]

image.png

[Kyle Miller]

I could see first working like this in general.

[Kyle Miller]

Same with <|>

[Yaël Dillies]

Yes please! I've been wanting this

[Eric Wieser]

Is there a reason that something like docs#List.anyM doesn't work in place of your firstLoop?

[Kyle Miller]

I didn't think about it much — I copied the code from the implementation of first

[Kyle Miller]

Do you have any idea how to eliminate xref from orElse'? That would help with making it possible to be the main implementation of <|>

[Kyle Miller]

Without xref, the error for x becomes reported as an error for all of <|>

[Jireh Loreaux]

I didn't see a way around the xref either, and my implementation was similar.

[Joachim Breitner]

What happens if this first is hidden in some other tactic, like decreasing_tactic? I assume the error messages will just all be shown, but without much context? In that case it might be nicer to be a bit verbose and say “Tactic rlf failed with: … Tactic simp failed with: …”? Not sure if it's a problem to pretty print the actual tactic here, I guess it could be too large?

[Yaël Dillies]

Surely the decreasing_tactic should have its own error message anyway, right?

[Joachim Breitner]

Yeah, but it essentially says “none of the tactics solved it” also swallowing the error messages.

Although that's actually using macro_rules not first to try various tactics. But same problem: you don't get to see the error messages from all but one of them. (Not sure if you really should see all of them in this case.)

[Eric Wieser]

Kyle Miller said:

Do you have any idea how to eliminate xref from orElse'? That would help with making it possible to be the main implementation of <|>

Can't you use e.getRef instead of xref?

[Thomas Murrills]

There's also simply logException e (which essentially just wraps logErrorAt e.getRef e.toMessageData in the non-internal-error case)

[Eric Wieser]

I couldn't get firstM to work without making a primed version:

import Lean

section
open Lean Elab Tactic
variable {α : Type}

instance betterOrElse : OrElse (TacticM α) where orElse x y := do
  try withoutRecover x catch e =>
    try y () catch e' =>
      if (← read).recover then
        logException e
      throw e'

instance (priority := high) betterAlternative : Alternative TacticM where
  orElse x y := (betterOrElse.orElse x y)
  failure := failure

/-- Like `firstM`, but without using `f a <|> failure` on `[a]`. -/
@[specialize]
def List.firstM'.{u,v,w} {m : Type u → Type v} [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
  | []    => failure
  | [a] => f a
  | a::as => f a <|> firstM' f as

elab "first' " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic => do
  let stx ← getRef
  let tacs := stx[1].getArgs
  if tacs.isEmpty then throwUnsupportedSyntax
  discard <| List.firstM' (fun stx => evalTactic stx[1]) tacs.toList
  pure ()

end

example (x y : Nat): x = y := by
  first' | rfl | rfl

[Eric Wieser]

Hmm, this doesn't work with more than two rfls

[Thomas Murrills]

On closer inspection, the original doesn't either, I think—the issue is that we throw e', which gets caught (when appearing inside y ()) and reverts our logErrorAt. This is unless we happen to have thrown e' to the top level, in which case we get both the first error and the last error.

[Kyle Miller]

Joachim Breitner said:

What happens if this first is hidden in some other tactic, like decreasing_tactic?

I think there needs to be some protocol for knowing when tactics are "interactive". There's already some of that protocol in the form of the recover flag, but it doesn't seem to be capturing interactivity — it seems to be an orthogonal concept.

"Interactive" mode might include

• having tactics generate time-consuming diagnostic messages on failure and
• logging errors even if they're being caught (like in the <|> and first modifications)

Then tactics that run tactic scripts could go into non-interactive mode to prevent logging incidental errors.

[Patrick Massot]

Thanks Kyle! I should have been more specific and say that I’m not actually using first, I have a single user-facing tactic that tries several things. But at least I know there is nothing already existing, and I will probably be able to reuse some of your code. And I think that first' could be useful anyway.

[Kyle Miller]

No problem — you happened to ask a question in the realm of something I had been thinking about anyway: what sort of protocol do we need or want for tactics in "interactive" mode?

first is a good example of the phenomenon. Even though you wouldn't see first in a completed proof like this, it would be helpful to see these messages to help you come up with your completed proof.

[Damiano Testa]

By the way, even though you do not see the errors, with the "unused tactic linter", you can do this:

example (x y : Nat): x = y := by
  first | rfl | aesop | sorry  -- <--  add a sorry, so you know that the goal will be closed

-- and the unused tactic linter reports:
/-
  'rfl' tactic does nothing [linter.unusedTactic]
  'aesop' tactic does nothing [linter.unusedTactic]
-/

[Thomas Murrills]

One of the things that could fix this particular issue would be a "compound error": if we could throw multiple errors at once in a single throw, we wouldn't have to manage the state carefully.

Likewise, it would be nice if there were a variant of catch which could catch (and bind) any generated messages—the gap between a control-flow-affecting Exception and a logged error can sometimes feel uncomfortably large.

(Of course, an interactive mode would still be very useful in general—this isn't any argument against that. :) )

[Thomas Murrills]

Though, the arguments of .error technically have enough structure for us to hack together "compound errors" anyway! So, just for fun, here's an extremely cursed thing you can do. :)

import Lean

section
open Lean Elab Tactic
variable {α : Type}

/-- Abuse `.compose` constructor to get a `MessageData` tree.
Propagate "All failures:" header to the top left; insert newlines between messages. -/
def composeMessages : MessageData → MessageData → MessageData
  | .compose (.tagged `comp _) c₁, .compose (.tagged `comp _) c₂
  | .compose (.tagged `comp _) c₁, c₂
  | c₁, .compose (.tagged `comp _) c₂
  | c₁, c₂ => .compose (.tagged `comp m!"All failures:\n") (.compose (.compose c₁ m!"\n\n") c₂)

protected def _root_.Lean.Exception.append : Exception → Exception → Exception
| .error ref msg, .error ref' msg' =>
  .error
    /- Use the source info from the rightmost node. This is a hack to get
    a red squiggle on each individual tactic instead of under the whole span. -/
    (Syntax.node (SourceInfo.fromRef ref') `compoundError #[ref, ref'])
    (composeMessages msg msg')
| _, _ => panic! "internal errors not yet implemented"

/-- Log each error in a compound error individually, in order. -/
partial def logComposedException {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m]
    [MonadOptions m] [MonadLiftT IO m] : Exception → m Unit
  | .error (Syntax.node _ `compoundError #[ref₁, ref₂])
    (.compose (.tagged `comp _) (.compose (.compose msg₁ _) msg₂))
  | .error (Syntax.node _ `compoundError #[ref₁, ref₂])
    (.compose (.compose msg₁ _) msg₂) => do
    logComposedException (.error ref₁ msg₁)
    logComposedException (.error ref₂ msg₂)
  | e => logException e

def orElse' (x : TacticM α) (y : Unit → TacticM α) : TacticM α := do
  try withoutRecover x catch e =>
    try y () catch e' =>
      let mut e' := e'
      if (← read).recover then
        e' := e.append e'
      logComposedException e'
      throw e'

partial def firstLoop (tacs : Array Syntax) (i : Nat) :=
  if i == tacs.size - 1 then
    evalTactic (tacs[i]!)[1]
  else
    let tac := (tacs[i]!)[1]
    orElse' (evalTactic tac) (fun _ => firstLoop tacs (i+1))

elab "first' " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic => do
  let stx ← getRef
  let tacs := stx[1].getArgs
  if tacs.isEmpty then throwUnsupportedSyntax
  firstLoop tacs 0

end

example (x y : Nat) : x = y := by
  first' | rfl | rfl | rfl

[Thomas Murrills]

The biggest "cheat" here is that we log all three errors, but the error we throw also renders as "All failures: ...", appears as a squiggle only on the last token, and lists all errors. For example, if we used first | simp | dsimp | simp, the errors would look like:

Foo.lean:223:11
simp made no progress

Foo.lean:223:18
dsimp made no progress

Foo.lean:223:26
simp made no progress

Foo.lean:223:26
All failures:

simp made no progress
dsimp made no progress
simp made no progress