Build Data Subtypes

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

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.DataKind (α : Type u) : Type

A Name descriptor of a data type.

• name : Lean.Name

  The name which describes α.

• wf : ¬(name α).isAnonymous = true ∧ α = DataType (name α)

  Proof that α is the data type described by name.

class Lake.OptDataKind (α : Type u) : Type

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

• name : Lean.Name

  The name which describes α (or Name.anonymous if none).

• wf (h : ¬(name α).isAnonymous = true) : α = DataType (name α)

  Proof that α is the data type described by name (if valid).

@[instance 100]

instance Lake.OptDataKind.anonymous {α : Type u_1} : OptDataKind α

Equations

• Lake.OptDataKind.anonymous = { name := Lean.Name.anonymous, wf := ⋯ }

instance Lake.instInhabitedOptDataKind {α : Type u_1} : Inhabited (OptDataKind α)

Equations

• Lake.instInhabitedOptDataKind = { default := Lake.OptDataKind.anonymous }

@[inline]

def Lake.OptDataKind.isAnonymous {α : Type u_1} (self : OptDataKind α) : Bool

Equations

• self.isAnonymous = (Lake.OptDataKind.name α).isAnonymous

theorem Lake.OptDataKind.eq_data_type {α : Type u_1} {self : OptDataKind α} (h : ¬self.isAnonymous = true) : α = DataType (name α)

instance Lake.instOptDataKindOfDataKind {α : Type u_1} [DataKind α] : OptDataKind α

Equations

• Lake.instOptDataKindOfDataKind = { name := Lake.DataKind.name α, wf := ⋯ }

instance Lake.instCoeOutOptDataKindName {α : Type u_1} : CoeOut (OptDataKind α) Lean.Name

Equations

• Lake.instCoeOutOptDataKindName = { coe := fun (x : Lake.OptDataKind α) => Lake.OptDataKind.name α }

instance Lake.instToStringOptDataKind {α : Type u_1} : ToString (OptDataKind α)

Equations

• Lake.instToStringOptDataKind = { toString := fun (x : Lake.OptDataKind α) => (Lake.OptDataKind.name α).toString }

@[reducible, inline, deprecated Lake.DataType (since := "2025-03-26")]

abbrev Lake.TargetData (kind : Lean.Name) : Type u_1

Equations

• Lake.TargetData = Lake.DataType

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

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) : Type

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

• Lake.FacetData kind facet = Lake.FacetOut (kind ++ facet)

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) : Type

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

• Lake.ModuleData = Lake.FacetData Lake.Module.facetKind

@[reducible, inline]

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

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

• Lake.PackageData = Lake.FacetData Lake.Package.facetKind

@[reducible, inline]

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

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

• Lake.LibraryData = Lake.FacetData Lake.LeanLib.facetKind

@[reducible, inline]

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

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

• Lake.LeanLibData = Lake.LibraryData

opaque Lake.CustomOut (target : Lean.Name × Lean.Name) : Type

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) : Type

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

• Lake.CustomData package target = Lake.CustomOut (package, target)

instance Lake.instFamilyDefNameCustomDataOfProdCustomOutMk {p t : Lean.Name} {α : Type} [h : FamilyDef CustomOut (p, t) α] : FamilyDef (CustomData p) t α

Build Data

@[reducible, inline]

abbrev Lake.BuildData : 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.module module) = Lake.DataType Lake.Module.facetKind
• Lake.BuildData (Lake.BuildKey.package package) = Lake.DataType Lake.Package.facetKind
• Lake.BuildData (Lake.BuildKey.packageTarget p t) = Lake.CustomData p t
• Lake.BuildData (target.facet f) = Lake.FacetOut f

@[instance 100]

instance Lake.instFamilyDefBuildKeyBuildDataPackageTargetCustomData {p t : Lean.Name} : FamilyDef BuildData (BuildKey.packageTarget p t) (CustomData p t)

@[instance 100]

instance Lake.instFamilyDefBuildKeyBuildDataFacetFacetOut {t : BuildKey} {f : Lean.Name} : FamilyDef BuildData (t.facet f) (FacetOut f)

instance Lake.instFamilyDefBuildKeyBuildDataPackageTargetOfFamilyOutNameCustomData {p t : Lean.Name} {α : Type} [FamilyOut (CustomData p) t α] : FamilyDef BuildData (BuildKey.packageTarget p t) α

instance Lake.instFamilyDefBuildKeyBuildDataModuleOfFamilyOutNameDataTypeFacetKind {α : Type} {k : Lean.Name} [FamilyOut DataType Module.facetKind α] : FamilyDef BuildData (BuildKey.module k) α

instance Lake.instFamilyDefBuildKeyBuildDataPackageOfFamilyOutNameDataTypeFacetKind {α : Type} {k : Lean.Name} [FamilyOut DataType Package.facetKind α] : FamilyDef BuildData (BuildKey.package k) α

Macros for Declaring Build Data

def Lake.dataTypeDecl : Lean.ParserDescr

Macro for declaring new DatayType.

Equations

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

instance Lake.instDataKindUnit : DataKind Unit

Equations

• Lake.instDataKindUnit = { name := `unit, wf := Lake.instDataKindUnit._proof_1 }

instance Lake.instFamilyDefNameDataTypeMkStr1Unit : FamilyDef DataType `unit Unit

@[simp]

axiom Lake.DataType.unit : DataType `unit = Unit

@[simp]

axiom Lake.DataType.bool : DataType `bool = Bool

instance Lake.instFamilyDefNameDataTypeMkStr1Bool : FamilyDef DataType `bool Bool

instance Lake.instDataKindBool : DataKind Bool

Equations

• Lake.instDataKindBool = { name := `bool, wf := Lake.instDataKindBool._proof_1 }

instance Lake.instDataKindFilePath : DataKind System.FilePath

Equations

• Lake.instDataKindFilePath = { name := `filepath, wf := Lake.instDataKindFilePath._proof_1 }

@[simp]

axiom Lake.DataType.filepath : DataType `filepath = System.FilePath

instance Lake.instFamilyDefNameDataTypeMkStr1FilePath : FamilyDef DataType `filepath System.FilePath

instance Lake.instFamilyDefNameDataTypeMkStr1Dynlib : FamilyDef DataType `dynlib Dynlib

@[simp]

axiom Lake.DataType.dynlib : DataType `dynlib = Dynlib

instance Lake.instDataKindDynlib : DataKind Dynlib

Equations

• Lake.instDataKindDynlib = { name := `dynlib, wf := Lake.instDataKindDynlib._proof_1 }

def Lake.builtinFacetCommand : Lean.ParserDescr

Internal macro for declaring new facet within Lake.

Equations

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

def Lake.facetDataDecl : Lean.ParserDescr

Macro for declaring new FacetData.

Equations

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

def Lake.packageDataDecl : Lean.ParserDescr

Macro for declaring new PackageData.

Equations

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

def Lake.moduleDataDecl : Lean.ParserDescr

Macro for declaring new ModuleData.

Equations

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

def Lake.libraryDataDecl : Lean.ParserDescr

Macro for declaring new LibraryData.

Equations

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

def Lake.targetDataDecl : Lean.ParserDescr

Macro for declaring new TargetData.

Equations

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

def Lake.customDataDecl : Lean.ParserDescr

Macro for declaring new CustomData.

Equations

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