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]

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
+def checkEq [DecidableEq α] [Repr α] (desc : String) (lhs rhs : α) : TestT m Unit := do
-  addTest $ LSpec.check desc (lhs == rhs)
+  addTest $ LSpec.check desc (lhs = rhs)
-def checkTrue [Monad m] (desc : String) (flag : Bool) : TestT m Unit := do
+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

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 := [