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

@[implicit_reducible, instance 100]

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

@[implicit_reducible]

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

@[inline]

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

theorem Lake.OptDataKind.isAnonymous_iff_name_isAnonymous {α✝ : Type u_1} {k : OptDataKind α✝} : k.isAnonymous = true ↔ (name α✝).isAnonymous = true

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

@[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 Array 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).

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

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

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 target to its output type.

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

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.

@[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.instFamilyDefBuildKeyBuildDataPackageModuleOfFamilyOutNameDataTypeFacetKind {α : Type} {p m : Lean.Name} [FamilyOut DataType Module.facetKind α] : FamilyDef BuildData (BuildKey.packageModule p m) α

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 a new DataType.

@[simp]

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

@[implicit_reducible]

instance Lake.instDataKindUnit : DataKind Unit

instance Lake.instFamilyDefNameDataTypeMkStr1Unit : FamilyDef DataType `unit Unit

@[implicit_reducible]

instance Lake.instDataKindBool : DataKind Bool

@[simp]

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

instance Lake.instFamilyDefNameDataTypeMkStr1Bool : FamilyDef DataType `bool Bool

@[implicit_reducible]

instance Lake.instDataKindFilePath : DataKind System.FilePath

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

@[simp]

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

@[simp]

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

instance Lake.instFamilyDefNameDataTypeMkStr1Dynlib : FamilyDef DataType `dynlib Dynlib

@[implicit_reducible]

instance Lake.instDataKindDynlib : DataKind Dynlib

def Lake.builtinFacetCommand : Lean.ParserDescr

Internal macro for declaring new facet within Lake.

def Lake.facetDataDecl : Lean.ParserDescr

Macro for declaring new FacetData.

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

def Lake.customDataDecl : Lean.ParserDescr

Macro for declaring new CustomData.