From 7aafd6956fe71770a356f3d852edc4e91cd5696a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Dec 2024 22:07:21 -0800
Subject: [PATCH] fix: Capture composite tactic failure

---
 Pantograph/Goal.lean |  5 +++++
 Test/Common.lean     | 22 ++++++++++++++--------
 Test/Proofs.lean     |  4 ++--
 3 files changed, 21 insertions(+), 10 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 79e3004..be745f4 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -73,6 +73,8 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
   return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
+protected def GoalState.coreState (state: GoalState): Core.SavedState :=
+  state.savedState.term.meta.core
 
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState
@@ -207,6 +209,9 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E
       Elab.TermElabM TacticResult := do
   try
     let nextState ← state.step goal tacticM
+    let newMessages ← (← getThe Core.State).messages.toList.drop (state.coreState.messages.toList.length) |>.mapM λ m => m.toString
+    if ¬ newMessages.isEmpty then
+      return .failure newMessages.toArray
     return .success nextState
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
diff --git a/Test/Common.lean b/Test/Common.lean
index 0a0b44c..212e164 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -123,23 +123,29 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
 
 -- Monadic testing
 
-abbrev TestT := StateT LSpec.TestSeq
+abbrev TestT := StateRefT' IO.RealWorld LSpec.TestSeq
 
-def addTest [Monad m] (test: LSpec.TestSeq) : TestT m Unit := do
+section Monadic
+
+variable [Monad m] [MonadLiftT (ST IO.RealWorld) m]
+
+def addTest (test: LSpec.TestSeq) : TestT m Unit := do
   set $ (← get) ++ test
 
-def checkEq [Monad m] [DecidableEq α] (desc : String) (lhs rhs : α) : TestT m Unit := do
-  addTest $ LSpec.check desc (lhs == rhs)
-def checkTrue [Monad m] (desc : String) (flag : Bool) : TestT m Unit := do
+def checkEq [DecidableEq α] [Repr α] (desc : String) (lhs rhs : α) : TestT m Unit := do
+  addTest $ LSpec.check desc (lhs = rhs)
+def checkTrue (desc : String) (flag : Bool) : TestT m Unit := do
   addTest $ LSpec.check desc flag
-def fail [Monad m] (desc : String) : TestT m Unit := do
+def fail (desc : String) : TestT m Unit := do
   addTest $ LSpec.check desc false
 
-def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
+def runTest (t: TestT m Unit): m LSpec.TestSeq :=
   Prod.snd <$> t.run LSpec.TestSeq.done
-def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) :=
+def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
   t.run LSpec.TestSeq.done
 
+end Monadic
+
 def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
   IO LSpec.TestSeq :=
   runTermElabMSeq env $ runTest t
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 8db8f19..65f099f 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -702,7 +702,7 @@ def test_nat_zero_add_alt: TestM Unit := do
     ])
 
 def test_composite_tactic_failure: TestM Unit := do
-  let state? ← startProof (.expr "∀ (p : Prop), ∃ (x : Nat), p")
+  let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
   let state0 ← match state? with
     | .some state => pure state
     | .none => do
@@ -718,7 +718,7 @@ def test_composite_tactic_failure: TestM Unit := do
 
   let tactic := "exact ⟨0, by simp⟩"
   let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
-  checkEq tactic messages #["placeholder"]
+  checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [