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).

@[inline, reducible]

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

A monad equipped with a Lake build store.

@[inline, reducible]

abbrev Lake.BuildStore : Type

The type of the Lake build store.

@[inline]

def Lake.BuildStore.empty : Lake.BuildStore

def Lake.BuildStore.collectModuleFacetArray {α : Type} (self : Lake.BuildStore) (facet : Lake.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 : Lake.Name) [Lake.FamilyOut Lake.ModuleData facet α] : Lake.NameMap α

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

def Lake.BuildStore.collectPackageFacetArray {α : Type} (self : Lake.BuildStore) (facet : Lake.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 : Lake.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.