fix: let simp arguments elaborate with error recovery (#5863)

Modifies `simp` to elaborate all simp arguments without disabling error
recovery. Like in #4177, simp arguments with elaboration errors are not
added to the simp set. Error recovery is still disabled when `simp` is
used in combinators such as `first`.

This enables better term info and features like tab completion when
there are elaboration errors.

Also included is a fix to the `all_goals` and `<;>` tactic combinators.
Recall that `try`/`catch` for the Tactic monad restores the state on
failure. This meant that all messages were being cleared on tactic
failure. The fix is to use `Tactic.tryCatch` instead, which doesn't
restore state.

Part of addressing #3831

Closes #4888

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -266,15 +266,16 @@ private def getOptRotation (stx : Syntax) : Nat :=
   for mvarId in mvarIds do
     unless (← mvarId.isAssigned) do
       setGoals [mvarId]
-      try
-        evalTactic stx[1]
-        mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals)
-      catch ex =>
-        if (← read).recover then
-          logException ex
-          mvarIdsNew := mvarIdsNew.push mvarId
-        else
-          throw ex
+      mvarIdsNew ← Tactic.tryCatch
+        (do
+          evalTactic stx[1]
+          return mvarIdsNew ++ (← getUnsolvedGoals))
+        (fun ex => do
+          if (← read).recover then
+            logException ex
+            return mvarIdsNew.push mvarId
+          else
+            throw ex)
   setGoals mvarIdsNew.toList
 
 @[builtin_tactic Parser.Tactic.anyGoals] def evalAnyGoals : Tactic := fun stx => do

src/Lean/Elab/Tactic/Simp.lean

@@ -119,17 +119,22 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
     thms.add id #[] e (post := post) (inv := inv)
 
 private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
-  let (levelParams, proof) ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do
+  let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
     let e ← instantiateMVars e
+    if e.hasSyntheticSorry then
+      return none
     let e := e.eta
     if e.hasMVar then
       let r ← abstractMVars e
-      return (r.paramNames, r.expr)
+      return some (r.paramNames, r.expr)
     else
-      return (#[], e)
-  thms.add id levelParams proof (post := post) (inv := inv)
+      return some (#[], e)
+  if let some (levelParams, proof) := thm? then
+    thms.add id levelParams proof (post := post) (inv := inv)
+  else
+    return thms
 
 structure ElabSimpArgsResult where
   ctx      : Simp.Context
@@ -167,7 +172,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
 
     syntax simpErase := "-" ident
     -/
-    withMainContext do
+    let go := withMainContext do
       let mut thmsArray := ctx.simpTheorems
       let mut thms      := thmsArray[0]!
       let mut simprocs  := simprocs
@@ -230,6 +235,12 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
           else
             throw ex
       return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
+    -- If recovery is disabled, then we want simp argument elaboration failures to be exceptions.
+    -- This affects `addSimpTheorem`.
+    if (← read).recover then
+      go
+    else
+      Term.withoutErrToSorry go
 where
   isSimproc? (e : Expr) : MetaM (Option Name) := do
     let .const declName _ := e | return none

tests/lean/run/4888.lean

@@ -0,0 +1,20 @@
+/-!
+# `all_goals` should not consume error messages
+
+https://github.com/leanprover/lean4/issues/4888
+-/
+
+/--
+error: application type mismatch
+  Nat.succ True
+argument
+  True
+has type
+  Prop : Type
+but is expected to have type
+  Nat : Type
+-/
+#guard_msgs in
+theorem bug: True := by
+ all_goals exact Nat.succ True
+ trivial

tests/lean/run/simp-elab-recover.lean

@@ -1,5 +1,5 @@
 /-!
-`simp [invaild]` makes progress which is great for interactive UX, but confusing
+`simp [invalid]` makes progress which is great for interactive UX, but confusing
 when inside a tactic combinator. This checks that without the `recover` flag,
 `simp [invalid]` fails.
 -/
@@ -25,3 +25,9 @@ example : 0 + n = n := by
 example : 0 + n = n := by
   skip <;> simp only [does_not_exist, Nat.zero_add]
   done
+
+/-- error: unknown identifier 'does_not_exist' -/
+#guard_msgs in
+example : 0 + n = n := by
+  all_goals simp only [does_not_exist, Nat.zero_add]
+  done