From e3b62dfeecf1473795942c983aba62b922c647b2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 13 Jul 2025 17:06:06 -0700 Subject: [PATCH 1/4] fix(serial): Pickle synthetic mvars --- Pantograph/Serial.lean | 12 ++++++++++-- Test/Serial.lean | 16 ++++++++++++++++ 2 files changed, 26 insertions(+), 2 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index ff82752..c81bd11 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -123,7 +123,9 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background }, meta, } - «elab», + «elab» := «elab»@{ + syntheticMVars, .. + }, }, tactic } @@ -131,12 +133,18 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background parentMVars, fragments, } := goalState + let syntheticMVars : MVarIdMap _ := syntheticMVars.fold (init := .empty) λ acc key val => + let kind := match val.kind with + | .typeClass _ => .typeClass .none + | .coe header? expectedType e f? _ => .coe header? expectedType e f? .none + | k => k + acc.insert key { val with kind } pickle path ( distillEnvironment env background?, ({ nextMacroScope, ngen } : CompactCoreState), meta, - «elab», + { «elab» with syntheticMVars }, tactic, root, diff --git a/Test/Serial.lean b/Test/Serial.lean index 05bbc0e..3e437be 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -96,6 +96,21 @@ def test_pickling_env_extensions : TestM Unit := do return () +/-- Synthetic mvars in this case creates closures. These cannot be pickled. -/ +def test_pickling_synthetic_mvars : TestM Unit := do + let coreSrc : Core.State := { env := ← getEnv } + IO.FS.withTempFile λ _ statePath => do + let stateGenerate : MetaM GoalState := runTermElabMInMeta do + let type ← Elab.Term.elabTerm (← `(term|(0 : Nat) < 1)) .none + let state ← GoalState.create type + let .success state _ ← state.tryHave .unfocus "h" "0 < 2" | unreachable! + assert! state.savedState.term.elab.syntheticMVars.size > 0 + return state + + let ((), _) ← runCoreM coreSrc do + let state ← stateGenerate.run' + goalStatePickle state statePath + structure Test where name : String routine: TestM Unit @@ -115,6 +130,7 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) := let tests: List Test := [ { name := "environment", routine := test_pickling_environment, }, { name := "goal simple", routine := test_goal_state_simple, }, + { name := "goal synthetic mvars", routine := test_pickling_synthetic_mvars, }, { name := "extensions", routine := test_pickling_env_extensions, }, ] tests.map (fun test => (test.name, test.run env)) From e58becd14ade3ebff19cff8cf8f1cc21b7aaf8d1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 13 Jul 2025 17:10:39 -0700 Subject: [PATCH 2/4] fix(serial): Pickle the `AuxDeclNGen` --- Pantograph/Serial.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index c81bd11..a7ae3d0 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -106,11 +106,17 @@ structure CompactCoreState where -- env : Environment nextMacroScope : MacroScope := firstFrontendMacroScope + 1 ngen : NameGenerator := {} + auxDeclNGen : DeclNameGenerator := {} -- traceState : TraceState := {} -- cache : Cache := {} -- messages : MessageLog := {} -- infoState : Elab.InfoState := {} +/-- Pickles a goal state by taking its diff relative to a background +environment. This function eliminates all `MessageData` from synthetic +metavariables, because these `MessageData` objects frequently carry closures, +which cannot be pickled. If there is no synthetic metavariable, this would not +cause a difference. -/ @[export pantograph_goal_state_pickle_m] def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background? : Option Environment := .none) : IO Unit := @@ -119,7 +125,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background term := { meta := { core := { - env, nextMacroScope, ngen, .. + env, nextMacroScope, ngen, auxDeclNGen, .. }, meta, } @@ -133,6 +139,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background parentMVars, fragments, } := goalState + -- Delete `MessageData`s let syntheticMVars : MVarIdMap _ := syntheticMVars.fold (init := .empty) λ acc key val => let kind := match val.kind with | .typeClass _ => .typeClass .none @@ -142,7 +149,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background pickle path ( distillEnvironment env background?, - ({ nextMacroScope, ngen } : CompactCoreState), + ({ nextMacroScope, ngen, auxDeclNGen } : CompactCoreState), meta, { «elab» with syntheticMVars }, tactic, From b101806c92d776926227239568e3638e1dbc88db Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 13 Jul 2025 17:12:24 -0700 Subject: [PATCH 3/4] doc: Add description for `CompactCoreState` --- Pantograph/Serial.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index a7ae3d0..a06c89c 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -101,7 +101,7 @@ def environmentUnpickle (path : System.FilePath) (background? : Option Environme return (← resurrectEnvironment distilled background?, region) -open Lean.Core in +/-- `CoreM`'s state, with information irrelevant to pickling masked out -/ structure CompactCoreState where -- env : Environment nextMacroScope : MacroScope := firstFrontendMacroScope + 1 From fc4d7397d7639d1c315fcda4bb25bc14c70bcf5d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 13 Jul 2025 17:16:46 -0700 Subject: [PATCH 4/4] refactor(serial): Use `structure` instead of tuple --- Pantograph/Serial.lean | 44 +++++++++++++++++++++--------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index a06c89c..63da99c 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -112,6 +112,17 @@ structure CompactCoreState where -- messages : MessageLog := {} -- infoState : Elab.InfoState := {} +structure CompactGoalState where + env : DistilledEnvironment + + core : CompactCoreState + meta : Meta.State + «elab»: Elab.Term.State + tactic: Elab.Tactic.State + root: MVarId + parentMVars: List MVarId + fragments: FragmentMap + /-- Pickles a goal state by taking its diff relative to a background environment. This function eliminates all `MessageData` from synthetic metavariables, because these `MessageData` objects frequently carry closures, @@ -146,26 +157,26 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background | .coe header? expectedType e f? _ => .coe header? expectedType e f? .none | k => k acc.insert key { val with kind } - pickle path ( - distillEnvironment env background?, + pickle path ({ + env := distillEnvironment env background?, - ({ nextMacroScope, ngen, auxDeclNGen } : CompactCoreState), + core := ({ nextMacroScope, ngen, auxDeclNGen } : CompactCoreState), meta, - { «elab» with syntheticMVars }, + «elab» := { «elab» with syntheticMVars }, tactic, root, parentMVars, fragments, - ) + } : CompactGoalState) @[export pantograph_goal_state_unpickle_m] def goalStateUnpickle (path : System.FilePath) (background? : Option Environment := .none) : IO (GoalState × CompactedRegion) := unsafe do - let (( - distilledEnv, + let ({ + env, - compactCore, + core, meta, «elab», tactic, @@ -173,25 +184,14 @@ def goalStateUnpickle (path : System.FilePath) (background? : Option Environment root, parentMVars, fragments, - ), region) ← Pantograph.unpickle ( - DistilledEnvironment × - - CompactCoreState × - Meta.State × - Elab.Term.State × - Elab.Tactic.State × - - MVarId × - List MVarId × - FragmentMap - ) path - let env ← resurrectEnvironment distilledEnv background? + }, region) ← Pantograph.unpickle CompactGoalState path + let env ← resurrectEnvironment env background? let goalState := { savedState := { term := { meta := { core := { - compactCore with + core with passedHeartbeats := 0, env, },