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

…er#4177)

this fixes a usability paper cut that just annoyed me. When editing a
larger simp proof, I usually want to see the goal state after the simp,
and this is what I see while the `simp` command is complete. But then,
when I start typing, and necessarily type incomplete lemma names, that
error makes `simp` do nothing again and I see the original goal state.
In fact, if a prefix of the simp theorem name I am typing is a valid
identifier, it jumps even more around.

With this PR, using `logException`, I still get the red squiggly lines
for the unknown identifer, but `simp` just ignores that argument and
still shows me the final goal. Much nicer.

I also demoted the message for `[-foo]` when `foo` isn’t `simp` to a
warning and gave it the correct `ref`.

See it in action here: (in the middle, when you suddenly see the
terminal,
I am switching lean versions.)


https://github.com/leanprover/lean4/assets/148037/8cb3c563-1354-4c2d-bcee-26dfa1005ae0

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
@@ -171,56 +172,58 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
       let mut simprocs  := simprocs
       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
-            -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
-            thms := thms.eraseCore (.fvar fvar.fvarId!)
-          else
-            let id := arg[1]
-            if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
-              if (← Simp.isSimproc declName) then
-                simprocs := simprocs.erase declName
-              else if ctx.config.autoUnfold then
-                thms := thms.eraseCore (.decl declName)
-              else
-                thms ← thms.erase (.decl declName)
+        try -- like withLogging, but compatible with do-notation
+          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
+              -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
+              thms := thms.eraseCore (.fvar fvar.fvarId!)
             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
+              let id := arg[1]
+              if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
+                if (← Simp.isSimproc declName) then
+                  simprocs := simprocs.erase declName
+                else if ctx.config.autoUnfold then
+                  thms := thms.eraseCore (.decl declName)
+                else
+                  thms ← withRef id <| thms.erase (.decl declName)
               else
-                throwUnknownConstant name
-        else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
-          let post :=
-            if arg[0].isNone then
-              true
-            else
-              arg[0][0].getKind == ``Parser.Tactic.simpPost
-          let inv  := !arg[1].isNone
-          let term := arg[2]
-          match (← resolveSimpIdTheorem? term) with
-          | .expr e  =>
-            let name ← mkFreshId
-            thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
-          | .simproc declName =>
-            simprocs ← simprocs.add declName post
-          | .ext (some ext₁) (some ext₂) _ =>
-            thmsArray := thmsArray.push (← ext₁.getTheorems)
-            simprocs  := simprocs.push (← ext₂.getSimprocs)
-          | .ext (some ext₁) none _ =>
-            thmsArray := thmsArray.push (← ext₁.getTheorems)
-          | .ext none (some ext₂) _ =>
-            simprocs  := simprocs.push (← ext₂.getSimprocs)
-          | .none    =>
-            let name ← mkFreshId
-            thms ← addSimpTheorem thms (.stx name arg) term post inv
-        else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
-          starArg := true
-        else
-          throwUnsupportedSyntax
+                -- 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
+                  withRef id <| throwUnknownConstant name
+          else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
+            let post :=
+              if arg[0].isNone then
+                true
+              else
+                arg[0][0].getKind == ``Parser.Tactic.simpPost
+            let inv  := !arg[1].isNone
+            let term := arg[2]
+            match (← resolveSimpIdTheorem? term) with
+            | .expr e  =>
+              let name ← mkFreshId
+              thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
+            | .simproc declName =>
+              simprocs ← simprocs.add declName post
+            | .ext (some ext₁) (some ext₂) _ =>
+              thmsArray := thmsArray.push (← ext₁.getTheorems)
+              simprocs  := simprocs.push (← ext₂.getSimprocs)
+            | .ext (some ext₁) none _ =>
+              thmsArray := thmsArray.push (← ext₁.getTheorems)
+            | .ext none (some ext₂) _ =>
+              simprocs  := simprocs.push (← ext₂.getSimprocs)
+            | .none    =>
+              let name ← mkFreshId
+              thms ← addSimpTheorem thms (.stx name arg) term post inv
+          else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
+            starArg := true
+          else
+            throwUnsupportedSyntax
+        catch ex => logException ex
       return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
 where
   isSimproc? (e : Expr) : MetaM (Option Name) := do

src/Lean/Elab/Util.lean

@@ -209,6 +209,9 @@ 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 and 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

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

@@ -31,7 +31,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