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 Lake.BuildData m

@[reducible, inline]

abbrev Lake.BuildStore : Type

The type of the Lake build store.

Equations

• Lake.BuildStore = Lake.DRBMap Lake.BuildKey Lake.BuildData Lake.BuildKey.quickCmp

@[inline]

def Lake.BuildStore.empty : Lake.BuildStore

Equations

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

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

Derive an array of built module facets from the store.

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

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 : Lake.BuildStore) (facet : Lean.Name) [Lake.FamilyOut Lake.PackageData facet α] : Array α

Derive an array of built package facets from the store.

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

Derive an array of built target facets from the store.

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

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

Equations

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