Documentation

Lake.Build.Module

Module Facet Builds #

Build function definitions for a module's builtin facets.

@[deprecated "Deprecated without replacement" (since := "2025-03-28")]

def Lake.recBuildExternDynlibs (pkgs : Array Package) :

FetchM (Array (Job 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 : Module) :

FetchM (Job (Array 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 :

ModuleFacetConfig importsFacet

The ModuleFacetConfig for the builtin importsFacet.

Equations

Lake.Module.importsFacetConfig = Lake.mkFacetJobConfig Lake.Module.recParseImports false

structure Lake.ModuleImportData :

module : Module
transImports : Job (Array Module)
includeSelf : Bool

@[inline]

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

FetchM (Job (Array Module))

Equations

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

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

FetchM (Job (Array 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 :

ModuleFacetConfig transImportsFacet

The ModuleFacetConfig for the builtin transImportsFacet.

Equations

Lake.Module.transImportsFacetConfig = Lake.mkFacetJobConfig Lake.Module.recComputeTransImports false

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

FetchM (Job (Array Module))

Equations

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

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

FetchM (Job (Array Module))

Recursively compute a module's precompiled imports.

Equations

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

def Lake.Module.precompileImportsFacetConfig :

ModuleFacetConfig precompileImportsFacet

The ModuleFacetConfig for the builtin precompileImportsFacet.

Equations

Lake.Module.precompileImportsFacetConfig = Lake.mkFacetJobConfig Lake.Module.recComputePrecompileImports false

def Lake.fetchExternLibs (pkgs : Array Package) :

FetchM (Job (Array Dynlib))

Fetch dynlibs of the packages' external libraries. For internal use.

Equations

Lake.fetchExternLibs pkgs = Lake.Job.collectArray <$> Array.flatMapM (fun (x : Lake.Package) => Array.mapM (fun (x : Lake.ExternLib) => x.dynlib.fetch) x.externLibs) pkgs

@[inline]

def Lake.fetchImportLibs (mods : Array Module) :

FetchM (Job (Array Dynlib))

Fetch the dynlibs of a list of imports. For internal use.

Equations

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

def Lake.computeModuleDeps (impLibs externLibs dynlibs plugins : Array Dynlib) :

Equations

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

def Lake.Module.recBuildDeps (mod : Module) :

FetchM (Job ModuleDeps)

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 :

ModuleFacetConfig depsFacet

The ModuleFacetConfig for the builtin depsFacet.

Equations

Lake.Module.depsFacetConfig = Lake.mkFacetJobConfig Lake.Module.recBuildDeps

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

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 : Module) :

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 : Module) :

FetchM (Job 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 :

ModuleFacetConfig leanArtsFacet

The ModuleFacetConfig for the builtin leanArtsFacet.

Equations

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

def Lake.Module.oleanFacetConfig :

ModuleFacetConfig oleanFacet

The ModuleFacetConfig for the builtin oleanFacet.

Equations

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

def Lake.Module.ileanFacetConfig :

ModuleFacetConfig ileanFacet

The ModuleFacetConfig for the builtin ileanFacet.

Equations

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

def Lake.Module.cFacetConfig :

ModuleFacetConfig cFacet

The ModuleFacetConfig for the builtin cFacet.

Equations

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

def Lake.Module.bcFacetConfig :

ModuleFacetConfig 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 : Module) :

FetchM (Job 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 :

ModuleFacetConfig coExportFacet

The ModuleFacetConfig for the builtin coExportFacet.

Equations

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

def Lake.Module.recBuildLeanCToONoExport (self : Module) :

FetchM (Job 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 :

ModuleFacetConfig coNoExportFacet

The ModuleFacetConfig for the builtin coNoExportFacet.

Equations

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

def Lake.Module.coFacetConfig :

ModuleFacetConfig 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 : Module) :

FetchM (Job 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 :

ModuleFacetConfig bcoFacet

The ModuleFacetConfig for the builtin bcoFacet.

Equations

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

def Lake.Module.oExportFacetConfig :

ModuleFacetConfig oExportFacet

The ModuleFacetConfig for the builtin oExportFacet.

Equations

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

def Lake.Module.oNoExportFacetConfig :

ModuleFacetConfig oNoExportFacet

The ModuleFacetConfig for the builtin oNoExportFacet.

Equations

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

def Lake.Module.oFacetConfig :

ModuleFacetConfig 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 : Module) :

FetchM (Job Dynlib)

Recursively build the shared library of a module (e.g., for --load-dynlib or --plugin).

Equations

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

def Lake.Module.dynlibFacetConfig :

ModuleFacetConfig dynlibFacet

The ModuleFacetConfig for the builtin dynlibFacet.

Equations

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

def Lake.Module.initFacetConfigs :

DNameMap ModuleFacetConfig

A name-configuration map for the initial set of Lake module facets (e.g., imports, c, o, dynlib).

Equations

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

@[reducible, inline]

abbrev Lake.initModuleFacetConfigs :

DNameMap ModuleFacetConfig

A name-configuration map for the initial set of Lake module facets (e.g., imports, c, o, dynlib).

Equations

Lake.initModuleFacetConfigs = Lake.Module.initFacetConfigs