From f2f71a60281f66d78687128b8fb879e0f7a11fe0 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 09:01:57 -0800
Subject: [PATCH 1/3] fix: Reset core message log

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

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 52562e7..b140ee7 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -250,6 +250,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E
           return .some $ ← m.toString
         else
           return .none
+    Core.resetMessageLog
     if ¬ newMessages.isEmpty then
       return .failure newMessages.toArray
     return .success nextState
-- 
2.44.1


From ab77418e242d81e502f4ae7a88ab7decf8d6b1a6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 09:05:47 -0800
Subject: [PATCH 2/3] fix: Drop previous message lists

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

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index b140ee7..6ff14d2 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -244,7 +244,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E
     let nextState ← state.step goal tacticM guardMVarErrors
 
     -- Check if error messages have been generated in the core.
-    let newMessages ← (← Core.getMessageLog).toList --.drop state.coreState.messages.toList.length
+    let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
       |>.filterMapM λ m => do
         if m.severity == .error then
           return .some $ ← m.toString
-- 
2.44.1


From 396a787771909d722e531acf2c11ffec2dd11900 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 09:06:42 -0800
Subject: [PATCH 3/3] feat: Reset message log in MainM

---
 Repl.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Repl.lean b/Repl.lean
index 283bcf3..2060061 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -79,6 +79,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
+    Lean.Core.resetMessageLog
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
     let state ← get
-- 
2.44.1