The Lake Build Store

The Lake build store is the map of Lake build keys to build task and/or build results that is slowly filled during a recursive build (e.g., via topological-based build of an initial key's dependencies).

@[reducible, inline]

abbrev Lake.MonadBuildStore (m : Type → Type u_1) : Type u_1

A monad equipped with a Lake build store.

@[reducible, inline]

abbrev Lake.BuildStore : Type

The type of the Lake build store.

@[inline]

def Lake.BuildStore.empty : BuildStore

def Lake.BuildStore.collectModuleFacetArray {α : Type} (self : BuildStore) (facet : Lean.Name) [FamilyOut FacetOut facet α] : Array (Job α)

Derive an array of built module facets from the store.

def Lake.BuildStore.collectModuleFacetMap {α : Type} (self : BuildStore) (facet : Lean.Name) [FamilyOut FacetOut facet α] : Lean.NameMap (Job α)

Derive a map of module names to built facets from the store.

def Lake.BuildStore.collectPackageFacetArray {α : Type} (self : BuildStore) (facet : Lean.Name) [FamilyOut FacetOut facet α] : Array (Job α)

Derive an array of built package facets from the store.

def Lake.BuildStore.collectTargetFacetArray {α : Type} (self : BuildStore) (facet : Lean.Name) [FamilyOut FacetOut facet α] : Array (Job α)

Derive an array of built target facets from the store.

def Lake.BuildStore.collectSharedExternLibs {α : Type} (self : BuildStore) [FamilyOut FacetOut `externLib.shared α] : Array (Job α)

Derive an array of built external shared libraries from the store.