def Lean.CompactedRegion : Type

A compacted region holds multiple Lean objects in a contiguous memory region, which can be read/written to/from disk. Objects inside the region do not have reference counters and cannot be freed individually. The contents of .olean files are compacted regions.

Equations

• Lean.CompactedRegion = USize

@[extern lean_compacted_region_is_memory_mapped]

opaque Lean.CompactedRegion.isMemoryMapped : CompactedRegion → Bool

@[extern lean_compacted_region_size]

opaque Lean.CompactedRegion.size : CompactedRegion → USize

Size in bytes.

@[extern lean_compacted_region_free]

unsafe opaque Lean.CompactedRegion.free : CompactedRegion → IO Unit

Frees a compacted region and its contents. No live references to the contents may exist at the time of invocation.

def Lean.Compactor : Type

Holds an opaque compactor handle returned by CompactedRegion.save, used to chain subsequent saves so that objects shared between parts are emitted exactly once.

Not thread-safe: a Compactor value must not be used concurrently from multiple threads. The CompactedRegions passed as depRegions when the Compactor was first created must outlive the Compactor; if any are freed (via CompactedRegion.free) while the Compactor is still in use, subsequent saves will dereference dangling pointers.

Equations

• Lean.Compactor = Lean.CompactorSpec✝.type

@[extern lean_compacted_region_save]

unsafe opaque Lean.CompactedRegion.save {α : Type} (fname : System.FilePath) (key : Name) (data : α) (depRegions : Array CompactedRegion) (prev : Option Compactor) : IO Compactor

Saves arbitrary data to a compacted region on disk.

The α type parameter is erased at the runtime/extern boundary: the compactor walks the live object graph rooted at data regardless of its Lean type. α is purely a hint for the caller to align save and load sites. Mismatched types between save and load yield undefined behavior on use.

key is hashed to derive a deterministic mmap base address; for module saves, pass the module Name. depRegions are loaded compacted regions (typically from imports) whose objects should not be re-serialized. prev, when present, likewise allows for reuse of objects from prior saves in the same session.

Returns a Compactor that may be passed as prev to subsequent saves. Unsafe because the returned Compactor carries thread-safety and depRegions lifetime contracts the type system cannot enforce; see Compactor.

@[extern lean_compacted_region_read]

unsafe opaque Lean.CompactedRegion.read {α : Type} (fname : System.FilePath) (depRegions : Array CompactedRegion) : IO (α × CompactedRegion)

Reads a compacted region from disk.

depRegions are existing compacted regions whose address ranges are needed for cross-region pointer fixup. The result is the root object reinterpreted at type α paired with the new CompactedRegion. Unsafe because α is type-erased at the extern boundary: it is the caller's responsibility to ensure α matches the type the data was saved at; mismatched types yield undefined behavior on use.