fix: without recover bad simp arg should fail (#4359)

this is an amendment to #4177, after @kmill pointed out an issue:

Users might expect that within a tactic combinator like `first`, `simp
[h]` fails if `h` does not exist. Therefore the behavior introduced in
PR #4177, which is really most useful in mormal interactive use of
`skip`, is restricted to when `recover := true`.

src/Lean/Elab/Tactic/Simp.lean

@@ -153,7 +153,8 @@ 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.
+  When `recover := true`, 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
@@ -223,7 +224,11 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             starArg := true
           else
             throwUnsupportedSyntax
-        catch ex => logException ex
+        catch ex =>
+          if (← read).recover then
+            logException ex
+          else
+            throw ex
       return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
 where
   isSimproc? (e : Expr) : MetaM (Option Name) := do

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

@@ -109,10 +109,16 @@
   "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": "no goals", "goals": []}
+{"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)"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 82, "character": 54}}
-{"rendered": "no goals", "goals": []}
+{"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)"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 86, "character": 38}}
 {"rendered": "no goals", "goals": []}

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

@@ -0,0 +1,27 @@
+/-!
+`simp [invaild]` 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.
+-/
+
+/-- error: unknown identifier 'does_not_exist' -/
+#guard_msgs in
+example : 0 + n = n := by
+  simp only [does_not_exist, Nat.zero_add]
+  done
+
+/--
+error: unsolved goals
+n : Nat
+⊢ 0 + n = n
+-/
+#guard_msgs in
+example : 0 + n = n := by
+  first | simp only [does_not_exist, Nat.zero_add] | skip
+  done
+
+/-- error: unknown identifier 'does_not_exist' -/
+#guard_msgs in
+example : 0 + n = n := by
+  skip <;> simp only [does_not_exist, Nat.zero_add]
+  done