Pickling and unpickling objects

By abusing saveModuleData and readModuleData we can pickle and unpickle objects to disk.

def pickle {α : Type} (path : System.FilePath) (x : α) (key : Lean.Name := by exact decl_name%) : IO Unit

Save an object to disk. If you need to write multiple objects from within a single declaration, you will need to provide a unique key for each.

Equations

• pickle path x key = Lean.saveModuleData path key (pickle.unsafe_impl_1 x)

unsafe def unpickle (α : Type) (path : System.FilePath) : IO (α × Lean.CompactedRegion)

Load an object from disk. Note: The returned CompactedRegion can be used to free the memory behind the value of type α, using CompactedRegion.free (which is only safe once all references to the α are released). Ignoring the CompactedRegion results in the data being leaked. Use withUnpickle to call CompactedRegion.free automatically.

This function is unsafe because the data being loaded may not actually have type α, and this may cause crashes or other bad behavior.

Equations

• unpickle α path = do let __discr ← Lean.readModuleData path match __discr with | (x, region) => pure (unsafeCast x, region)

unsafe def withUnpickle {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] {α β : Type} (path : System.FilePath) (f : α → m β) : m β

Load an object from disk and run some continuation on it, freeing memory afterwards.

Equations

• withUnpickle path f = do let __discr ← liftM (unpickle α path) match __discr with | (x, region) => do let r ← f x liftM region.free pure r