From f22b48b2269324258ad121c6003a91a53de5b5cd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Feb 2022 09:49:06 -0800
Subject: [PATCH] fix: display all remaining goals at `fail` tactic error
 message

---
 src/Lean/Elab/Tactic/Basic.lean         | 2 +-
 src/Lean/Elab/Tactic/BuiltinTactic.lean | 7 ++++---
 tests/lean/failTac.lean                 | 4 ++++
 tests/lean/failTac.lean.expected.out    | 8 ++++++++
 4 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 7bdc1ffd4b..f9377f3a01 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -26,7 +26,7 @@ def admitGoal (mvarId : MVarId) : MetaM Unit :=
     assignExprMVar mvarId (← mkSorry mvarType (synthetic := true))
 
 def goalsToMessageData (goals : List MVarId) : MessageData :=
-  MessageData.joinSep (goals.map $ MessageData.ofGoal) m!"\n\n"
+  MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n"
 
 def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit :=
   withPPInaccessibleNames do
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 681e94c190..2b8a595d25 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -274,13 +274,14 @@ where
       evalTactic tacs[i][1] <|> loop tacs (i+1)
 
 @[builtinTactic «fail»] def evalFail : Tactic := fun stx => do
-  let mvarId ← getMainGoal
+  let goals ← getGoals
+  let goalsMsg := MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n"
   match stx with
-  | `(tactic| fail)      => throwError "tactic 'fail' failed\n{mvarId}"
+  | `(tactic| fail)      => throwError "tactic 'fail' failed\n{goalsMsg}"
   | `(tactic| fail $msg) =>
     match msg.isStrLit? with
     | none     => throwIllFormedSyntax
-    | some msg => throwError "{msg}\n{mvarId}"
+    | some msg => throwError "{msg}\n{goalsMsg}"
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic
diff --git a/tests/lean/failTac.lean b/tests/lean/failTac.lean
index 27ad4c015a..f2f1f326a2 100644
--- a/tests/lean/failTac.lean
+++ b/tests/lean/failTac.lean
@@ -8,3 +8,7 @@ example (a b : Nat) : True := by
   first
    | fail "giving up"
    | constructor
+
+example (a b : Nat) : True ∧ False := by
+  constructor
+  fail "failing here"
diff --git a/tests/lean/failTac.lean.expected.out b/tests/lean/failTac.lean.expected.out
index c52e439710..72b99491b6 100644
--- a/tests/lean/failTac.lean.expected.out
+++ b/tests/lean/failTac.lean.expected.out
@@ -4,3 +4,11 @@ a b : Nat
 failTac.lean:5:2-5:18: error: giving up
 a b : Nat
 ⊢ False
+failTac.lean:14:2-14:21: error: failing here
+case left
+a b : Nat
+⊢ True
+
+case right
+a b : Nat
+⊢ False