Catching all tactic errors

Stream: Is there code for X?

[Joachim Breitner]

I have a tactic expression (Syntax) and a goal (MVarId). I want to find out if the tactic solves the goal, in an isolated manner – I don’t care about the resulting proof or error messages, I just need a Bool.

I thought I could just use Term.runTactic and catch exceptions, but that doesn’t quite work: There are tactics, in particular { … } or the center dot, that will themselves recover from errors, log an Error (but not throw one) and admit the goal.

What is the most robust way to still fail them. I tried

              if ← MonadLog.hasErrors then
                throwError "Tactic execution had errors"

but the message log is rather global (CoreM), and it seems to be a heavy hammer to try to recognize if the tactic added any new errors to the log etc.

Looking for sorry in the expression isn’t great either, because if the user really writes sorry, then that should work.

So I think I'd like to locally say logError is throwError.

[Kyle Miller]

Tactics are supposed to recover or not depending on the current recover state. You can turn off recovery with docs#Lean.Elab.Tactic.withoutRecover

[Joachim Breitner]

Ah, now I see it. Great!

[Kyle Miller]

There's also docs#Lean.Elab.Term.withoutErrToSorry to turn off elaboration errors creating sorries

[Joachim Breitner]

I saw that one, but not the other. Let’s see…

[Kyle Miller]

Re sorries in expressions: you can look for synthetic sorries, which are ones users did not write

[Kyle Miller]

(docs#Lean.Elab.Tactic.evalFailIfSuccess is an example of turning off recovery and error-to-sorry)

[Kyle Miller]

By the way, withoutRecover is key to the implementation of the <|> tactic combinator. That's how the LHS tactic failing can reliably cause backtracking and trying the RHS tactic.

[Kyle Miller]

If you need a bool, perhaps the implementation is (t *> done *> pure true) <|> pure false