Pantograph/Goal.lean

@@ -136,9 +136,8 @@ 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, ngen }))
+    { st with nextMacroScope := state.nextMacroScope, ngen := state.ngen }))
 -- Restore the name generator and macro scopes of the core state
 protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
   restoreCoreMExtra state.coreState
@@ -336,9 +335,6 @@ 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
@@ -480,10 +476,7 @@ 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
-  let messageLog ← Core.getMessageLog
-  unless messageLog.toList.isEmpty do
-    IO.eprintln s!"{← messageLog.toList.mapM (·.toString)}"
-    assert! messageLog.toList.isEmpty
+  assert! (← Core.getMessageLog).toList.isEmpty
   try
     let state ← elabM
 

Pantograph/Serial.lean

@@ -1,19 +1,19 @@
-import Pantograph.Goal
-
 import Lean.Environment
 import Lean.Replay
+import Init.System.IOError
 import Std.Data.HashMap
-
-open Lean
+import Pantograph.Goal
 
 /-!
-Input/Output functions borrowed from REPL
+Input/Output functions
 
 # Pickling and unpickling objects
 
 By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk.
 -/
 
+open Lean
+
 namespace Pantograph
 
 /--
@@ -46,21 +46,6 @@ 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.
 
@@ -71,23 +56,15 @@ 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) (background? : Option Environment := .none)
-  : IO Unit :=
-  pickle path $ distillEnvironment env background?
-
-deriving instance BEq for Import
+def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit :=
+  Pantograph.pickle path (env.header.imports, env.constants.map₂)
 
 def resurrectEnvironment
-  (distilled : DistilledEnvironment)
-  (background? : Option Environment := .none)
+  (imports : Array Import)
+  (map₂ : PHashMap Name ConstantInfo)
   : IO Environment := do
-  let (imports, constArray) := distilled
-  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)
+  let env ← importModules imports {} 0 (loadExts := true)
+  env.replay (Std.HashMap.ofList map₂.toList)
 /--
 Unpickle an `Environment` from disk.
 
@@ -95,10 +72,9 @@ 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) (background? : Option Environment := .none)
-  : IO (Environment × CompactedRegion) := unsafe do
-  let (distilled, region) ← unpickle (Array Import × ConstArray) path
-  return (← resurrectEnvironment distilled background?, region)
+def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
+  let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
+  return (← resurrectEnvironment imports map₂, region)
 
 
 open Lean.Core in
@@ -112,8 +88,7 @@ structure CompactCoreState where
   -- infoState       : Elab.InfoState := {}
 
 @[export pantograph_goal_state_pickle_m]
-def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background? : Option Environment := .none)
-  : IO Unit :=
+def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :=
   let {
     savedState := {
       term := {
@@ -131,8 +106,8 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background
     parentMVars,
     fragments,
   } := goalState
-  pickle path (
-    distillEnvironment env background?,
+  Pantograph.pickle path (
+    env.constants.map₂,
 
     ({ nextMacroScope, ngen } : CompactCoreState),
     meta,
@@ -145,10 +120,10 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background
   )
 
 @[export pantograph_goal_state_unpickle_m]
-def goalStateUnpickle (path : System.FilePath) (background? : Option Environment := .none)
+def goalStateUnpickle (path : System.FilePath) (env : Environment)
     : IO (GoalState × CompactedRegion) := unsafe do
   let ((
-    distilledEnv,
+    map₂,
 
     compactCore,
     meta,
@@ -159,7 +134,7 @@ def goalStateUnpickle (path : System.FilePath) (background? : Option Environment
     parentMVars,
     fragments,
   ), region) ← Pantograph.unpickle (
-    DistilledEnvironment ×
+    PHashMap Name ConstantInfo ×
 
     CompactCoreState ×
     Meta.State ×
@@ -170,7 +145,7 @@ def goalStateUnpickle (path : System.FilePath) (background? : Option Environment
     List MVarId ×
     FragmentMap
   ) path
-  let env ← resurrectEnvironment distilledEnv background?
+  let env ← env.replay (Std.HashMap.ofList map₂.toList)
   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 (background? := .some $ ← getEnv)
+    goalStatePickle goalState args.path
     return {}
   goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do
-    let (goalState, _) ← goalStateUnpickle args.path (background? := .some $ ← getEnv)
+    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
     let id ← newGoalState goalState
     return { id }
 

Test/Common.lean

@@ -187,11 +187,9 @@ namespace Tactic
 
 /-- Create an aux lemma and assigns it to `mvarId`, which is circuitous, but
 exercises the aux lemma generator. -/
-def assignWithAuxLemma (type : Expr) (value? : Option Expr := .none) : Elab.Tactic.TacticM Unit := do
+def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do
   let type ← instantiateMVars type
-  let value ← match value? with
-    | .some value => instantiateMVars value
-    | .none => Meta.mkSorry type (synthetic := false)
+  let value ← instantiateMVars value
   if type.hasExprMVar then
     throwError "Type has expression mvar"
   if value.hasExprMVar then
@@ -202,7 +200,6 @@ def assignWithAuxLemma (type : Expr) (value? : Option Expr := .none) : Elab.Tact
   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,32 +281,6 @@ 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),
@@ -315,7 +289,6 @@ 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,17 +82,18 @@ 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 ← goal.withContext do
+    let (type, value) ← 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) | unreachable!
+      let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable!
+      pure (type, value)
+    let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
     let parentExpr := state1.parentExpr!
-    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)
+    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.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 (·.isAuxLemma)
+    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
 
   return ()