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

Equations

• self.key = Lake.BuildKey.package self.name

@[reducible, inline, deprecated Lake.Package.key (since := "2025-03-28")]

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

Equations

• self.buildKey = Lake.BuildKey.package self.name

@[reducible, inline, deprecated Lake.BuildKey.facet (since := "2025-03-28")]

abbrev Lake.Package.facetBuildKey (facet : Lean.Name) (self : Package) : BuildKey

Equations

• Lake.Package.facetBuildKey facet self = self.key.facet facet

@[reducible, inline]

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

Equations

• Lake.Package.targetKey target self = Lake.BuildKey.packageTarget self.name target

@[reducible, inline, deprecated Lake.Package.targetKey (since := "2025-03-28")]

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

Equations

• Lake.Package.targetBuildKey target self = Lake.BuildKey.packageTarget self.name target

Build Info to Key

@[reducible]

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

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

Equations

• (Lake.BuildInfo.target p t).key = Lake.Package.targetKey t p
• (Lake.BuildInfo.facet t kind data f).key = t.facet f

instance Lake.instToStringBuildInfo : ToString BuildInfo

Equations

• Lake.instToStringBuildInfo = { toString := fun (x : Lake.BuildInfo) => toString x.key }

Instances for deducing data types of BuildInfo keys

@[instance 100]

instance Lake.instFamilyDefBuildKeyBuildDataCustomTargetNameCustomData {n t : Lean.Name} {p : NPackage n} : FamilyDef BuildData (BuildKey.customTarget p.name 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 α