Module Facet Builds #
Build function definitions for a module's builtin facets.
Compute library directories and build external library Jobs of the given packages.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Build the dynlibs of the transitive imports that want precompilation and the dynlibs of their imports.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Recursively parse the Lean files of a module and its imports
building an Array
product of its direct local imports.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin importsFacet
.
Equations
- Lake.Module.importsFacetConfig = Lake.mkFacetConfig fun (x : Lake.Module) => x.recParseImports
Instances For
Recursively compute a module's transitive imports.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin transImportsFacet
.
Equations
- Lake.Module.transImportsFacetConfig = Lake.mkFacetConfig fun (x : Lake.Module) => x.recComputeTransImports
Instances For
Recursively compute a module's precompiled imports.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin precompileImportsFacet
.
Equations
- Lake.Module.precompileImportsFacetConfig = Lake.mkFacetConfig fun (x : Lake.Module) => x.recComputePrecompileImports
Instances For
Recursively build a module's dependencies, including:
- Transitive local imports
- Shared libraries (e.g.,
extern_lib
targets or precompiled modules) extraDepTargets
of its library
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin depsFacet
.
Equations
- Lake.Module.depsFacetConfig = Lake.mkFacetJobConfig fun (x : Lake.Module) => x.recBuildDeps
Instances For
Recursively build a Lean module.
Fetch its dependencies and then elaborate the Lean source file, producing
all possible artifacts (i.e., .olean
, ilean
, .c
, and .bc
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin leanArtsFacet
.
Equations
- Lake.Module.leanArtsFacetConfig = Lake.mkFacetJobConfig fun (x : Lake.Module) => x.recBuildLean
Instances For
The ModuleFacetConfig
for the builtin oleanFacet
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin ileanFacet
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin cFacet
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin bcFacet
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Recursively build the module's object file from its C file produced by lean
with -DLEAN_EXPORTING
set, which exports Lean symbols defined within the C files.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin coExportFacet
.
Instances For
Recursively build the module's object file from its C file produced by lean
.
This version does not export any Lean symbols.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin coNoExportFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin coFacet
.
Equations
- Lake.Module.coFacetConfig = Lake.mkFacetJobConfig fun (mod : Lake.Module) => if System.Platform.isWindows = true then mod.coNoExport.fetch else mod.coExport.fetch
Instances For
Recursively build the module's object file from its bitcode file produced by lean
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin bcoFacet
.
Instances For
The ModuleFacetConfig
for the builtin oExportFacet
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin oNoExportFacet
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin oFacet
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Recursively build the shared library of a module (e.g., for --load-dynlib
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ModuleFacetConfig
for the builtin dynlibFacet
.
Instances For
A name-configuration map for the initial set of
Lake module facets (e.g., lean.{imports, c, o, dynlib]
).
Equations
- One or more equations did not get rendered due to their size.