fix: display all remaining goals at fail tactic error message

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

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

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"

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