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.Module.key (self : Module) : BuildKey

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

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

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

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

@[reducible, inline]

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

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

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

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

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

@[reducible, inline]

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

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

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

@[reducible, inline]

abbrev Lake.ConfigTarget.key {kind : Lean.Name} (self : ConfigTarget kind) : BuildKey

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

abbrev Lake.ConfigTarget.buildKey {kind : Lean.Name} (self : ConfigTarget kind) : BuildKey

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

abbrev Lake.ConfigTarget.facetBuildKey {kind : Lean.Name} (self : ConfigTarget kind) (facet : Lean.Name) : BuildKey

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

abbrev Lake.ExternLib.dynlibBuildKey (self : ExternLib) : 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.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 α

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.

instance Lake.instDataKindModule : DataKind Module

@[simp]

axiom Lake.DataType.module : DataType `module = Module

instance Lake.instFamilyDefNameDataTypeMkStr1Module : FamilyDef DataType `module Module

instance Lake.instFamilyDefNameDataTypeMkStr1Package : FamilyDef DataType `package Package

@[simp]

axiom Lake.DataType.package : DataType `package = Package

instance Lake.instDataKindPackage : DataKind Package

instance Lake.instDataKindLeanLib : DataKind LeanLib

instance Lake.instFamilyDefNameDataTypeMkStr1LeanLib : FamilyDef DataType `lean_lib LeanLib

@[simp]

axiom Lake.DataType.lean_lib : DataType `lean_lib = LeanLib

instance Lake.instFamilyDefNameDataTypeMkStr1LeanExe : FamilyDef DataType `lean_exe LeanExe

instance Lake.instDataKindLeanExe : DataKind LeanExe

@[simp]

axiom Lake.DataType.lean_exe : DataType `lean_exe = LeanExe

@[simp]

axiom Lake.DataType.extern_lib : DataType `extern_lib = ExternLib

instance Lake.instFamilyDefNameDataTypeMkStr1ExternLib : FamilyDef DataType `extern_lib ExternLib

instance Lake.instDataKindExternLib : DataKind ExternLib

@[simp]

axiom Lake.DataType.input_file : DataType `input_file = InputFile

instance Lake.instFamilyDefNameDataTypeMkStr1InputFile : FamilyDef DataType `input_file InputFile

instance Lake.instDataKindInputFile : DataKind InputFile

instance Lake.instFamilyDefNameDataTypeMkStr1InputDir : FamilyDef DataType `input_dir InputDir

@[simp]

axiom Lake.DataType.input_dir : DataType `input_dir = InputDir

instance Lake.instDataKindInputDir : DataKind InputDir

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule : FamilyDef FacetOut (`module ++ `imports) (Array Module)

@[simp]

axiom Lake.FacetOut.module.imports : FacetOut `module.imports = Array Module

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule : FamilyDef FacetOut `module.imports (Array Module)

@[reducible]

def Lake.Module.importsFacet : Lean.Name

The direct local imports of the Lean module.

@[simp]

axiom Lake.FacetOut.module.transImports : FacetOut `module.transImports = Array Module

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_1 : FamilyDef FacetOut (`module ++ `transImports) (Array Module)

@[reducible]

def Lake.Module.transImportsFacet : Lean.Name

The transitive local imports of the Lean module.

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_1 : FamilyDef FacetOut `module.transImports (Array Module)

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_2 : FamilyDef FacetOut (`module ++ `precompileImports) (Array Module)

@[reducible]

def Lake.Module.precompileImportsFacet : Lean.Name

The transitive local imports of the Lean module.

@[simp]

axiom Lake.FacetOut.module.precompileImports : FacetOut `module.precompileImports = Array Module

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_2 : FamilyDef FacetOut `module.precompileImports (Array Module)

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1Dynlib_2 : FamilyDef FacetOut (`module ++ `dynlib) Dynlib

instance Lake.instFamilyDefNameFacetOutMkStr2Dynlib_2 : FamilyDef FacetOut `module.dynlib Dynlib

@[simp]

axiom Lake.FacetOut.module.dynlib : FacetOut `module.dynlib = Dynlib

@[reducible]

def Lake.Module.dynlibFacet : Lean.Name

Shared library for --load-dynlib.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayModule_3 : FamilyDef FacetOut (`lean_lib ++ `modules) (Array Module)

@[simp]

axiom Lake.FacetOut.lean_lib.modules : FacetOut `lean_lib.modules = Array Module

@[reducible]

def Lake.LeanLib.modulesFacet : Lean.Name

A Lean library's Lean modules.

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayModule_3 : FamilyDef FacetOut `lean_lib.modules (Array Module)

@[simp]

axiom Lake.FacetOut.package.deps : FacetOut `package.deps = Array Package

@[reducible]

def Lake.Package.depsFacet : Lean.Name

The package's array of dependencies.

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayPackage : FamilyDef FacetOut (`package ++ `deps) (Array Package)

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayPackage : FamilyDef FacetOut `package.deps (Array Package)

@[simp]

axiom Lake.FacetOut.package.transDeps : FacetOut `package.transDeps = Array Package

instance Lake.instFamilyDefNameFacetOutHAppendMkStr1ArrayPackage_1 : FamilyDef FacetOut (`package ++ `transDeps) (Array Package)

instance Lake.instFamilyDefNameFacetOutMkStr2ArrayPackage_1 : FamilyDef FacetOut `package.transDeps (Array Package)

@[reducible]

def Lake.Package.transDepsFacet : Lean.Name

The package's complete array of transitive dependencies.

Facet Build Info Helper Constructors

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

Module Infos

@[reducible, inline]

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

Build info for applying the specified facet to the module. It is the user's obiligation to ensure the facet in question is a module facet.

@[reducible, inline]

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

Build info for a module facet.

@[reducible, inline, deprecated Lake.Module.facetCore (since := "2025-03-04")]

abbrev Lake.BuildInfo.moduleFacet (module : Module) (facet : Lean.Name) : BuildInfo

@[reducible, inline]

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

The direct local imports of the Lean module.

@[reducible, inline]

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

The transitive local imports of the Lean module.

@[reducible, inline]

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

The transitive local imports of the Lean module.

@[reducible, inline]

abbrev Lake.Module.deps (self : Module) : 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.

@[reducible, inline]

abbrev Lake.Module.leanArts (self : Module) : 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.

@[reducible, inline]

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

The olean file produced by lean.

@[reducible, inline]

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

The ilean file produced by lean.

@[reducible, inline]

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

The C file built from the Lean file via lean.

@[reducible, inline]

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

The C file built from the Lean file via lean.

@[reducible, inline]

abbrev Lake.Module.o (self : Module) : 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.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

The object file .bc.o built from bc.

@[reducible, inline]

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

Shared library for --load-dynlib.

Package Infos

@[reducible, inline]

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

Build info for a package target (e.g., a library, executable, or custom target).

@[reducible, inline]

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

@[reducible, inline]

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

Build info for a package facet.

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

abbrev Lake.BuildInfo.packageFacet (package : Package) (facet : Lean.Name) : BuildInfo

@[reducible, inline]

abbrev Lake.Package.buildCache (self : Package) : 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.

@[reducible, inline]

abbrev Lake.Package.optBuildCache (self : Package) : 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.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

abbrev Lake.Package.optGitHubRelease (self : Package) : 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.

@[reducible, inline]

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

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

@[reducible, inline]

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

The package's array of dependencies.

@[reducible, inline]

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

The package's complete array of transitive dependencies.

Lean Library Infos

@[reducible, inline]

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

@[reducible, inline]

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

Build info for a facet of a Lean library.

@[reducible, inline, deprecated Lake.LeanLib.facetCore (since := "2025-03-04")]

abbrev Lake.BuildInfo.libraryFacet (lib : LeanLib) (facet : Lean.Name) : BuildInfo

@[reducible, inline]

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

A Lean library's Lean modules.

@[reducible, inline]

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

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

@[reducible, inline]

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

A Lean library's static artifact.

@[reducible, inline]

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

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

Static libraries with explicit exports are built as thin libraries. Such libraries are usually used as part of the local build process of some shared artifact and not publicly distributed. Standard static libraries are much better for distribution.

@[reducible, inline]

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

A Lean library's shared artifact.

@[reducible, inline]

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

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

Lean Executable Infos

@[reducible, inline]

abbrev Lake.LeanExe.facetCore (facet : Lean.Name) (self : LeanExe) : BuildInfo

@[reducible, inline]

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

Build info of the Lean executable.

@[reducible, inline, deprecated Lake.LeanExe.exe (since := "2025-03-04")]

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

External Library Infos

@[reducible, inline]

abbrev Lake.ExternLib.facetCore (facet : Lean.Name) (self : ExternLib) : BuildInfo

@[reducible, inline]

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

Build info of the external library's static binary.

@[reducible, inline, deprecated Lake.ExternLib.static (since := "2025-03-04")]

abbrev Lake.BuildInfo.staticExternLib (lib : ExternLib) : BuildInfo

@[reducible, inline]

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

Build info of the external library's shared binary.

@[reducible, inline, deprecated Lake.ExternLib.shared (since := "2025-03-04")]

abbrev Lake.BuildInfo.sharedExternLib (lib : ExternLib) : BuildInfo

@[reducible, inline]

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

Build info of the external library's dynlib.

@[reducible, inline, deprecated Lake.ExternLib.dynlib (since := "2025-03-04")]

abbrev Lake.BuildInfo.dynlibExternLib (lib : ExternLib) : BuildInfo

Input File & Directory Infos

@[reducible, inline]

abbrev Lake.InputFile.facetCore (facet : Lean.Name) (self : InputFile) : BuildInfo

@[reducible, inline]

abbrev Lake.InputFile.default (self : InputFile) : BuildInfo

Build info of the input file's default facet.

@[reducible, inline]

abbrev Lake.InputDir.facetCore (facet : Lean.Name) (self : InputDir) : BuildInfo

@[reducible, inline]

abbrev Lake.InputDir.default (self : InputDir) : BuildInfo

Build info of the input directory's default facet.