fix(goal): Reset messages in replay

Pantograph/Goal.lean

@@ -335,6 +335,9 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM
     core := {
       core with
       ngen,
+      env := ← core.env.replayConsts src.env src'.env (skipExisting := true),
+      -- Reset the message log when declaration uses `sorry`
+      messages := {}
     }
     meta := {
       meta with
@@ -476,7 +479,10 @@ private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × Array
 
 /-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/
 def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do
-  assert! (← Core.getMessageLog).toList.isEmpty
+  let messageLog ← Core.getMessageLog
+  unless messageLog.toList.isEmpty do
+    IO.eprintln s!"{← messageLog.toList.mapM (·.toString)}"
+    assert! messageLog.toList.isEmpty
   try
     let state ← elabM
 

Repl.lean

@@ -412,10 +412,10 @@ def execute (command: Protocol.Command): MainM Json := do
     let state ← getMainState
     let .some goalState := state.goalStates[args.id]? |
       Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.id}"
-    goalStatePickle goalState args.path
+    goalStatePickle goalState args.path (background? := .some $ ← getEnv)
     return {}
   goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do
-    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
+    let (goalState, _) ← goalStateUnpickle args.path (background? := .some $ ← getEnv)
     let id ← newGoalState goalState
     return { id }
 

Test/Common.lean

@@ -187,9 +187,11 @@ namespace Tactic
 
 /-- Create an aux lemma and assigns it to `mvarId`, which is circuitous, but
 exercises the aux lemma generator. -/
-def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do
+def assignWithAuxLemma (type : Expr) (value? : Option Expr := .none) : Elab.Tactic.TacticM Unit := do
   let type ← instantiateMVars type
-  let value ← instantiateMVars value
+  let value ← match value? with
+    | .some value => instantiateMVars value
+    | .none => Meta.mkSorry type (synthetic := false)
   if type.hasExprMVar then
     throwError "Type has expression mvar"
   if value.hasExprMVar then
@@ -200,6 +202,7 @@ def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do
   unless ← Meta.isDefEq type (← goal.getType) do
     throwError "Type provided is incorrect"
   goal.assign (.const name [])
+  Elab.Tactic.pruneSolvedGoals
 
 end Tactic
 

Test/Metavar.lean

@@ -281,6 +281,31 @@ def test_branch_unification : TestM Unit := do
   let .some root := stateT.rootExpr? | fail "Root expression must exist"
   checkEq "(root)" (toString $ ← Meta.ppExpr root) "fun p q h => ⟨h, Or.inl h⟩"
 
+def test_replay_environment : TestM Unit := do
+  let .ok rootTarget ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable!
+  let state ← GoalState.create rootTarget
+  let .success state _  ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | fail "apply And.intro failed to run"
+  let goal := state.goals[0]!
+  let type ← goal.withContext do
+    let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
+    pure type
+  let .success state1 _  ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "left"
+
+  let goal := state.goals[1]!
+  let type ← goal.withContext do
+    let .ok type ← elabTerm (← `(term|(3: Nat) ≤ 5)) (.some $ .sort 0) | unreachable!
+    pure type
+  let .success state2 _  ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "right"
+  checkEq "(state1 goals)" state1.goals.length 0
+  checkEq "(state2 goals)" state2.goals.length 0
+  let stateT ← state2.replay state state1
+  checkEq "(stateT goals)" stateT.goals.length 0
+  let .some root := stateT.rootExpr? | fail "Root expression must exist"
+  checkTrue "root has aux lemma" $ root.getUsedConstants.any (·.isAuxLemma)
+  checkEq "(root)" (toString $ ← Meta.ppExpr root) "⟨_proof_1, _proof_2⟩"
+  let root ← unfoldAuxLemmas root
+  checkEq "(root unfold)" (toString $ ← Meta.ppExpr root) "⟨sorry, sorry⟩"
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("Instantiate", test_instantiate_mvar),
@@ -289,6 +314,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Proposition Generation", test_proposition_generation),
     ("Partial Continuation", test_partial_continuation),
     ("Branch Unification", test_branch_unification),
+    ("Replay Environment", test_replay_environment),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

Test/Serial.lean

@@ -82,18 +82,17 @@ def test_pickling_env_extensions : TestM Unit := do
     let .success state _ ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | unreachable!
 
     let goal := state.goals[0]!
-    let (type, value) ← goal.withContext do
+    let type ← goal.withContext do
       let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
-      let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable!
+      pure type
-      pure (type, value)
+    let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable!
-    let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
     let parentExpr := state1.parentExpr!
-    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
+    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)
     goalStatePickle state1 statePath
   let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
     let (state1, _) ← goalStateUnpickle statePath (← getEnv)
     let parentExpr := state1.parentExpr!
-    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
+    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)
 
   return ()