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 : autoParam Lean.Name _auto✝) :

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.

Instances For
    unsafe def unpickle (α : Type) (path : System.FilePath) :

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

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

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

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

      Instances For