Documentation

Lake.Build.Data

Build Data Subtypes #

opaque Lake.DataType (kind : Lean.Name) :

The open type family which maps a Lake data kind to its associated type. For example, LeanLib.facetKind maps to LeanLib.

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

class Lake.OptDataKind (α : Type u) :

Tries to synthesize a Name descriptor of a data type. Otherwise uses Name.anonymous to indicate none was found.

Instances
@[instance 100]
Equations
theorem Lake.OptDataKind.eq_data_type {α : Type u_1} {self : OptDataKind α} (h : ¬self.isAnonymous = true) :
α = DataType (name α)
@[reducible, inline, deprecated Lake.DataType (since := "2025-03-26")]
abbrev Lake.TargetData (kind : Lean.Name) :
Type u_1
Equations
opaque Lake.FacetOut (facet : Lean.Name) :

The open type family which maps a Lake facet to its output type. For example, a FilePath for the module.olean facet.

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

@[reducible, inline]
abbrev Lake.FacetData (kind facet : Lean.Name) :

The open type family which maps a Lake facet kind and name to its output type. For example, a FilePath for the module olean facet.

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

Equations
Instances For
instance Lake.instFamilyDefNameFacetDataOfFacetOutHAppend {kind facet : Lean.Name} {α : Type} [h : FamilyDef FacetOut (kind ++ facet) α] :
FamilyDef (FacetData kind) facet α
instance Lake.instFamilyDefNameFacetOutHAppendOfFacetData {kind facet : Lean.Name} {α : Type} [h : FamilyDef (FacetData kind) facet α] :
FamilyDef FacetOut (kind ++ facet) α
@[reducible, inline]
abbrev Lake.ModuleData (facet : Lean.Name) :

The open type family which maps a module facet's name to its output type. For example, a FilePath for the module olean facet.

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

Equations
@[reducible, inline]
abbrev Lake.PackageData (facet : Lean.Name) :

The open type family which maps a package facet's name to output type. For example, an Arrry Package of direct dependencies for the deps facet.

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

Equations
@[reducible, inline]
abbrev Lake.LibraryData (facet : Lean.Name) :

The open type family which maps a Lean library facet's name to its output type. For example, the FilePath pf the generated static library for the static facet.

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

Equations
@[reducible, inline]
abbrev Lake.LeanLibData (facet : Lean.Name) :

The open type family which maps a Lean library facet's name to its output type. For example, the FilePath pf the generated static library for the static facet.

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

Equations

The open type family which maps a custom package target (package × target name) to its output type.

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

@[reducible, inline]
abbrev Lake.CustomData (package target : Lean.Name) :

The open type family which maps a custom package targetto its output type.

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

Equations
Instances For

Build Data #

Macros for Declaring Build Data #

Macro for declaring new DatayType.

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

Internal macro for declaring new facet within Lake.

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

Macro for declaring new FacetData.

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

Macro for declaring new PackageData.

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

Macro for declaring new ModuleData.

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

Macro for declaring new LibraryData.

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

Macro for declaring new TargetData.

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

Macro for declaring new CustomData.

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