Build Data Subtypes

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

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

opaque Lake.PackageData (facet : Lean.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).

opaque Lake.TargetData (facet : Lean.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).

@[reducible, inline]

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

Equations

• Lake.LibraryData facet = Lake.TargetData (`leanLib ++ facet)

theorem Lake.instFamilyDefNameTargetDataHAppendMkStr1OfFamilyOutLibraryData {facet : Lean.Name} {α : Type} [h : Lake.FamilyOut Lake.LibraryData facet α] : Lake.FamilyDef Lake.TargetData (`leanLib ++ facet) α

theorem Lake.instFamilyDefNameLibraryDataOfFamilyOutTargetDataHAppendMkStr1 {facet : Lean.Name} {α : Type} [h : Lake.FamilyOut Lake.TargetData (`leanLib ++ facet) α] : Lake.FamilyDef Lake.LibraryData facet α

opaque Lake.CustomData (target : Lean.Name × Lean.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

@[reducible, inline]

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.

Equations

• Lake.BuildData (Lake.BuildKey.moduleFacet module f) = Lake.ModuleData f
• Lake.BuildData (Lake.BuildKey.packageFacet package f) = Lake.PackageData f
• Lake.BuildData (Lake.BuildKey.targetFacet package target f) = Lake.TargetData f
• Lake.BuildData (Lake.BuildKey.customTarget p t) = Lake.CustomData (p, t)

theorem Lake.instFamilyDefBuildKeyBuildData {k : Lake.BuildKey} : Lake.FamilyDef Lake.BuildData k (Lake.BuildData k)

theorem Lake.instFamilyDefBuildKeyBuildDataModuleFacetModuleData {m f : Lean.Name} : Lake.FamilyDef Lake.BuildData (Lake.BuildKey.moduleFacet m f) (Lake.ModuleData f)

theorem Lake.instFamilyDefBuildKeyBuildDataPackageFacetPackageData {p f : Lean.Name} : Lake.FamilyDef Lake.BuildData (Lake.BuildKey.packageFacet p f) (Lake.PackageData f)

theorem Lake.instFamilyDefBuildKeyBuildDataTargetFacetTargetData {p t f : Lean.Name} : Lake.FamilyDef Lake.BuildData (Lake.BuildKey.targetFacet p t f) (Lake.TargetData f)

theorem Lake.instFamilyDefBuildKeyBuildDataCustomTargetCustomDataMkName {p t : Lean.Name} : Lake.FamilyDef Lake.BuildData (Lake.BuildKey.customTarget p t) (Lake.CustomData (p, t))

Macros for Declaring Build Data

def Lake.packageDataDecl : Lean.ParserDescr

Macro for declaring new PackageData.

def Lake.moduleDataDecl : Lean.ParserDescr

Macro for declaring new ModuleData.

def Lake.libraryDataDecl : Lean.ParserDescr

Macro for declaring new TargetData for libraries.

Equations

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

def Lake.targetDataDecl : Lean.ParserDescr

Macro for declaring new TargetData.

def Lake.customDataDecl : Lean.ParserDescr

Macro for declaring new CustomData.

Equations

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