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

• 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

The type of Lake's build info.

Build Info & Keys

Build Key Helper Constructors

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

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.

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

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

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

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

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

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

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

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

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

Recursive Building

@[inline, reducible]

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

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

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

@[inline, reducible]

abbrev Lake.IndexBuildM (α : Type) : Type

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

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

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.

@[simp]

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

instance Lake.instFamilyDefNameModuleDataMkStrAnonymousArrayModule : Lake.FamilyDef 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.

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

@[inline, reducible]

abbrev Lake.Module.precompileImportsFacet : Lake.Name

The transitive local imports of the Lean module.

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

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

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

@[inline, reducible]

abbrev Lake.LeanLib.modulesFacet : Lake.Name

A Lean library's Lean modules.

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

@[simp]

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

@[inline, reducible]

abbrev Lake.Package.depsFacet : Lake.Name

The package's complete array of transitive dependencies.

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

@[simp]

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

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.

@[inline, reducible]

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

The direct local imports of the Lean module.

@[inline, reducible]

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

The transitive local imports of the Lean module.

@[inline, reducible]

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

The transitive local imports of the Lean module.

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

@[inline, reducible]

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

The core compilation / elaboration of the Lean file via lean, which produce the Lean binaries of the module (i.e., olean, ilean, c). Its trace just includes its dependencies.

@[inline, reducible]

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

The leanBinFacet combined with the module's trace (i.e., the trace of its olean and ilean). It is the facet used for building a Lean import of a module.

@[inline, reducible]

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

The olean file produced by lean

@[inline, reducible]

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

The ilean file produced by lean

@[inline, reducible]

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

The C file built from the Lean file via lean

@[inline, reducible]

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

The object file built from lean.c

@[inline, reducible]

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

Shared library for --load-dynlib.

@[inline, reducible]

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

Build info for the package's specified facet.

@[inline, reducible]

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

A package's cloud build release.

@[inline, reducible]

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

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

@[inline, reducible]

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

Build info for a custom package target.

@[inline, reducible]

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

Build info of the Lean library's Lean binaries.

@[inline, reducible]

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

A Lean library's Lean modules.

@[inline, reducible]

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

A Lean library's Lean libraries.

@[inline, reducible]

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

A Lean library's static binary.

@[inline, reducible]

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

A Lean library's shared binary.

@[inline, reducible]

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

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

@[inline, reducible]

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

Build info of the Lean executable.

@[inline, reducible]

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

Build info of the external library's static binary.

@[inline, reducible]

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

Build info of the external library's shared binary.

@[inline, reducible]

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

Build info of the external library's dynlib.