From 262ac674aa29b0f11e609150aa62a79c61e1bf8f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Jul 2022 07:40:26 -0700
Subject: [PATCH] feat: improve `runTactic`

It must catch exceptions.
See #1342
---
 src/Lean/Elab/SyntheticMVars.lean             | 18 +++++++++----
 tests/lean/1074b.lean.expected.out            |  5 ----
 tests/lean/1301.lean.expected.out             |  1 +
 tests/lean/runTacticMustCatchExceptions.lean  | 11 ++++++++
 ...acticMustCatchExceptions.lean.expected.out | 27 +++++++++++++++++++
 5 files changed, 52 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/runTacticMustCatchExceptions.lean
 create mode 100644 tests/lean/runTacticMustCatchExceptions.lean.expected.out

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 064f015390..b5ef41f8ca 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/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
diff --git a/tests/lean/1074b.lean.expected.out b/tests/lean/1074b.lean.expected.out
index 16fe748212..55b37e8482 100644
--- a/tests/lean/1074b.lean.expected.out
+++ b/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)
diff --git a/tests/lean/1301.lean.expected.out b/tests/lean/1301.lean.expected.out
index 964b6e3b2d..c760eef6e5 100644
--- a/tests/lean/1301.lean.expected.out
+++ b/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
diff --git a/tests/lean/runTacticMustCatchExceptions.lean b/tests/lean/runTacticMustCatchExceptions.lean
new file mode 100644
index 0000000000..534dda2670
--- /dev/null
+++ b/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
diff --git a/tests/lean/runTacticMustCatchExceptions.lean.expected.out b/tests/lean/runTacticMustCatchExceptions.lean.expected.out
new file mode 100644
index 0000000000..47f3cba7c0
--- /dev/null
+++ b/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