feat: improve runTactic

It must catch exceptions.
See #1342

src/Lean/Elab/SyntheticMVars.lean

@@ -322,11 +322,19 @@ mutual
     /- Recall, `tacticCode` is the whole `by ...` expression. -/
     let code := tacticCode[1]
     instantiateMVarDeclMVars mvarId
-    let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
-       withTacticInfoContext tacticCode (evalTactic code)
-       synthesizeSyntheticMVars (mayPostpone := false)
-    unless remainingGoals.isEmpty do
-      reportUnsolvedGoals remainingGoals
+    try
+      let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
+         withTacticInfoContext tacticCode (evalTactic code)
+         synthesizeSyntheticMVars (mayPostpone := false)
+      unless remainingGoals.isEmpty do
+        reportUnsolvedGoals remainingGoals
+    catch ex =>
+      if (← read).errToSorry then
+        for mvarId in (← getMVars (mkMVar mvarId)) do
+          mvarId.admit
+        logException ex
+      else
+        throw ex
 
   /-- Try to synthesize the given pending synthetic metavariable. -/
   private partial def synthesizeSyntheticMVar (mvarId : MVarId) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := do

tests/lean/1074b.lean.expected.out

@@ -2,8 +2,3 @@
 1074b.lean:11:43-11:53: error: tactic 'assumption' failed
 a n : Term
 ⊢ Brx (sorryAx Term true)
-1074b.lean:11:9-11:55: error: unsolved goals
-case id
-a n z✝ : Term
-: Brx z✝
-⊢ True ∧ Brx (sorryAx Term true)

tests/lean/1301.lean.expected.out

@@ -1,6 +1,7 @@
 1301.lean:2:23-2:26: error: tactic 'tacticTac' has not been implemented
 a : True
 1301.lean:5:32-5:35: error: tactic 'tacticTac' has not been implemented
+1301.lean:5:40-5:43: error: tactic 'tacticTac' has not been implemented
 a' : True ∧ True
 1301.lean:9:25-9:29: error: elaboration function for 'termTerm' has not been implemented
   term

tests/lean/runTacticMustCatchExceptions.lean

@@ -0,0 +1,11 @@
+example (a b : Nat) : 1 ≤ 2 :=
+  have : 1 ≤ a + b := by rfl
+  have : a + b ≤ b := by rfl
+  have : b ≤ 2     := by rfl
+  by decide
+
+example (a b : Nat) : 1 ≤ 2 :=
+calc
+  1 ≤ a + b := by rfl
+  _ ≤ b := by rfl
+  _ ≤ 2 := by rfl

tests/lean/runTacticMustCatchExceptions.lean.expected.out

@@ -0,0 +1,27 @@
+runTacticMustCatchExceptions.lean:2:25-2:28: error: tactic 'rfl' failed, equality expected
+  Nat.le 1 (a + b)
+a b : Nat
+⊢ 1 ≤ a + b
+runTacticMustCatchExceptions.lean:3:25-3:28: error: tactic 'rfl' failed, equality expected
+  Nat.le (a + b) b
+a b : Nat
+this : 1 ≤ a + b
+⊢ a + b ≤ b
+runTacticMustCatchExceptions.lean:4:25-4:28: error: tactic 'rfl' failed, equality expected
+  Nat.le b 2
+a b : Nat
+: 1 ≤ a + b
+this : a + b ≤ b
+⊢ b ≤ 2
+runTacticMustCatchExceptions.lean:9:18-9:21: error: tactic 'rfl' failed, equality expected
+  Nat.le 1 (a + b)
+a b : Nat
+⊢ 1 ≤ a + b
+runTacticMustCatchExceptions.lean:10:14-10:17: error: tactic 'rfl' failed, equality expected
+  Nat.le (a + b) b
+a b : Nat
+⊢ a + b ≤ b
+runTacticMustCatchExceptions.lean:11:14-11:17: error: tactic 'rfl' failed, equality expected
+  Nat.le b 2
+a b : Nat
+⊢ b ≤ 2