Pantograph/Serial.lean

@@ -101,16 +101,33 @@ 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
   ngen            : NameGenerator  := {}
+  auxDeclNGen     : DeclNameGenerator := {}
   -- traceState      : TraceState     := {}
   -- cache           : Cache     := {}
   -- 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,
+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,11 +136,13 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background
       term := {
         meta := {
           core := {
-            env, nextMacroScope, ngen, ..
+            env, nextMacroScope, ngen, auxDeclNGen, ..
           },
           meta,
         }
-        «elab»,
+        «elab» := «elab»@{
+          syntheticMVars, ..
+        },
       },
       tactic
     }
@@ -131,26 +150,33 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background
     parentMVars,
     fragments,
   } := goalState
-  pickle path (
+  -- Delete `MessageData`s
-    distillEnvironment env background?,
+  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 ({
+    env := distillEnvironment env background?,
 
-    ({ nextMacroScope, ngen } : CompactCoreState),
+    core := ({ nextMacroScope, ngen, auxDeclNGen } : CompactCoreState),
     meta,
-    «elab»,
+    «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 ((
+  let ({
-    distilledEnv,
+    env,
 
-    compactCore,
+    core,
     meta,
     «elab»,
     tactic,
@@ -158,25 +184,14 @@ def goalStateUnpickle (path : System.FilePath) (background? : Option Environment
     root,
     parentMVars,
     fragments,
-  ), region) ← Pantograph.unpickle (
+  }, region) ← Pantograph.unpickle CompactGoalState path
-    DistilledEnvironment ×
+  let env ← resurrectEnvironment env background?
-
-    CompactCoreState ×
-    Meta.State ×
-    Elab.Term.State ×
-    Elab.Tactic.State ×
-
-    MVarId ×
-    List MVarId ×
-    FragmentMap
-  ) path
-  let env ← resurrectEnvironment distilledEnv background?
   let goalState := {
     savedState := {
       term := {
         meta := {
           core := {
-            compactCore with
+            core with
             passedHeartbeats := 0,
             env,
           },

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))