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.

Equations

• Lake.MonadBuildStore m = Lake.MonadDStore Lake.BuildKey (fun (x : Lake.BuildKey) => Lake.Job (Lake.BuildData x)) m

@[reducible, inline]

abbrev Lake.BuildStore : Type

The type of the Lake build store.

Equations

• Lake.BuildStore = Lake.DRBMap Lake.BuildKey (fun (x : Lake.BuildKey) => Lake.Job (Lake.BuildData x)) Lake.BuildKey.quickCmp

@[inline]

def Lake.BuildStore.empty : BuildStore

Equations

• Lake.BuildStore.empty = Lake.DRBMap.empty

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• self.collectSharedExternLibs = self.collectTargetFacetArray `externLib.shared