fix: workaround for Meta.Context.config private (#64)

leanprover-community · Jan 8, 2025 · ad380d5 · ad380d5
1 parent ddca959
commit ad380d5
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
@@ -259,13 +259,14 @@ When pickling the `Environment`, we do so relative to its imports.
 def pickle (p : ProofSnapshot) (path : FilePath) : IO Unit := do
   let env := p.coreState.env
   let p' := { p with coreState := { p.coreState with env := ← mkEmptyEnvironment }}
+  let (cfg, _) ← Lean.Meta.getConfig.toIO p'.coreContext p'.coreState p'.metaContext p'.metaState
   _root_.pickle path
     (env.header.imports,
      env.constants.map₂,
      ({ p'.coreState with } : CompactableCoreState),
      p'.coreContext,
      p'.metaState,
-     ({ p'.metaContext with } : CompactableMetaContext),
+     ({ p'.metaContext with config := cfg } : CompactableMetaContext),
      p'.termState,
      ({ p'.termContext with } : CompactableTermContext),
      p'.tacticState,