Module Facet Builds #
Build function definitions for a module's builtin facets.
The ModuleFacetConfig
for the builtin importsFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin transImportsFacet
.
Equations
Instances For
Equations
Instances For
The ModuleFacetConfig
for the builtin precompileImportsFacet
.
Equations
Instances For
Equations
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
Instances For
The ModuleFacetConfig
for the builtin depsFacet
.
Equations
Instances For
Remove cached file hashes of the module build outputs (in .hash
files).
Equations
Instances For
Cache the file hashes of the module build outputs in .hash
files.
Equations
Instances For
The ModuleFacetConfig
for the builtin leanArtsFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin oleanFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin ileanFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin cFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin bcFacet
.
Equations
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
Instances For
The ModuleFacetConfig
for the builtin coExportFacet
.
Equations
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
Instances For
The ModuleFacetConfig
for the builtin coNoExportFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin coFacet
.
Equations
Instances For
Recursively build the module's object file from its bitcode file produced by lean
.
Equations
Instances For
The ModuleFacetConfig
for the builtin bcoFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin oExportFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin oNoExportFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin oFacet
.
Equations
Instances For
The ModuleFacetConfig
for the builtin dynlibFacet
.
Equations
Instances For
A name-configuration map for the initial set of
Lake module facets (e.g., imports
, c
, o
, dynlib
).
Equations
Instances For
A name-configuration map for the initial set of
Lake module facets (e.g., imports
, c
, o
, dynlib
).