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 → Lake.Name → Lake.BuildInfo
• packageFacet: Lake.Package → Lake.Name → Lake.BuildInfo
• libraryFacet: Lake.LeanLib → Lake.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 → Lake.Name → Lake.BuildInfo

Build Info & Keys

Build Key Helper Constructors

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

@[inline, reducible]

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

Equations

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

Build Info to Key

@[inline, reducible]

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

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

Equations

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

Instances for deducing data types of BuildInfo keys

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

Recursive Building

@[inline, reducible]

abbrev Lake.IndexBuildFn (m : Type → Type v) : Type v

A build function for any element of the Lake build index.

Equations

• Lake.IndexBuildFn m = ((info : Lake.BuildInfo) → m (Lake.BuildData (Lake.BuildInfo.key info)))

@[inline, reducible]

abbrev Lake.IndexT (m : Type → Type v) (α : Type) : Type v

A transformer to equip a monad with a build function for the Lake index.

Equations

• Lake.IndexT m = Lake.EquipT (Lake.IndexBuildFn m) m

@[inline, reducible]

abbrev Lake.IndexBuildM (α : Type) : Type

The monad for build functions that are part of the index.

Equations

• Lake.IndexBuildM = Lake.IndexT Lake.RecBuildM

@[inline]

def Lake.BuildInfo.fetch {α : Type} (self : Lake.BuildInfo) [Lake.FamilyOut Lake.BuildData (Lake.BuildInfo.key self) α] : Lake.IndexBuildM α

Fetch the result associated with the info using the Lake build index.

Equations

• Lake.fetch self build = cast ⋯ (build self)

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.

@[inline, reducible]

abbrev Lake.Module.importsFacet : Lake.Name

The direct local imports of the Lean module.

Equations

• Lake.Module.importsFacet = `lean.imports

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousArrayModule : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "lean") "imports") (Array Lake.Module)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousArrayModule = ⋯

@[simp]

axiom Lake.ModuleData.lean.imports : Lake.ModuleData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "lean") "imports") = Array Lake.Module

@[inline, reducible]

abbrev Lake.Module.transImportsFacet : Lake.Name

The transitive local imports of the Lean module.

Equations

• Lake.Module.transImportsFacet = `lean.transImports

@[simp]

axiom Lake.ModuleData.lean.transImports : Lake.ModuleData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "lean") "transImports") = Array Lake.Module

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousArrayModule_1 : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "lean") "transImports") (Array Lake.Module)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousArrayModule_1 = ⋯

@[inline, reducible]

abbrev Lake.Module.precompileImportsFacet : Lake.Name

The transitive local imports of the Lean module.

Equations

• Lake.Module.precompileImportsFacet = `lean.precompileImports

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousArrayModule_2 : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "lean") "precompileImports") (Array Lake.Module)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousArrayModule_2 = ⋯

@[simp]

axiom Lake.ModuleData.lean.precompileImports : Lake.ModuleData (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "lean") "precompileImports") = Array Lake.Module

@[inline, reducible]

abbrev Lake.Module.dynlibFacet : Lake.Name

Shared library for --load-dynlib.

Equations

• Lake.Module.dynlibFacet = `dynlib

@[simp]

axiom Lake.ModuleData.dynlib : Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "dynlib") = Lake.BuildJob Lake.Dynlib

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobDynlib : Lake.FamilyDef Lake.ModuleData (Lean.Name.mkStr Lean.Name.anonymous "dynlib") (Lake.BuildJob Lake.Dynlib)

Equations

• Lake.instFamilyDefNameModuleDataMkStrAnonymousBuildJobDynlib = ⋯

@[inline, reducible]

abbrev Lake.LeanLib.modulesFacet : Lake.Name

A Lean library's Lean modules.

Equations

• Lake.LeanLib.modulesFacet = `modules

@[simp]

axiom Lake.TargetData.leanLib.modules : Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "modules") = Array Lake.Module

instance Lake.instFamilyDefNameTargetDataHAppendInstHAppendInstAppendNameMkStr1MkStrAnonymousArrayModule : Lake.FamilyDef Lake.TargetData (`leanLib ++ Lean.Name.mkStr Lean.Name.anonymous "modules") (Array Lake.Module)

Equations

• Lake.instFamilyDefNameTargetDataHAppendInstHAppendInstAppendNameMkStr1MkStrAnonymousArrayModule = ⋯

@[inline, reducible]

abbrev Lake.Package.depsFacet : Lake.Name

The package's complete array of transitive dependencies.

Equations

• Lake.Package.depsFacet = `deps

@[simp]

axiom Lake.PackageData.deps : Lake.PackageData (Lean.Name.mkStr Lean.Name.anonymous "deps") = Array Lake.Package

instance Lake.instFamilyDefNamePackageDataMkStrAnonymousArrayPackage : Lake.FamilyDef Lake.PackageData (Lean.Name.mkStr Lean.Name.anonymous "deps") (Array Lake.Package)

Equations

• Lake.instFamilyDefNamePackageDataMkStrAnonymousArrayPackage = ⋯

Facet Build Info Helper Constructors

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

@[inline, reducible]

abbrev Lake.Module.facet (facet : Lake.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

@[inline, reducible]

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

The direct local imports of the Lean module.

Equations

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

@[inline, reducible]

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

The transitive local imports of the Lean module.

Equations

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

@[inline, reducible]

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

The transitive local imports of the Lean module.

Equations

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

@[inline, reducible]

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

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

@[inline, reducible]

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

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

@[inline, reducible]

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

The olean file produced by lean.

Equations

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

@[inline, reducible]

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

The ilean file produced by lean.

Equations

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

@[inline, reducible]

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

The C file built from the Lean file via lean.

Equations

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

@[inline, reducible]

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

The C file built from the Lean file via lean.

Equations

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

@[inline, reducible]

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

The object file built from c/bc.

Equations

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

@[inline, reducible]

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

The object file .c.o built from c.

Equations

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

@[inline, reducible]

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

The object file .bc.o built from bc.

Equations

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

@[inline, reducible]

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

Shared library for --load-dynlib.

Equations

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

@[inline, reducible]

abbrev Lake.Package.facet (facet : Lake.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

@[inline, reducible]

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

A package's cloud build release.

Equations

• Lake.Package.release self = Lake.Package.facet Lake.Package.releaseFacet self

@[inline, reducible]

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

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

Equations

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

@[inline, reducible]

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

Build info for a custom package target.

Equations

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

@[inline, reducible]

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

Build info of the Lean library's Lean binaries.

Equations

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

@[inline, reducible]

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

A Lean library's Lean modules.

Equations

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

@[inline, reducible]

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

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

Equations

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

@[inline, reducible]

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

A Lean library's static artifact.

Equations

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

@[inline, reducible]

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

A Lean library's shared artifact.

Equations

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

@[inline, reducible]

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

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

Equations

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

@[inline, reducible]

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

Build info of the Lean executable.

Equations

• Lake.LeanExe.exe self = Lake.BuildInfo.leanExe self

@[inline, reducible]

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

Build info of the external library's static binary.

Equations

• Lake.ExternLib.static self = Lake.BuildInfo.staticExternLib self

@[inline, reducible]

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

Build info of the external library's shared binary.

Equations

• Lake.ExternLib.shared self = Lake.BuildInfo.sharedExternLib self

@[inline, reducible]

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

Build info of the external library's dynlib.

Equations

• Lake.ExternLib.dynlib self = Lake.BuildInfo.dynlibExternLib self