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.
Build Info & Keys #
Build Key Helper Constructors #
Equations
- self.buildKey = Lake.BuildKey.module self.keyName
Instances For
Equations
- Lake.Module.facetBuildKey facet self = self.key.facet facet
Instances For
Equations
- self.buildKey = Lake.BuildKey.package self.name
Instances For
Equations
- Lake.Package.facetBuildKey facet self = self.key.facet facet
Instances For
Equations
- Lake.Package.targetKey target self = Lake.BuildKey.packageTarget self.name target
Instances For
Equations
- Lake.Package.targetBuildKey target self = Lake.BuildKey.packageTarget self.name target
Instances For
Instances For
Instances For
Equations
- self.facetBuildKey facet = self.key.facet facet
Instances For
Equations
- self.exeBuildKey = (Lake.ConfigTarget.key self).facet Lake.LeanExe.exeFacet
Instances For
Equations
Instances For
Equations
Instances For
Build Info to Key #
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
Instances For
Equations
- Lake.instToStringBuildInfo = { toString := fun (x : Lake.BuildInfo) => toString x.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.
Equations
- Lake.instDataKindModule = { name := `module, wf := Lake.instDataKindModule.proof_1 }
Equations
- Lake.instDataKindPackage = { name := `package, wf := Lake.instDataKindPackage.proof_1 }
Equations
- Lake.instDataKindLeanLib = { name := `lean_lib, wf := Lake.instDataKindLeanLib.proof_1 }
Equations
- Lake.instDataKindLeanExe = { name := `lean_exe, wf := Lake.instDataKindLeanExe.proof_1 }
Equations
- Lake.instDataKindExternLib = { name := `extern_lib, wf := Lake.instDataKindExternLib.proof_1 }
Equations
- Lake.instDataKindInputFile = { name := `input_file, wf := Lake.instDataKindInputFile.proof_1 }
Equations
- Lake.instDataKindInputDir = { name := `input_dir, wf := Lake.instDataKindInputDir.proof_1 }
The direct local imports of the Lean module.
Equations
- Lake.Module.importsFacet = `module.imports
Instances For
The transitive local imports of the Lean module.
Equations
- Lake.Module.transImportsFacet = `module.transImports
Instances For
The transitive local imports of the Lean module.
Equations
- Lake.Module.precompileImportsFacet = `module.precompileImports
Instances For
Shared library for --load-dynlib
.
Equations
- Lake.Module.dynlibFacet = `module.dynlib
Instances For
A Lean library's Lean modules.
Equations
- Lake.LeanLib.modulesFacet = `lean_lib.modules
Instances For
The package's array of dependencies.
Equations
- Lake.Package.depsFacet = `package.deps
Instances For
The package's complete array of transitive dependencies.
Equations
- Lake.Package.transDepsFacet = `package.transDeps
Instances For
Facet Build Info Helper Constructors #
Definitions to easily construct BuildInfo
values for module, package,
and target facets.
Module Infos #
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.
Equations
- Lake.Module.facetCore facet self = Lake.BuildInfo.facet self.key Lake.Module.facetKind (Lake.toFamily self) facet
Instances For
Build info for a module facet.
Equations
- Lake.Module.facet facet self = Lake.Module.facetCore (Lake.Module.facetKind ++ facet) self
Instances For
Equations
- Lake.BuildInfo.moduleFacet module facet = Lake.Module.facetCore facet module
Instances For
The direct local imports of the Lean module.
Equations
Instances For
The transitive local imports of the Lean module.
Equations
Instances For
The transitive local imports of the Lean module.
Equations
Instances For
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.facetCore Lake.Module.depsFacet self
Instances For
The olean
file produced by lean
.
Equations
- self.olean = Lake.Module.facetCore Lake.Module.oleanFacet self
Instances For
The ilean
file produced by lean
.
Equations
- self.ilean = Lake.Module.facetCore Lake.Module.ileanFacet self
Instances For
The C file built from the Lean file via lean
.
Equations
- self.c = Lake.Module.facetCore Lake.Module.cFacet self
Instances For
The C file built from the Lean file via lean
.
Equations
- self.bc = Lake.Module.facetCore Lake.Module.bcFacet self
Instances For
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.facetCore Lake.Module.oFacet self
Instances For
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.facetCore Lake.Module.coFacet self
Instances For
The object file .c.o.export
built from c
(with -DLEAN_EXPORTING
).
Equations
Instances For
The object file .c.o.noexport
built from c
(without -DLEAN_EXPORTING
).
Equations
Instances For
The object file .bc.o
built from bc
.
Equations
- self.bco = Lake.Module.facetCore Lake.Module.bcoFacet self
Instances For
Shared library for --load-dynlib
.
Equations
- self.dynlib = Lake.Module.facetCore Lake.Module.dynlibFacet self
Instances For
Package Infos #
Build info for a package target (e.g., a library, executable, or custom target).
Equations
- Lake.Package.target target self = Lake.BuildInfo.target self target
Instances For
Equations
- Lake.Package.facetCore facet self = Lake.BuildInfo.facet self.key Lake.Package.facetKind (Lake.toFamily self) facet
Instances For
Build info for a package facet.
Equations
- Lake.Package.facet facet self = Lake.Package.facetCore (Lake.Package.facetKind ++ facet) self
Instances For
Equations
- Lake.BuildInfo.packageFacet package facet = Lake.Package.facetCore facet package
Instances For
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
Instances For
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
Instances For
A package's Reservoir build archive from Reservoir. Will cause the whole build to fail if the barrel cannot be fetched.
Equations
Instances For
A package's optional build archive from Reservoir. Will NOT cause the whole build to fail if the barrel cannot be fetched.
Equations
Instances For
A package's build archive from a GitHub release. Will cause the whole build to fail if the release cannot be fetched.
Equations
Instances For
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
Instances For
Instances For
Instances For
A package's extraDepTargets
mixed with its transitive dependencies'.
Equations
Instances For
The package's array of dependencies.
Equations
- self.deps = Lake.Package.facetCore Lake.Package.depsFacet self
Instances For
The package's complete array of transitive dependencies.
Equations
Instances For
Lean Library Infos #
Equations
- Lake.LeanLib.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.LeanLib.facetKind (Lake.toFamily self) facet
Instances For
Build info for a facet of a Lean library.
Equations
- Lake.LeanLib.facet facet self = Lake.LeanLib.facetCore (Lake.LeanLib.facetKind ++ facet) self
Instances For
Equations
- Lake.BuildInfo.libraryFacet lib facet = Lake.LeanLib.facetCore facet lib
Instances For
A Lean library's Lean modules.
Equations
Instances For
A Lean library's static artifact.
Equations
Instances For
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.
Equations
Instances For
A Lean library's extraDepTargets
mixed with its package's.
Equations
Instances For
Lean Executable Infos #
Equations
- Lake.LeanExe.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.LeanExe.facetKind (Lake.toFamily self) facet
Instances For
Build info of the Lean executable.
Equations
- self.exe = Lake.LeanExe.facetCore Lake.LeanExe.exeFacet self
Instances For
Equations
- Lake.BuildInfo.leanExe exe = exe.exe
Instances For
External Library Infos #
Equations
- Lake.ExternLib.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.ExternLib.facetKind (Lake.toFamily self) facet
Instances For
Build info of the external library's static binary.
Equations
Instances For
Equations
Instances For
Build info of the external library's dynlib.
Equations
Instances For
Equations
Instances For
Input File & Directory Infos #
Equations
- Lake.InputFile.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.InputFile.facetKind (Lake.toFamily self) facet
Instances For
Build info of the input file's default facet.
Equations
Instances For
Equations
- Lake.InputDir.facetCore facet self = Lake.BuildInfo.facet (Lake.ConfigTarget.key self) Lake.InputDir.facetKind (Lake.toFamily self) facet
Instances For
Build info of the input directory's default facet.