Pickling #95

New Issue

aniva · 2024-09-06T22:38:16-07:00

aniva commented

2024-09-06 22:38:16 -07:00

We should have this wonderful feature, pickling from, REPL:

import REPL.Util.Pickle
import Lean.Replay

open System (FilePath)

namespace Lean.Environment

/--
Pickle an `Environment` to disk.

We only store:
* the list of imports
* the new constants from `Environment.constants`
and when unpickling, we build a fresh `Environment` from the imports,
and then add the new constants.
-/
def pickle (env : Environment) (path : FilePath) : IO Unit :=
  _root_.pickle path (env.header.imports, env.constants.map₂)

/--
Unpickle an `Environment` from disk.

We construct a fresh `Environment` with the relevant imports,
and then replace the new constants.
-/
def unpickle (path : FilePath) : IO (Environment × CompactedRegion) := unsafe do
  let ((imports, map₂), region) ← _root_.unpickle (Array Import × PHashMap Name ConstantInfo) path
  let env ← importModules imports {} 0
  return (← env.replay (HashMap.ofList map₂.toList), region)

end Lean.Environment

We should have this wonderful feature, pickling from, [REPL](https://github.com/leanprover-community/repl/blob/adbbfcb9d4e61c12db96c45d227de92f21cc17dd/REPL/Lean/Environment.lean): ```lean import REPL.Util.Pickle import Lean.Replay open System (FilePath) namespace Lean.Environment /-- Pickle an `Environment` to disk. We only store: * the list of imports * the new constants from `Environment.constants` and when unpickling, we build a fresh `Environment` from the imports, and then add the new constants. -/ def pickle (env : Environment) (path : FilePath) : IO Unit := _root_.pickle path (env.header.imports, env.constants.map₂) /-- Unpickle an `Environment` from disk. We construct a fresh `Environment` with the relevant imports, and then replace the new constants. -/ def unpickle (path : FilePath) : IO (Environment × CompactedRegion) := unsafe do let ((imports, map₂), region) ← _root_.unpickle (Array Import × PHashMap Name ConstantInfo) path let env ← importModules imports {} 0 return (← env.replay (HashMap.ofList map₂.toList), region) end Lean.Environment ```

aniva added the

part/Environment

category

feature

labels 2024-09-06 22:38:16 -07:00

aniva self-assigned this 2024-09-06 22:38:16 -07:00

aniva added this to the 0.3 milestone 2024-09-08 13:48:58 -07:00

aniva added a new dependency 2024-11-14 23:10:49 -08:00

#120 feat: State and environment pickling

aniva modified the milestone from 0.3 to 0.2.21

2024-11-15 23:10:44 -08:00

aniva commented