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,

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