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.

def Lake.Module.recFetchInput (mod : Module) : FetchM (Job ModuleInput)

Parse the header of a Lean file from its source.

def Lake.Module.inputFacetConfig : ModuleFacetConfig inputFacet

The ModuleFacetConfig for the builtin inputFacet.

def Lake.Module.leanFacetConfig : ModuleFacetConfig leanFacet

The ModuleFacetConfig for the builtin leanFacet.

def Lake.Module.headerFacetConfig : ModuleFacetConfig headerFacet

The ModuleFacetConfig for the builtin headerFacet.

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

Compute an Array of a module's direct local imports from its header.

def Lake.Module.importsFacetConfig : ModuleFacetConfig importsFacet

The ModuleFacetConfig for the builtin importsFacet.

structure Lake.ModuleImportData : Type

• 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))

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

Recursively compute a module's transitive imports.

def Lake.Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet

The ModuleFacetConfig for the builtin transImportsFacet.

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

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

Recursively compute a module's precompiled imports.

def Lake.Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet

The ModuleFacetConfig for the builtin precompileImportsFacet.

def Lake.fetchImportLibs (mods : Array Module) : FetchM (Job (Array Dynlib))

For internal use.

Fetches the library dynlibs of a list of non-local imports. Modules are loaded as part of their whole library.

def Lake.Module.recFetchSetup (mod : Module) : FetchM (Job Lean.ModuleSetup)

Recursively build a module's dependencies, including:

• Transitive local imports
• Shared libraries (e.g., extern_lib targets or precompiled modules)
• extraDepTargets of its library

def Lake.Module.setupFacetConfig : ModuleFacetConfig setupFacet

The ModuleFacetConfig for the builtin setupFacet.

def Lake.Module.depsFacetConfig : ModuleFacetConfig depsFacet

The ModuleFacetConfig for the builtin depsFacet.

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

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

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

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

@[inline]

def Lake.ModuleOutputHashes.getArtifacts? {m : Type → Type u_1} [MonadLakeEnv m] [MonadLiftT BaseIO m] [Monad m] (hashes : ModuleOutputHashes) : m (Option ModuleOutputArtifacts)

instance Lake.instResolveArtifactsModuleOutputHashesModuleOutputArtifactsOfMonadLakeEnvOfMonadLiftTBaseIOOfMonad {m : Type → Type u_1} [MonadLakeEnv m] [MonadLiftT BaseIO m] [Monad m] : ResolveArtifacts m ModuleOutputHashes ModuleOutputArtifacts

def Lake.Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifacts)

Recursively build a Lean module. Fetch its dependencies and then elaborate the Lean source file, producing all possible artifacts (e.g., .olean, .ilean, .c, .bc).

def Lake.Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet

The ModuleFacetConfig for the builtin leanArtsFacet.

def Lake.Module.oleanFacetConfig : ModuleFacetConfig oleanFacet

The ModuleFacetConfig for the builtin oleanFacet.

def Lake.Module.oleanServerFacetConfig : ModuleFacetConfig oleanServerFacet

The ModuleFacetConfig for the builtin oleanServerFacet.

def Lake.Module.oleanPrivateFacetConfig : ModuleFacetConfig oleanPrivateFacet

The ModuleFacetConfig for the builtin oleanPrivateFacet.

def Lake.Module.ileanFacetConfig : ModuleFacetConfig ileanFacet

The ModuleFacetConfig for the builtin ileanFacet.

def Lake.Module.cFacetConfig : ModuleFacetConfig cFacet

The ModuleFacetConfig for the builtin cFacet.

def Lake.Module.bcFacetConfig : ModuleFacetConfig bcFacet

The ModuleFacetConfig for the builtin bcFacet.

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.

def Lake.Module.coExportFacetConfig : ModuleFacetConfig coExportFacet

The ModuleFacetConfig for the builtin coExportFacet.

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.

def Lake.Module.coNoExportFacetConfig : ModuleFacetConfig coNoExportFacet

The ModuleFacetConfig for the builtin coNoExportFacet.

def Lake.Module.coFacetConfig : ModuleFacetConfig coFacet

The ModuleFacetConfig for the builtin coFacet.

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

Recursively build the module's object file from its bitcode file produced by lean.

def Lake.Module.bcoFacetConfig : ModuleFacetConfig bcoFacet

The ModuleFacetConfig for the builtin bcoFacet.

def Lake.Module.oExportFacetConfig : ModuleFacetConfig oExportFacet

The ModuleFacetConfig for the builtin oExportFacet.

def Lake.Module.oNoExportFacetConfig : ModuleFacetConfig oNoExportFacet

The ModuleFacetConfig for the builtin oNoExportFacet.

def Lake.Module.oFacetConfig : ModuleFacetConfig oFacet

The ModuleFacetConfig for the builtin oFacet.

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

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

def Lake.Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet

The ModuleFacetConfig for the builtin dynlibFacet.

def Lake.Module.initFacetConfigs : DNameMap ModuleFacetConfig

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

@[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).

Definitions to support lake setup-file builds.

def Lake.buildImportsAndDeps (leanFile : System.FilePath) (imports : Array Lean.Import) : FetchM (Job ModuleDeps)

Builds an Array of module imports for a Lean file. Used by lake setup-file to build modules for the Lean server and by lake lean to build the imports of a file. Returns the dynlibs and plugins built (so they can be loaded by Lean).