Module Facet Builds

Build function definitions for a module's builtin facets.

def Lake.recBuildExternDynlibs (pkgs : Array Lake.Package) : Lake.FetchM (Array (Lake.BuildJob Lake.Dynlib) × Array System.FilePath)

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.

def Lake.Module.recParseImports (mod : Lake.Module) : Lake.FetchM (Array Lake.Module)

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.

def Lake.Module.importsFacetConfig : Lake.ModuleFacetConfig Lake.Module.importsFacet

The ModuleFacetConfig for the builtin importsFacet.

Equations

• Lake.Module.importsFacetConfig = Lake.mkFacetConfig fun (x : Lake.Module) => x.recParseImports

@[inline]

def Lake.collectImportsAux (leanFile : System.FilePath) (imports : Array Lake.Module) (f : Lake.Module → Lake.FetchM (Bool × Array Lake.Module)) : Lake.FetchM (Array Lake.Module)

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.recComputeTransImports (mod : Lake.Module) : Lake.FetchM (Array Lake.Module)

Recursively compute a module's transitive imports.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.transImportsFacetConfig : Lake.ModuleFacetConfig Lake.Module.transImportsFacet

The ModuleFacetConfig for the builtin transImportsFacet.

Equations

• Lake.Module.transImportsFacetConfig = Lake.mkFacetConfig fun (x : Lake.Module) => x.recComputeTransImports

@[inline]

def Lake.computePrecompileImportsAux (leanFile : System.FilePath) (imports : Array Lake.Module) : Lake.FetchM (Array Lake.Module)

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.recComputePrecompileImports (mod : Lake.Module) : Lake.FetchM (Array Lake.Module)

Recursively compute a module's precompiled imports.

Equations

• mod.recComputePrecompileImports = do let __do_lift ← mod.imports.fetch Lake.computePrecompileImportsAux mod.leanFile __do_lift

def Lake.Module.precompileImportsFacetConfig : Lake.ModuleFacetConfig Lake.Module.precompileImportsFacet

The ModuleFacetConfig for the builtin precompileImportsFacet.

Equations

• Lake.Module.precompileImportsFacetConfig = Lake.mkFacetConfig fun (x : Lake.Module) => x.recComputePrecompileImports

def Lake.Module.recBuildDeps (mod : Lake.Module) : Lake.FetchM (Lake.BuildJob (System.SearchPath × Array System.FilePath))

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.

def Lake.Module.depsFacetConfig : Lake.ModuleFacetConfig Lake.Module.depsFacet

The ModuleFacetConfig for the builtin depsFacet.

Equations

• Lake.Module.depsFacetConfig = Lake.mkFacetJobConfig fun (x : Lake.Module) => x.recBuildDeps

def Lake.Module.clearOutputHashes (mod : Lake.Module) : IO PUnit

Remove cached file hashes of the module build outputs (in .hash files).

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.cacheOutputHashes (mod : Lake.Module) : IO PUnit

Cache the file hashes of the module build outputs in .hash files.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.recBuildLean (mod : Lake.Module) : Lake.FetchM (Lake.BuildJob Unit)

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.

def Lake.Module.leanArtsFacetConfig : Lake.ModuleFacetConfig Lake.Module.leanArtsFacet

The ModuleFacetConfig for the builtin leanArtsFacet.

Equations

• Lake.Module.leanArtsFacetConfig = Lake.mkFacetJobConfig fun (x : Lake.Module) => x.recBuildLean

def Lake.Module.oleanFacetConfig : Lake.ModuleFacetConfig Lake.Module.oleanFacet

The ModuleFacetConfig for the builtin oleanFacet.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.ileanFacetConfig : Lake.ModuleFacetConfig Lake.Module.ileanFacet

The ModuleFacetConfig for the builtin ileanFacet.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.cFacetConfig : Lake.ModuleFacetConfig Lake.Module.cFacet

The ModuleFacetConfig for the builtin cFacet.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.bcFacetConfig : Lake.ModuleFacetConfig Lake.Module.bcFacet

The ModuleFacetConfig for the builtin bcFacet.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.recBuildLeanCToOExport (self : Lake.Module) : Lake.FetchM (Lake.BuildJob System.FilePath)

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.

def Lake.Module.coExportFacetConfig : Lake.ModuleFacetConfig Lake.Module.coExportFacet

The ModuleFacetConfig for the builtin coExportFacet.

Equations

• Lake.Module.coExportFacetConfig = Lake.mkFacetJobConfig Lake.Module.recBuildLeanCToOExport

def Lake.Module.recBuildLeanCToONoExport (self : Lake.Module) : Lake.FetchM (Lake.BuildJob System.FilePath)

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.

def Lake.Module.coNoExportFacetConfig : Lake.ModuleFacetConfig Lake.Module.coNoExportFacet

The ModuleFacetConfig for the builtin coNoExportFacet.

Equations

• Lake.Module.coNoExportFacetConfig = Lake.mkFacetJobConfig Lake.Module.recBuildLeanCToONoExport

def Lake.Module.coFacetConfig : Lake.ModuleFacetConfig Lake.Module.coFacet

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

def Lake.Module.recBuildLeanBcToO (self : Lake.Module) : Lake.FetchM (Lake.BuildJob System.FilePath)

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.

def Lake.Module.bcoFacetConfig : Lake.ModuleFacetConfig Lake.Module.bcoFacet

The ModuleFacetConfig for the builtin bcoFacet.

Equations

• Lake.Module.bcoFacetConfig = Lake.mkFacetJobConfig Lake.Module.recBuildLeanBcToO

def Lake.Module.oExportFacetConfig : Lake.ModuleFacetConfig Lake.Module.oExportFacet

The ModuleFacetConfig for the builtin oExportFacet.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.oNoExportFacetConfig : Lake.ModuleFacetConfig Lake.Module.oNoExportFacet

The ModuleFacetConfig for the builtin oNoExportFacet.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.oFacetConfig : Lake.ModuleFacetConfig Lake.Module.oFacet

The ModuleFacetConfig for the builtin oFacet.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Module.recBuildDynlib (mod : Lake.Module) : Lake.FetchM (Lake.BuildJob Lake.Dynlib)

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.

def Lake.Module.dynlibFacetConfig : Lake.ModuleFacetConfig Lake.Module.dynlibFacet

The ModuleFacetConfig for the builtin dynlibFacet.

Equations

• Lake.Module.dynlibFacetConfig = Lake.mkFacetJobConfig Lake.Module.recBuildDynlib

def Lake.initModuleFacetConfigs : Lake.DNameMap Lake.ModuleFacetConfig

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.