Pantograph/Goal.lean

@@ -136,8 +136,9 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n]
   Meta.mapMetaM <| state.withContext' state.root
 
 private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit :=
+  let { nextMacroScope, ngen, .. } := state
   modifyGetThe Core.State (fun st => ((),
-    { st with nextMacroScope := state.nextMacroScope, ngen := state.ngen }))
+    { st with nextMacroScope, ngen }))
 -- Restore the name generator and macro scopes of the core state
 protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
   restoreCoreMExtra state.coreState
@@ -335,6 +336,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 +480,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
 

Pantograph/Serial.lean

@@ -1,19 +1,19 @@
-import Lean.Environment
-import Lean.Replay
-import Init.System.IOError
-import Std.Data.HashMap
 import Pantograph.Goal
 
+import Lean.Environment
+import Lean.Replay
+import Std.Data.HashMap
+
+open Lean
+
 /-!
-Input/Output functions
+Input/Output functions borrowed from REPL
 
 # Pickling and unpickling objects
 
 By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk.
 -/
 
-open Lean
-
 namespace Pantograph
 
 /--
@@ -46,6 +46,21 @@ unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type}
   region.free
   pure r
 
+abbrev ConstArray := Array (Name × ConstantInfo)
+abbrev DistilledEnvironment := Array Import × ConstArray
+
+/-- Boil an environment down to minimal components -/
+def distillEnvironment (env : Environment) (background? : Option Environment := .none)
+  : DistilledEnvironment :=
+  let filter : Name → Bool := match background? with
+    | .some env => (¬ env.contains ·)
+    | .none => λ _ => true
+  let constants : ConstArray := env.constants.map₂.foldl (init := #[]) λ acc name info =>
+    if filter name then
+      acc.push (name, info)
+    else
+      acc
+  (env.header.imports, constants)
 /--
 Pickle an `Environment` to disk.
 
@@ -56,15 +71,23 @@ and when unpickling, we build a fresh `Environment` from the imports,
 and then add the new constants.
 -/
 @[export pantograph_env_pickle_m]
-def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit :=
+def environmentPickle (env : Environment) (path : System.FilePath) (background? : Option Environment := .none)
-  Pantograph.pickle path (env.header.imports, env.constants.map₂)
+  : IO Unit :=
+  pickle path $ distillEnvironment env background?
+
+deriving instance BEq for Import
 
 def resurrectEnvironment
-  (imports : Array Import)
+  (distilled : DistilledEnvironment)
-  (map₂ : PHashMap Name ConstantInfo)
+  (background? : Option Environment := .none)
   : IO Environment := do
-  let env ← importModules imports {} 0 (loadExts := true)
+  let (imports, constArray) := distilled
-  env.replay (Std.HashMap.ofList map₂.toList)
+  let env ← match background? with
+    | .none => importModules imports {} 0 (loadExts := true)
+    | .some env =>
+      assert! env.imports == imports
+      pure env
+  env.replay (Std.HashMap.ofList constArray.toList)
 /--
 Unpickle an `Environment` from disk.
 
@@ -72,9 +95,10 @@ We construct a fresh `Environment` with the relevant imports,
 and then replace the new constants.
 -/
 @[export pantograph_env_unpickle_m]
-def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
+def environmentUnpickle (path : System.FilePath) (background? : Option Environment := .none)
-  let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
+  : IO (Environment × CompactedRegion) := unsafe do
-  return (← resurrectEnvironment imports map₂, region)
+  let (distilled, region) ← unpickle (Array Import × ConstArray) path
+  return (← resurrectEnvironment distilled background?, region)
 
 
 open Lean.Core in
@@ -88,7 +112,8 @@ structure CompactCoreState where
   -- infoState       : Elab.InfoState := {}
 
 @[export pantograph_goal_state_pickle_m]
-def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :=
+def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background? : Option Environment := .none)
+  : IO Unit :=
   let {
     savedState := {
       term := {
@@ -106,8 +131,8 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
     parentMVars,
     fragments,
   } := goalState
-  Pantograph.pickle path (
+  pickle path (
-    env.constants.map₂,
+    distillEnvironment env background?,
 
     ({ nextMacroScope, ngen } : CompactCoreState),
     meta,
@@ -120,10 +145,10 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
   )
 
 @[export pantograph_goal_state_unpickle_m]
-def goalStateUnpickle (path : System.FilePath) (env : Environment)
+def goalStateUnpickle (path : System.FilePath) (background? : Option Environment := .none)
     : IO (GoalState × CompactedRegion) := unsafe do
   let ((
-    map₂,
+    distilledEnv,
 
     compactCore,
     meta,
@@ -134,7 +159,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
     parentMVars,
     fragments,
   ), region) ← Pantograph.unpickle (
-    PHashMap Name ConstantInfo ×
+    DistilledEnvironment ×
 
     CompactCoreState ×
     Meta.State ×
@@ -145,7 +170,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
     List MVarId ×
     FragmentMap
   ) path
-  let env ← env.replay (Std.HashMap.ofList map₂.toList)
+  let env ← resurrectEnvironment distilledEnv background?
   let goalState := {
     savedState := {
       term := {

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,32 @@ 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"
+
+  state.restoreMetaM
+  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 +315,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 ()