Disappearing error message.

Stream: lean4

[Patrick Massot]

The following code contains two variants of https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Calc.lean#L19. The first one simply removes some code that is not relevant to the question. Unsurprisingly the corresponding Calc tactic show an error message when there is an unknown variable in the code. Then the Balc tactic has exactly the same code but wrapped into a try … catch e => throw e. This time the error message disappears and we only get a sorry. How could I fix that?

import Lean

open Lean Elab Tactic Meta

syntax "Calc" calcSteps : tactic

elab_rules : tactic
| `(tactic| Calc%$tk $steps:calcSteps) =>
    withRef tk do
    closeMainGoalUsing `calc (checkNewUnassigned := false) fun target tag => do
    withTacticInfoContext steps do
      let steps ← Term.mkCalcStepViews steps
      let target := (← instantiateMVars target).consumeMData
      let (val, mvarIds) ← withCollectingNewGoalsFrom (parentTag := tag) (tagSuffix := `calc) <| runTermElab do
        let (val, valType) ← Term.elabCalcSteps steps
        if (← isDefEq valType target) then
          -- Immediately the right type, no need for further processing.
          return val

        Term.ensureHasTypeWithErrorMsgs target val
          (mkImmedErrorMsg := fun _ => Term.throwCalcFailure steps)
          (mkErrorMsg := fun _ => Term.throwCalcFailure steps)
      pushGoals mvarIds
      return val

/-- error: Unknown identifier `x` -/
#guard_msgs in
example : 1 = 1 := by
    Calc x = 1 := rfl
         _ = 1 := rfl

syntax "Balc" calcSteps : tactic

elab_rules : tactic
| `(tactic| Balc%$tk $steps:calcSteps) =>
    withRef tk do
    try
      closeMainGoalUsing `calc (checkNewUnassigned := false) fun target tag => do
      withTacticInfoContext steps do
        let steps ← Term.mkCalcStepViews steps
        let target := (← instantiateMVars target).consumeMData
        let (val, mvarIds) ← withCollectingNewGoalsFrom (parentTag := tag) (tagSuffix := `calc) <| runTermElab do
          let (val, valType) ← Term.elabCalcSteps steps
          if (← isDefEq valType target) then
            -- Immediately the right type, no need for further processing.
            return val

          Term.ensureHasTypeWithErrorMsgs target val
            (mkImmedErrorMsg := fun _ => Term.throwCalcFailure steps)
            (mkErrorMsg := fun _ => Term.throwCalcFailure steps)
        pushGoals mvarIds
        return val
    catch e => throw e

/-- warning: declaration uses 'sorry' -/
#guard_msgs in
example : 1 = 1 := by
    Balc x = 1 := rfl
         _ = 1 := rfl

[Patrick Massot]

Of course in my real code I’d like to try more things in the catch part, but still being able to throw e (and get the error message) when it fails.

[Thomas Murrills]

What's going on here is that Term.throwCalcFailure is merely logging the informative error that you want to keep, and the actual error it throws (which is caught by catch) is an internal error, from e.g. throwAbortTerm. If you write catch e => logInfo m!"{e.toMessageData}"; throw e instead, you can see from the logged message that e is internal exception #4. That is, e does not contain these errors you see; the messages in the tactic state do, and try/catch is rewinding that state when it catches the error.

I believe you might have to resort to docs#Lean.Elab.Tactic.tryCatch, which is just a regular function that does non-backtracking try/catch. Then you can manage state manually like so (replace the Balc elab_rules in your code above):

elab_rules : tactic
| `(tactic| Balc%$tk $steps:calcSteps) =>
    withRef tk do
    let s ← saveState
    Tactic.tryCatch (do
      -- same code...
      closeMainGoalUsing `calc (checkNewUnassigned := false) fun target tag => do
        withTacticInfoContext steps do
          let steps ← Term.mkCalcStepViews steps
          let target := (← instantiateMVars target).consumeMData
          let (val, mvarIds) ← withCollectingNewGoalsFrom (parentTag := tag) (tagSuffix := `calc) <| runTermElab do
            let (val, valType) ← Term.elabCalcSteps steps
            if (← isDefEq valType target) then
              -- Immediately the right type, no need for further processing.
              return val

            Term.ensureHasTypeWithErrorMsgs target val
              (mkImmedErrorMsg := fun _ => Term.throwCalcFailure steps)
              (mkErrorMsg := fun _ => Term.throwCalcFailure steps)
          pushGoals mvarIds
          return val)
      -- ...until here.
      (fun e₁ => do
        -- save the state created by the failure, which has error messages
        let failureState ← saveState
        try
          s.restore -- restore the initial state to start fresh
          let success := false
          unless success do throwError "Oh no, a second time!"
        catch _e₂ => do
          -- in the case of a second failure restore state of first failure and throw that error
          failureState.restore; throw e₁)

You may need to make your nested try/catch a Tactic.tryCatch if you want to save state from there as well! And you may want to do things like merge your two exceptions or messages.

Technically the second try/catch will save and restore failureState automatically. But I wanted to make it clear what's going on, and give you the chance to adjust it to another Tactic.tryCatch if you need to.

Note also that this is partly because you're in TacticM. You might be aware that there's quite unfortunate inconsistency among do notation try/catch: TacticM's try/catch backtracks, restoring the state, but in other monads like MetaM it won't.

[Thomas Murrills]

(EDIT: hang on, I think I copied the wrong code, or made an edit somewhere...) ah, nevermind, all is well.

[Patrick Massot]

Thanks a lot Thomas! I had partly understood what was going on but couldn’t fix it. Your solution also seems to work in my real code.