remove throwing exceptions on error, this is needed for leanprover#4177

src/Lean/Elab/Tactic/Simp.lean

@@ -118,7 +118,7 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
   else
     thms.add id #[] e (post := post) (inv := inv)
 
-private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM (Option SimpTheorems) := do
+private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
   let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
@@ -134,7 +134,7 @@ private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (p
   if let some (levelParams, proof) := thm? then
     thms.add id levelParams proof (post := post) (inv := inv)
   else
-    return none
+    return thms
 
 structure ElabSimpArgsResult where
   ctx      : Simp.Context
@@ -172,12 +172,11 @@ 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
       let mut starArg   := false
-      let mut elabFail  := false
       for arg in stx[1].getSepArgs do
         try -- like withLogging, but compatible with do-notation
           if arg.getKind == ``Lean.Parser.Tactic.simpErase then
@@ -225,10 +224,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
               simprocs  := simprocs.push (← ext₂.getSimprocs)
             | .none    =>
               let name ← mkFreshId
-              if let some thms' ← addSimpTheorem thms (.stx name arg) term post inv then
-                thms := thms'
-              else
-                elabFail := true
+              thms ← addSimpTheorem thms (.stx name arg) term post inv
           else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
             starArg := true
           else
@@ -238,13 +234,13 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             logException ex
           else
             throw ex
-      if elabFail then
-        if ← MonadLog.hasErrors then
-          throwAbortTactic
-        else
-          -- We assume elaboration failure logs error messages. However, we have this backup exception just in case:
-          throwError "'simp' tactic failed to elaborate simp arguments"
       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/1569.lean.expected.out

@@ -1,3 +1 @@
 1569.lean:2:26-2:30: error: unknown identifier 'typo'
-1569.lean:2:17-2:37: error: unsolved goals
-⊢ 0 = 0

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

@@ -4,13 +4,7 @@ when inside a tactic combinator. This checks that without the `recover` flag,
 `simp [invalid]` fails.
 -/
 
-/--
-error: unknown identifier 'does_not_exist'
----
-error: unsolved goals
-n : Nat
-⊢ 0 + n = n
--/
+/-- error: unknown identifier 'does_not_exist' -/
 #guard_msgs in
 example : 0 + n = n := by
   simp only [does_not_exist, Nat.zero_add]
@@ -26,13 +20,7 @@ example : 0 + n = n := by
   first | simp only [does_not_exist, Nat.zero_add] | skip
   done
 
-/--
-error: unknown identifier 'does_not_exist'
----
-error: unsolved goals
-n : Nat
-⊢ 0 + n = n
--/
+/-- error: unknown identifier 'does_not_exist' -/
 #guard_msgs in
 example : 0 + n = n := by
   all_goals simp only [does_not_exist, Nat.zero_add]

tests/lean/simpArgTypeMismatch.lean.expected.out

@@ -6,8 +6,3 @@ has type
   Type : Type 1
 but is expected to have type
   ¬?m : Prop
-simpArgTypeMismatch.lean:2:41-3:34: error: unsolved goals
-p : Prop
-inst✝ : Decidable p
-hnp : ¬p
-⊢ if decide p = true then 0 = 1 else 1 = 1