Build Info

This module defines the Lake build info type and related utilities. Build info is what is the data passed to a Lake build function to facilitate the build.

inductive Lake.BuildInfo : Type

The type of Lake's build info.

• target (package : Package) (target : Lean.Name) : BuildInfo
• facet (target : BuildKey) (kind : Lean.Name) (data : DataType kind) (facet : Lean.Name) : BuildInfo

Build Info & Keys

Build Key Helper Constructors

@[reducible, inline]

abbrev Lake.Package.key (self : Package) : BuildKey

@[reducible, inline]

abbrev Lake.Package.targetKey (target : Lean.Name) (self : Package) : BuildKey

Build Info to Key

@[reducible]

def Lake.BuildInfo.key (self : BuildInfo) : BuildKey

The key that identifies the build in the Lake build store.

instance Lake.instToStringBuildInfo : ToString BuildInfo

Instances for deducing data types of BuildInfo keys

@[instance 100]

instance Lake.instFamilyDefBuildKeyBuildDataCustomTargetKeyNameCustomData {n t : Lean.Name} {p : NPackage n} : FamilyDef BuildData (BuildKey.customTarget p.keyName t) (CustomData n t)

instance Lake.instFamilyDefBuildKeyBuildDataKeyTargetOfFamilyOutNameCustomData {n t : Lean.Name} {α : Type} {p : NPackage n} [FamilyOut (CustomData n) t α] : FamilyDef BuildData (BuildInfo.target p.toPackage t).key α

instance Lake.instFamilyDefBuildKeyBuildDataKeyTargetOfFamilyOutPackageTarget {n t : Lean.Name} {α : Type} {p : NPackage n} [FamilyOut BuildData (BuildKey.packageTarget n t) α] : FamilyDef BuildData (BuildInfo.target p.toPackage t).key α

instance Lake.instFamilyDefBuildKeyBuildDataKeyFacetOfFamilyOutNameFacetOut {f : Lean.Name} {α : Type} {t : BuildKey} {k : Lean.Name} {d : DataType k} [FamilyOut FacetOut f α] : FamilyDef BuildData (BuildInfo.facet t k d f).key α