Lake.Build.Data

Build Data Subtypes #

opaque Lake.ModuleData (facet : Lake.Name) :

The open type family which maps a module facet's name to its build data in the Lake build store. For example, a transitive × direct import pair for the lean.imports facet or an active build target for lean.c.

It is an open type, meaning additional mappings can be add lazily as needed (via module_data).

source

opaque Lake.PackageData (facet : Lake.Name) :

Type

The open type family which maps a package facet's name to its build data in the Lake build store. For example, a transitive dependencies of the package for the facet deps.

It is an open type, meaning additional mappings can be add lazily as needed (via package_data).

source

opaque Lake.TargetData (facet : Lake.Name) :

Type

The open type family which maps a (builtin) Lake target's (e.g., extern_lib) facet to its associated build data. For example, an active build target for the externLib.static facet.

It is an open type, meaning additional mappings can be add lazily as needed (via target_data).

source

@[inline, reducible]

abbrev Lake.LibraryData (facet : Lake.Name) :

Type

Instances For

source

instance Lake.instFamilyDefNameTargetDataHAppendInstHAppendInstAppendNameMkStr1 {facet : Lake.Name} {α : Type} [h : Lake.FamilyOut Lake.LibraryData facet α] :

Lake.FamilyDef Lake.TargetData (`leanLib ++ facet) α

source

instance Lake.instFamilyDefNameLibraryData {facet : Lake.Name} {α : Type} [h : Lake.FamilyOut Lake.TargetData (`leanLib ++ facet) α] :

Lake.FamilyDef Lake.LibraryData facet α

source

opaque Lake.CustomData (target : Lake.Name × Lake.Name) :

Type

The open type family which maps a custom target (package × target name) to its build data in the Lake build store.

It is an open type, meaning additional mappings can be add lazily as needed (via custom_data).

Build Data #

source

@[inline, reducible]

abbrev Lake.BuildData :

Lake.BuildKey → Type

A mapping between a build key and its associated build data in the store. It is a simple type function composed of the separate open type families for modules facets, package facets, Lake target facets, and custom targets.

Instances For

source

instance Lake.instFamilyDefBuildKeyBuildDataModuleFacetModuleData {m : Lake.Name} {f : Lake.Name} :

Lake.FamilyDef Lake.BuildData (Lake.BuildKey.moduleFacet m f) (Lake.ModuleData f)

source

instance Lake.instFamilyDefBuildKeyBuildDataPackageFacetPackageData {p : Lake.Name} {f : Lake.Name} :

Lake.FamilyDef Lake.BuildData (Lake.BuildKey.packageFacet p f) (Lake.PackageData f)

source