From 575b1187c500af22bfc4c49c8aa58371d91843fa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 Apr 2022 10:47:15 -0700
Subject: [PATCH] feat: add `Tactic.Context.recover` for controlling error
 recovery

Moreover, when executing `tac_1 <|> tac_2`, we now disable error
recovery at `tac_1`.

closes #1126 #1127
---
 src/Lean/Elab/Tactic/Basic.lean         | 23 ++++++++++++++++++-----
 src/Lean/Elab/Tactic/BuiltinTactic.lean |  7 +++++--
 tests/lean/run/1127.lean                | 25 +++++++++++++++++++++++++
 3 files changed, 48 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/1127.lean

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 5e037a5bf0..9add88f68e 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -37,8 +37,14 @@ namespace Tactic
 
 structure Context where
   main       : MVarId
-  -- declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree
+  /-- Declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree -/
   elaborator : Name
+  /--
+    If `true`, enable "error recovery" in some tactics. For example, `cases` tactic
+    admits unsolved alternatives when `recover == true`. The combinator `withoutRecover <tac>` disables
+    "error recovery" while executing `<tac>`. This is useful for tactics such as `first | ... | ...`.
+  -/
+  recover    : Bool := true
 
 structure SavedState where
   term   : Term.SavedState
@@ -221,9 +227,12 @@ def closeUsingOrAdmit (tac : TacticM Unit) : TacticM Unit := do
   try
     focusAndDone tac
   catch ex =>
-    logException ex
-    admitGoal mvarId
-    setGoals mvarIds
+    if (← read).recover then
+      logException ex
+      admitGoal mvarId
+      setGoals mvarIds
+    else
+      throw ex
 
 instance : MonadBacktrack SavedState TacticM where
   saveState := Tactic.saveState
@@ -237,8 +246,12 @@ instance : MonadExcept Exception TacticM where
   throw    := throw
   tryCatch := Tactic.tryCatch
 
+/-- Execute `x` with error recovery disabled -/
+def withoutRecover (x : TacticM α) : TacticM α :=
+  withReader (fun ctx => { ctx with recover := false }) x
+
 @[inline] protected def orElse {α} (x : TacticM α) (y : Unit → TacticM α) : TacticM α := do
-  try x catch _ => y ()
+  try withoutRecover x catch _ => y ()
 
 instance {α} : OrElse (TacticM α) where
   orElse := Tactic.orElse
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 8beda4ffe3..f84cfce785 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -116,8 +116,11 @@ private def getOptRotation (stx : Syntax) : Nat :=
         evalTactic stx[1]
         mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals)
       catch ex =>
-        logException ex
-        mvarIdsNew := mvarIdsNew.push mvarId
+        if (← read).recover then
+          logException ex
+          mvarIdsNew := mvarIdsNew.push mvarId
+        else
+          throw ex
   setGoals mvarIdsNew.toList
 
 @[builtinTactic Parser.Tactic.anyGoals] def evalAnyGoals : Tactic := fun stx => do
diff --git a/tests/lean/run/1127.lean b/tests/lean/run/1127.lean
new file mode 100644
index 0000000000..1c9d8d1ad3
--- /dev/null
+++ b/tests/lean/run/1127.lean
@@ -0,0 +1,25 @@
+example: p ∧ q := by first | apply And.intro <;> fail | sorry
+
+variable (p q : Prop)
+
+example (hp : p) : p := by
+  try trivial -- succeeds, as expected
+
+example : p := by
+  try trivial -- fails quietly, as expected
+  admit
+
+example (hp : p) (hq : q) : p ∧ q := by
+  try trivial -- succeeds, as expected
+
+example (hp : p) : p ∧ q := by
+  try trivial
+  admit
+
+example (hq : p) : p ∧ q := by
+  try trivial
+  admit
+
+example : p ∧ q := by
+  try trivial -- fails quietly
+  admit       -- splits goals p and q