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.

• moduleFacet: Lake.Module → Lean.Name → Lake.BuildInfo
• packageFacet: Lake.Package → Lean.Name → Lake.BuildInfo
• libraryFacet: Lake.LeanLib → Lean.Name → Lake.BuildInfo
• leanExe: Lake.LeanExe → Lake.BuildInfo
• staticExternLib: Lake.ExternLib → Lake.BuildInfo
• sharedExternLib: Lake.ExternLib → Lake.BuildInfo
• dynlibExternLib: Lake.ExternLib → Lake.BuildInfo
• target: Lake.Package → Lean.Name → Lake.BuildInfo

Build Info & Keys

Build Key Helper Constructors

@[reducible, inline]

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

Equations

• Lake.Module.facetBuildKey facet self = Lake.BuildKey.moduleFacet self.keyName facet

@[reducible, inline]

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

Equations

• Lake.Package.facetBuildKey facet self = Lake.BuildKey.packageFacet self.name facet

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• self.facetBuildKey facet = Lake.BuildKey.targetFacet self.pkg.name self.name (`leanLib ++ facet)

@[reducible, inline]

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

Equations

• self.buildKey = Lake.BuildKey.targetFacet self.pkg.name self.name Lake.LeanExe.exeFacet

@[reducible, inline]

abbrev Lake.ExternLib.staticBuildKey (self : Lake.ExternLib) : Lake.BuildKey

Equations

• self.staticBuildKey = Lake.BuildKey.targetFacet self.pkg.name self.name Lake.ExternLib.staticFacet

@[reducible, inline]

abbrev Lake.ExternLib.sharedBuildKey (self : Lake.ExternLib) : Lake.BuildKey

Equations

• self.sharedBuildKey = Lake.BuildKey.targetFacet self.pkg.name self.name Lake.ExternLib.sharedFacet

@[reducible, inline]

abbrev Lake.ExternLib.dynlibBuildKey (self : Lake.ExternLib) : Lake.BuildKey

Equations

• self.dynlibBuildKey = Lake.BuildKey.targetFacet self.pkg.name self.name Lake.ExternLib.dynlibFacet

Build Info to Key

@[reducible]

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

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

Equations

• (Lake.BuildInfo.moduleFacet m f).key = Lake.Module.facetBuildKey f m
• (Lake.BuildInfo.packageFacet p f).key = Lake.Package.facetBuildKey f p
• (Lake.BuildInfo.libraryFacet l f).key = l.facetBuildKey f
• (Lake.BuildInfo.leanExe x_1).key = x_1.buildKey
• (Lake.BuildInfo.staticExternLib l).key = l.staticBuildKey
• (Lake.BuildInfo.sharedExternLib l).key = l.sharedBuildKey
• (Lake.BuildInfo.dynlibExternLib l).key = l.dynlibBuildKey
• (Lake.BuildInfo.target p t).key = Lake.Package.targetBuildKey t p

Instances for deducing data types of BuildInfo keys

instance Lake.instFamilyDefBuildKeyBuildDataKeyModuleFacetOfFamilyOutNameModuleData {f : Lean.Name} {α : Type} {m : Lake.Module} [Lake.FamilyOut Lake.ModuleData f α] : Lake.FamilyDef Lake.BuildData (Lake.BuildInfo.moduleFacet m f).key α

Equations

• ⋯ = ⋯

instance Lake.instFamilyDefBuildKeyBuildDataKeyPackageFacetOfFamilyOutNamePackageData {f : Lean.Name} {α : Type} {p : Lake.Package} [Lake.FamilyOut Lake.PackageData f α] : Lake.FamilyDef Lake.BuildData (Lake.BuildInfo.packageFacet p f).key α

Equations

• ⋯ = ⋯

@[instance 100]

instance Lake.instFamilyDefBuildKeyBuildDataCustomTargetNameCustomDataMkName {n t : Lean.Name} {p : Lake.NPackage n} : Lake.FamilyDef Lake.BuildData (Lake.BuildKey.customTarget p.name t) (Lake.CustomData (n, t))

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Lake.instFamilyDefBuildKeyBuildDataKeyLibraryFacetOfFamilyOutNameTargetDataHAppendMkStr1 {f : Lean.Name} {α : Type} {l : Lake.LeanLib} [Lake.FamilyOut Lake.TargetData (`leanLib ++ f) α] : Lake.FamilyDef Lake.BuildData (Lake.BuildInfo.libraryFacet l f).key α

Equations

• ⋯ = ⋯

instance Lake.instFamilyDefBuildKeyBuildDataKeyLeanExeOfFamilyOutNameTargetDataExeFacet {α : Type} {x : Lake.LeanExe} [Lake.FamilyOut Lake.TargetData Lake.LeanExe.exeFacet α] : Lake.FamilyDef Lake.BuildData (Lake.BuildInfo.leanExe x).key α

Equations

• ⋯ = ⋯

instance Lake.instFamilyDefBuildKeyBuildDataKeyStaticExternLibOfFamilyOutNameTargetDataStaticFacet {α : Type} {l : Lake.ExternLib} [Lake.FamilyOut Lake.TargetData Lake.ExternLib.staticFacet α] : Lake.FamilyDef Lake.BuildData (Lake.BuildInfo.staticExternLib l).key α

Equations

• ⋯ = ⋯

instance Lake.instFamilyDefBuildKeyBuildDataKeySharedExternLibOfFamilyOutNameTargetDataSharedFacet {α : Type} {l : Lake.ExternLib} [Lake.FamilyOut Lake.TargetData Lake.ExternLib.sharedFacet α] : Lake.FamilyDef Lake.BuildData (Lake.BuildInfo.sharedExternLib l).key α

Equations

• ⋯ = ⋯

instance Lake.instFamilyDefBuildKeyBuildDataKeyDynlibExternLibOfFamilyOutNameTargetDataDynlibFacet {α : Type} {l : Lake.ExternLib} [Lake.FamilyOut Lake.TargetData Lake.ExternLib.dynlibFacet α] : Lake.FamilyDef Lake.BuildData (Lake.BuildInfo.dynlibExternLib l).key α

Equations

• ⋯ = ⋯

Build Info & Facets

Complex Builtin Facet Declarations

Additional builtin facets missing from Build.Facets. These are defined here because they need configuration definitions (e.g., Module), whereas the facets there are needed by the configuration definitions.

@[reducible, inline]

abbrev Lake.Module.importsFacet : Lean.Name

The direct local imports of the Lean module.

Equations

• Lake.Module.importsFacet = `lean.imports

instance Lake.instFamilyDefNameModuleDataMkStr2ArrayModule : Lake.FamilyDef Lake.ModuleData `lean.imports (Array Lake.Module)

Equations

• Lake.instFamilyDefNameModuleDataMkStr2ArrayModule = ⋯

@[simp]

axiom Lake.ModuleData.lean.imports : Lake.ModuleData `lean.imports = Array Lake.Module

@[reducible, inline]

abbrev Lake.Module.transImportsFacet : Lean.Name

The transitive local imports of the Lean module.

Equations

• Lake.Module.transImportsFacet = `lean.transImports

@[simp]

axiom Lake.ModuleData.lean.transImports : Lake.ModuleData `lean.transImports = Array Lake.Module

instance Lake.instFamilyDefNameModuleDataMkStr2ArrayModule_1 : Lake.FamilyDef Lake.ModuleData `lean.transImports (Array Lake.Module)

Equations

• Lake.instFamilyDefNameModuleDataMkStr2ArrayModule_1 = ⋯

@[reducible, inline]

abbrev Lake.Module.precompileImportsFacet : Lean.Name

The transitive local imports of the Lean module.

Equations

• Lake.Module.precompileImportsFacet = `lean.precompileImports

@[simp]

axiom Lake.ModuleData.lean.precompileImports : Lake.ModuleData `lean.precompileImports = Array Lake.Module

instance Lake.instFamilyDefNameModuleDataMkStr2ArrayModule_2 : Lake.FamilyDef Lake.ModuleData `lean.precompileImports (Array Lake.Module)

Equations

• Lake.instFamilyDefNameModuleDataMkStr2ArrayModule_2 = ⋯

@[reducible, inline]

abbrev Lake.Module.dynlibFacet : Lean.Name

Shared library for --load-dynlib.

Equations

• Lake.Module.dynlibFacet = `dynlib

@[simp]

axiom Lake.ModuleData.dynlib : Lake.ModuleData `dynlib = Lake.BuildJob Lake.Dynlib

instance Lake.instFamilyDefNameModuleDataMkStr1BuildJobDynlib : Lake.FamilyDef Lake.ModuleData `dynlib (Lake.BuildJob Lake.Dynlib)

Equations

• Lake.instFamilyDefNameModuleDataMkStr1BuildJobDynlib = ⋯

@[reducible, inline]

abbrev Lake.LeanLib.modulesFacet : Lean.Name

A Lean library's Lean modules.

Equations

• Lake.LeanLib.modulesFacet = `modules

@[simp]

axiom Lake.TargetData.leanLib.modules : Lake.TargetData (`leanLib ++ `modules) = Array Lake.Module

instance Lake.instFamilyDefNameTargetDataHAppendMkStr1ArrayModule : Lake.FamilyDef Lake.TargetData (`leanLib ++ `modules) (Array Lake.Module)

Equations

• Lake.instFamilyDefNameTargetDataHAppendMkStr1ArrayModule = ⋯

@[reducible, inline]

abbrev Lake.Package.depsFacet : Lean.Name

The package's complete array of transitive dependencies.

Equations

• Lake.Package.depsFacet = `deps

@[simp]

axiom Lake.PackageData.deps : Lake.PackageData `deps = Array Lake.Package

instance Lake.instFamilyDefNamePackageDataMkStr1ArrayPackage : Lake.FamilyDef Lake.PackageData `deps (Array Lake.Package)

Equations

• Lake.instFamilyDefNamePackageDataMkStr1ArrayPackage = ⋯

Facet Build Info Helper Constructors

Definitions to easily construct BuildInfo values for module, package, and target facets.

@[reducible, inline]

abbrev Lake.Module.facet (facet : Lean.Name) (self : Lake.Module) : Lake.BuildInfo

Build info for the module's specified facet.

Equations

• Lake.Module.facet facet self = Lake.BuildInfo.moduleFacet self facet

@[reducible, inline]

abbrev Lake.Module.imports (self : Lake.Module) : Lake.BuildInfo

The direct local imports of the Lean module.

Equations

• self.imports = Lake.Module.facet Lake.Module.importsFacet self

@[reducible, inline]

abbrev Lake.Module.transImports (self : Lake.Module) : Lake.BuildInfo

The transitive local imports of the Lean module.

Equations

• self.transImports = Lake.Module.facet Lake.Module.transImportsFacet self

@[reducible, inline]

abbrev Lake.Module.precompileImports (self : Lake.Module) : Lake.BuildInfo

The transitive local imports of the Lean module.

Equations

• self.precompileImports = Lake.Module.facet Lake.Module.precompileImportsFacet self

@[reducible, inline]

abbrev Lake.Module.deps (self : Lake.Module) : Lake.BuildInfo

The facet which builds all of a module's dependencies (i.e., transitive local imports and --load-dynlib shared libraries). Returns the list of shared libraries to load along with their search path.

Equations

• self.deps = Lake.Module.facet Lake.Module.depsFacet self

@[reducible, inline]

abbrev Lake.Module.leanArts (self : Lake.Module) : Lake.BuildInfo

The core build facet of a Lean file. Elaborates the Lean file via lean and produces all the Lean artifacts of the module (i.e., olean, ilean, c). Its trace just includes its dependencies.

Equations

• self.leanArts = Lake.Module.facet Lake.Module.leanArtsFacet self

@[reducible, inline]

abbrev Lake.Module.olean (self : Lake.Module) : Lake.BuildInfo

The olean file produced by lean.

Equations

• self.olean = Lake.Module.facet Lake.Module.oleanFacet self

@[reducible, inline]

abbrev Lake.Module.ilean (self : Lake.Module) : Lake.BuildInfo

The ilean file produced by lean.

Equations

• self.ilean = Lake.Module.facet Lake.Module.ileanFacet self

@[reducible, inline]

abbrev Lake.Module.c (self : Lake.Module) : Lake.BuildInfo

The C file built from the Lean file via lean.

Equations

• self.c = Lake.Module.facet Lake.Module.cFacet self

@[reducible, inline]

abbrev Lake.Module.bc (self : Lake.Module) : Lake.BuildInfo

The C file built from the Lean file via lean.

Equations

• self.bc = Lake.Module.facet Lake.Module.bcFacet self

@[reducible, inline]

abbrev Lake.Module.o (self : Lake.Module) : Lake.BuildInfo

The object file built from c/bc. On Windows with the C backend, no Lean symbols are exported. On every other configuration, symbols are exported.

Equations

• self.o = Lake.Module.facet Lake.Module.oFacet self

@[reducible, inline]

abbrev Lake.Module.oExport (self : Lake.Module) : Lake.BuildInfo

The object file built from c/bc (with Lean symbols exported).

Equations

• self.oExport = Lake.Module.facet Lake.Module.oExportFacet self

@[reducible, inline]

abbrev Lake.Module.oNoExport (self : Lake.Module) : Lake.BuildInfo

The object file built from c/bc (without Lean symbols exported).

Equations

• self.oNoExport = Lake.Module.facet Lake.Module.oNoExportFacet self

@[reducible, inline]

abbrev Lake.Module.co (self : Lake.Module) : Lake.BuildInfo

The object file .c.o built from c. On Windows, this is c.o.noexport, on other systems it is c.o.export).

Equations

• self.co = Lake.Module.facet Lake.Module.coFacet self

@[reducible, inline]

abbrev Lake.Module.coExport (self : Lake.Module) : Lake.BuildInfo

The object file .c.o.export built from c (with -DLEAN_EXPORTING).

Equations

• self.coExport = Lake.Module.facet Lake.Module.coExportFacet self

@[reducible, inline]

abbrev Lake.Module.coNoExport (self : Lake.Module) : Lake.BuildInfo

The object file .c.o.noexport built from c (without -DLEAN_EXPORTING).

Equations

• self.coNoExport = Lake.Module.facet Lake.Module.coNoExportFacet self

@[reducible, inline]

abbrev Lake.Module.bco (self : Lake.Module) : Lake.BuildInfo

The object file .bc.o built from bc.

Equations

• self.bco = Lake.Module.facet Lake.Module.bcoFacet self

@[reducible, inline]

abbrev Lake.Module.dynlib (self : Lake.Module) : Lake.BuildInfo

Shared library for --load-dynlib.

Equations

• self.dynlib = Lake.Module.facet Lake.Module.dynlibFacet self

@[reducible, inline]

abbrev Lake.Package.facet (facet : Lean.Name) (self : Lake.Package) : Lake.BuildInfo

Build info for the package's specified facet.

Equations

• Lake.Package.facet facet self = Lake.BuildInfo.packageFacet self facet

@[reducible, inline]

abbrev Lake.Package.buildCache (self : Lake.Package) : Lake.BuildInfo

A package's cached build archive (e.g., from Reservoir or GitHub). Will cause the whole build to fail if the archive cannot be fetched.

Equations

• self.buildCache = Lake.Package.facet Lake.Package.buildCacheFacet self

@[reducible, inline]

abbrev Lake.Package.optBuildCache (self : Lake.Package) : Lake.BuildInfo

A package's optional cached build archive (e.g., from Reservoir or GitHub). Will NOT cause the whole build to fail if the archive cannot be fetched.

Equations

• self.optBuildCache = Lake.Package.facet Lake.Package.optBuildCacheFacet self

@[reducible, inline]

abbrev Lake.Package.reservoirBarrel (self : Lake.Package) : Lake.BuildInfo

A package's Reservoir build archive from Reservoir. Will cause the whole build to fail if the barrel cannot be fetched.

Equations

• self.reservoirBarrel = Lake.Package.facet Lake.Package.reservoirBarrelFacet self

@[reducible, inline]

abbrev Lake.Package.optReservoirBarrel (self : Lake.Package) : Lake.BuildInfo

A package's optional build archive from Reservoir. Will NOT cause the whole build to fail if the barrel cannot be fetched.

Equations

• self.optReservoirBarrel = Lake.Package.facet Lake.Package.optReservoirBarrelFacet self

@[reducible, inline]

abbrev Lake.Package.gitHubRelease (self : Lake.Package) : Lake.BuildInfo

A package's build archive from a GitHub release. Will cause the whole build to fail if the release cannot be fetched.

Equations

• self.gitHubRelease = Lake.Package.facet Lake.Package.gitHubReleaseFacet self

@[reducible, inline]

abbrev Lake.Package.optGitHubRelease (self : Lake.Package) : Lake.BuildInfo

A package's optional build archive from a GitHub release. Will NOT cause the whole build to fail if the release cannot be fetched.

Equations

• self.optGitHubRelease = Lake.Package.facet Lake.Package.optGitHubReleaseFacet self

@[reducible, inline, deprecated]

abbrev Lake.Package.release (self : Lake.Package) : Lake.BuildInfo

Equations

• Lake.Package.release = Lake.Package.gitHubRelease

@[reducible, inline, deprecated]

abbrev Lake.Package.optRelease (self : Lake.Package) : Lake.BuildInfo

Equations

• Lake.Package.optRelease = Lake.Package.optGitHubRelease

@[reducible, inline]

abbrev Lake.Package.extraDep (self : Lake.Package) : Lake.BuildInfo

A package's extraDepTargets mixed with its transitive dependencies'.

Equations

• self.extraDep = Lake.Package.facet Lake.Package.extraDepFacet self

@[reducible, inline]

abbrev Lake.Package.target (target : Lean.Name) (self : Lake.Package) : Lake.BuildInfo

Build info for a custom package target.

Equations

• Lake.Package.target target self = Lake.BuildInfo.target self target

@[reducible, inline]

abbrev Lake.LeanLib.facet (self : Lake.LeanLib) (facet : Lean.Name) : Lake.BuildInfo

Build info of the Lean library's Lean binaries.

Equations

• self.facet facet = Lake.BuildInfo.libraryFacet self facet

@[reducible, inline]

abbrev Lake.LeanLib.modules (self : Lake.LeanLib) : Lake.BuildInfo

A Lean library's Lean modules.

Equations

• self.modules = self.facet Lake.LeanLib.modulesFacet

@[reducible, inline]

abbrev Lake.LeanLib.leanArts (self : Lake.LeanLib) : Lake.BuildInfo

A Lean library's Lean artifacts (i.e., olean, ilean, c).

Equations

• self.leanArts = self.facet Lake.LeanLib.leanArtsFacet

@[reducible, inline]

abbrev Lake.LeanLib.static (self : Lake.LeanLib) : Lake.BuildInfo

A Lean library's static artifact.

Equations

• self.static = self.facet Lake.LeanLib.staticFacet

@[reducible, inline]

abbrev Lake.LeanLib.staticExport (self : Lake.LeanLib) : Lake.BuildInfo

A Lean library's static artifact (with exported symbols).

Equations

• self.staticExport = self.facet Lake.LeanLib.staticExportFacet

@[reducible, inline]

abbrev Lake.LeanLib.shared (self : Lake.LeanLib) : Lake.BuildInfo

A Lean library's shared artifact.

Equations

• self.shared = self.facet Lake.LeanLib.sharedFacet

@[reducible, inline]

abbrev Lake.LeanLib.extraDep (self : Lake.LeanLib) : Lake.BuildInfo

A Lean library's extraDepTargets mixed with its package's.

Equations

• self.extraDep = self.facet Lake.LeanLib.extraDepFacet

@[reducible, inline]

abbrev Lake.LeanExe.exe (self : Lake.LeanExe) : Lake.BuildInfo

Build info of the Lean executable.

Equations

• self.exe = Lake.BuildInfo.leanExe self

@[reducible, inline]

abbrev Lake.ExternLib.static (self : Lake.ExternLib) : Lake.BuildInfo

Build info of the external library's static binary.

Equations

• self.static = Lake.BuildInfo.staticExternLib self

@[reducible, inline]

abbrev Lake.ExternLib.shared (self : Lake.ExternLib) : Lake.BuildInfo

Build info of the external library's shared binary.

Equations

• self.shared = Lake.BuildInfo.sharedExternLib self

@[reducible, inline]

abbrev Lake.ExternLib.dynlib (self : Lake.ExternLib) : Lake.BuildInfo

Build info of the external library's dynlib.

Equations

• self.dynlib = Lake.BuildInfo.dynlibExternLib self