From 2e2658bde79aa02c6593371e098a924488ba98bf Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Dec 2024 21:35:37 -0800
Subject: [PATCH 1/6] test: Add test case for composite tactic

---
 Test/Proofs.lean | 25 +++++++++++++++++++++----
 1 file changed, 21 insertions(+), 4 deletions(-)

diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 02c1bf6..8db8f19 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -14,10 +14,7 @@ inductive Start where
   | copy (name: String) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
-
-def addTest (test: LSpec.TestSeq): TestM Unit := do
-  set $ (← get) ++ test
+abbrev TestM := TestT $ ReaderT Protocol.Options $ Elab.TermElabM
 
 def startProof (start: Start): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
@@ -704,6 +701,25 @@ 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 state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p"
+  let state1 ← match ← state0.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let tactic := "exact ⟨0, by simp⟩"
+  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
+  checkEq tactic messages #["placeholder"]
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("identity", test_identity),
@@ -716,6 +732,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("calc", test_calc),
     ("Nat.zero_add", test_nat_zero_add),
     ("Nat.zero_add alt", test_nat_zero_add_alt),
+    ("composite tactic failure", test_composite_tactic_failure),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

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 2/6] 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 := [

From a62ac51c37ad5dde6c3e850aaaf1e9b9265ec652 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Dec 2024 22:11:37 -0800
Subject: [PATCH 3/6] chore: Remove all redundant filenames

---
 Pantograph/Goal.lean            | 10 ++++------
 Test/Common.lean                |  6 +++---
 Test/Tactic/MotivatedApply.lean |  6 +++---
 Test/Tactic/NoConfuse.lean      |  6 +++---
 Test/Tactic/Prograde.lean       |  2 +-
 5 files changed, 14 insertions(+), 16 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index be745f4..8d29aa8 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -10,8 +10,6 @@ import Lean
 namespace Pantograph
 open Lean
 
-def filename: String := "<pantograph>"
-
 /--
 Represents an interconnected set of metavariables, or a state in proof search
  -/
@@ -224,7 +222,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (env := ← MonadEnv.getEnv)
     (catName := if state.isConv then `conv else `tactic)
     (input := tactic)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
   state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
@@ -236,7 +234,7 @@ protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: Strin
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := expr)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal $ Tactic.evalAssign expr
@@ -250,7 +248,7 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := type)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal $ Tactic.evalLet binderName.toName type
@@ -337,7 +335,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
     (env := state.env)
     (catName := `term)
     (input := pred)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   goal.checkNotAssigned `GoalState.tryCalc
diff --git a/Test/Common.lean b/Test/Common.lean
index 212e164..53adaa0 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -95,19 +95,19 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
-def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
+def strToTermSyntax (s: String): CoreM Syntax := do
   let .ok stx := Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
-    (fileName := filename) | panic! s!"Failed to parse {s}"
+    (fileName := ← getFileName) | panic! s!"Failed to parse {s}"
   return stx
 def parseSentence (s: String): Elab.TermElabM Expr := do
   let stx ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
   Elab.Term.elabTerm (stx := stx) .none
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index 4fb05e3..61d7d6c 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -28,7 +28,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "@Nat.brecOn")
-      (fileName := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -52,7 +52,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "@List.brecOn")
-      (fileName := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -74,7 +74,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := "@Nat.brecOn")
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
   let expr ← parseSentence expr
diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean
index ac277e2..93f0606 100644
--- a/Test/Tactic/NoConfuse.lean
+++ b/Test/Tactic/NoConfuse.lean
@@ -15,7 +15,7 @@ def test_nat : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "h")
-      (fileName := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -32,7 +32,7 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "h")
-      (fileName := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -52,7 +52,7 @@ def test_list : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "h")
-      (fileName := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean
index 132718a..b3347cb 100644
--- a/Test/Tactic/Prograde.lean
+++ b/Test/Tactic/Prograde.lean
@@ -15,7 +15,7 @@ def test_define : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "Or.inl h")
-      (fileName := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic

From 34a4bf5b7321f413e12c1c1cd814d0b0e1a52e29 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Dec 2024 22:12:04 -0800
Subject: [PATCH 4/6] feat: Export GoalState.tryTactic

---
 Pantograph/Goal.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 8d29aa8..ac09109 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -215,6 +215,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E
     return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
+@[export pantograph_goal_state_try_tactic_m]
 protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
     Elab.TermElabM TacticResult := do
   state.restoreElabM

From 0415baaaff3a55475cd532749c1fe9724a16fb43 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Dec 2024 22:16:20 -0800
Subject: [PATCH 5/6] chore: Cleanup old `TestM`

---
 Test/Metavar.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 506e963..c6fc4f0 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -8,10 +8,7 @@ namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
-
-def addTest (test: LSpec.TestSeq): TestM Unit := do
-  set $ (← get) ++ test
+abbrev TestM := TestT $ ReaderT Protocol.Options Elab.TermElabM
 
 -- Tests that all delay assigned mvars are instantiated
 def test_instantiate_mvar: TestM Unit := do
@@ -32,8 +29,6 @@ def test_instantiate_mvar: TestM Unit := do
     "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
   return ()
 
-
-
 def startProof (expr: String): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
   let syn? := parseTerm env expr

From 929311a0429c2fafb5533c8f44e326c6d66b4d9c Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 6 Dec 2024 00:08:20 -0800
Subject: [PATCH 6/6] fix: Only signal failure when there is error

---
 Pantograph/Goal.lean | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index ac09109..e190d5d 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -202,12 +202,19 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
-/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
+/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit):
       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
+
+    -- Check if error messages have been generated in the core.
+    let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
+      |>.filterMapM λ m => do
+        if m.severity == .error then
+          return .some $ ← m.toString
+        else
+          return .none
     if ¬ newMessages.isEmpty then
       return .failure newMessages.toArray
     return .success nextState
@@ -357,7 +364,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
       throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
     if let some prevRhs := calcPrevRhs? then
       unless ← Meta.isDefEqGuarded lhs prevRhs do
-        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- "
+        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}"
 
     -- Creates a mvar to represent the proof that the calc tactic solves the
     -- current branch