feat: simp to still work even if one simp arg does not work

src/Lean/Elab/Tactic/Simp.lean

@@ -153,6 +153,7 @@ inductive ResolveSimpIdResult where
   Elaborate extra simp theorems provided to `simp`. `stx` is of the form `"[" simpTheorem,* "]"`
   If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`),
   this option only makes sense for `simp_all` or `*` is used.
+  Try to recover from errors as much as possible so that users keep seeing the current goal.
 -/
 def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
   if stx.isNone then
@@ -172,8 +173,8 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
       let mut starArg   := false
       for arg in stx[1].getSepArgs do
         if arg.getKind == ``Lean.Parser.Tactic.simpErase then
-          let fvar ← if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none
-          if let some fvar := fvar then
+          let fvar? ← if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none
+          if let some fvar := fvar? then
             -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
@@ -184,15 +185,15 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
               else if ctx.config.autoUnfold then
                 thms := thms.eraseCore (.decl declName)
               else
-                thms ← thms.erase (.decl declName)
+                thms ← withRef id <| thms.erase (.decl declName)
             else
               -- If `id` could not be resolved, we should check whether it is a builtin simproc.
               -- before returning error.
               let name := id.getId.eraseMacroScopes
               if (← Simp.isBuiltinSimproc name) then
                 simprocs := simprocs.erase name
               else
-                throwUnknownConstant name
+                withLogging <| withRef id <| throwUnknownConstant name
         else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
           let post :=
             if arg[0].isNone then
@@ -201,7 +202,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
               arg[0][0].getKind == ``Parser.Tactic.simpPost
           let inv  := !arg[1].isNone
           let term := arg[2]
-          match (← resolveSimpIdTheorem? term) with
+          match ← resolveSimpIdTheorem? term with
           | .expr e  =>
             let name ← mkFreshId
             thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
@@ -216,7 +217,8 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             simprocs  := simprocs.push (← ext₂.getSimprocs)
           | .none    =>
             let name ← mkFreshId
-            thms ← addSimpTheorem thms (.stx name arg) term post inv
+            thms ← withLoggingD thms <|
+              addSimpTheorem thms (.stx name arg) term post inv
         else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
           starArg := true
         else

src/Lean/Elab/Util.lean

@@ -209,9 +209,20 @@ def logException [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [
       let name ← id.getName
       logError m!"internal exception: {name}"
 
+/--
+If `x` throws an exception, catch it, turn it into a log message (using `logException`), and returns
+the given default value.
+-/
+def withLoggingD [Monad m] [MonadLog m] [MonadExcept Exception m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
+    (d : α) (x : m α) : m α := do
+  try x catch ex => logException ex; pure d
+
+/--
+If `x` throws an exception, catch it, turn it into a log message (using `logException`).
+-/
 def withLogging [Monad m] [MonadLog m] [MonadExcept Exception m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
-    (x : m Unit) : m Unit := do
-  try x catch ex => logException ex
+    (x : m Unit) : m Unit := withLoggingD .unit x
+
 
 def nestedExceptionToMessageData [Monad m] [MonadLog m] (ex : Exception) : m MessageData := do
   let pos ← getRefPos

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -221,13 +221,14 @@ partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpThe
   else
     d
 
-def SimpTheorems.erase [Monad m] [MonadError m] (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
+def SimpTheorems.erase [Monad m] [MonadLog m]  [AddMessageContext m] [MonadOptions m]
+    (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
   unless d.isLemma thmId ||
     match thmId with
     | .decl declName .. => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
     | _ => false
   do
-    throwError "'{thmId.key}' does not have [simp] attribute"
+    logWarning m!"'{thmId.key}' does not have [simp] attribute"
   return d.eraseCore thmId
 
 private partial def isPerm : Expr → Expr → MetaM Bool

tests/lean/eraseSimp.lean.expected.out

@@ -1 +1 @@
-eraseSimp.lean:4:18-4:21: error: 'foo' does not have [simp] attribute
+eraseSimp.lean:4:18-4:21: warning: 'foo' does not have [simp] attribute

tests/lean/interactive/plainGoal.lean.expected.out

@@ -109,16 +109,10 @@
   "t a n✝ : Nat\na✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 82, "character": 53}}
-{"rendered":
- "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
- "goals":
- ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
+{"rendered": "no goals", "goals": []}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 82, "character": 54}}
-{"rendered":
- "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
- "goals":
- ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
+{"rendered": "no goals", "goals": []}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 86, "character": 38}}
 {"rendered": "no goals", "goals": []}

tests/lean/run/simproc1.lean

@@ -30,7 +30,7 @@ example : x + foo 2 = 12 + x := by
 
 example : x + foo 2 = 12 + x := by
   -- We can use `-` to disable `simproc`s
-  fail_if_success simp [-reduce_foo]
+  fail_if_success simp [-reduceFoo]
   simp_arith
 
 example (x : Nat) (h : x < 86) : ¬100 ≤ x + 14 := by simp; exact h