Documentation

Lake.Build.Module

Module Build Definitions #

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.recFetchInput (mod : Module) :

FetchM (Job ModuleInput)

Parse the header of a Lean file from its source.

Equations

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

def Lake.Module.inputFacetConfig :

ModuleFacetConfig inputFacet

The ModuleFacetConfig for the builtin inputFacet.

Equations

Lake.Module.inputFacetConfig = Lake.mkFacetJobConfig Lake.Module.recFetchInput false

def Lake.Module.leanFacetConfig :

ModuleFacetConfig leanFacet

The ModuleFacetConfig for the builtin leanFacet.

Equations

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

def Lake.Module.headerFacetConfig :

ModuleFacetConfig headerFacet

The ModuleFacetConfig for the builtin headerFacet.

Equations

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

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

FetchM (Job (Array Module))

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

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

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.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.Module.importInfoFacetConfig :

ModuleFacetConfig importInfoFacet

The ModuleFacetConfig for the builtin importInfoFacet.

Equations

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

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

FetchM (Job ModuleExportInfo)

Computes the import artifacts and transitive import trace of a module's imports.

Equations

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

def Lake.Module.exportInfoFacetConfig :

ModuleFacetConfig exportInfoFacet

The ModuleFacetConfig for the builtin exportInfoFacet.

Equations

Lake.Module.exportInfoFacetConfig = Lake.mkFacetJobConfig Lake.Module.computeExportInfo false

def Lake.Module.importArtsFacetConfig :

ModuleFacetConfig importArtsFacet

The ModuleFacetConfig for the builtin importArtsFacet.

Equations

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

def Lake.Module.importAllArtsFacetConfig :

ModuleFacetConfig importAllArtsFacet

The ModuleFacetConfig for the builtin importAllArtsFacet.

Equations

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

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

Equations

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

def Lake.Module.setupFacetConfig :

ModuleFacetConfig setupFacet

The ModuleFacetConfig for the builtin setupFacet.

Equations

Lake.Module.setupFacetConfig = Lake.mkFacetJobConfig Lake.Module.recFetchSetup

def Lake.Module.depsFacetConfig :

ModuleFacetConfig depsFacet

The ModuleFacetConfig for the builtin depsFacet.

Equations

Lake.Module.depsFacetConfig = Lake.mkFacetJobConfig fun (mod : Lake.Module) => (fun (x : Lake.Job Lean.ModuleSetup) => x.toOpaque) <$> mod.setup.fetch

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

Remove any 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.

@[inline]

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

m (Option ModuleOutputArtifacts)

Equations

hashes.getArtifacts? = do let __do_lift ← Lake.getLakeCache liftM (Lake.ModuleOutputHashes.getArtifactsFrom?✝ __do_lift hashes)

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

ResolveArtifacts m ModuleOutputHashes ModuleOutputArtifacts

Equations

Lake.instResolveArtifactsModuleOutputHashesModuleOutputArtifactsOfMonadLakeEnvOfMonadLiftTBaseIOOfMonad = { resolveArtifacts? := Lake.ModuleOutputHashes.getArtifacts? }

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

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 Lake.Module.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.oleanServerFacetConfig :

ModuleFacetConfig oleanServerFacet

The ModuleFacetConfig for the builtin oleanServerFacet.

Equations

Lake.Module.oleanServerFacetConfig = Lake.mkFacetJobConfig (Lake.Module.fetchOLeanCore✝ "olean.server" (fun (x : Lake.ModuleOutputArtifacts) => x.oleanServer?) Lake.noServerOLeanError✝)

def Lake.Module.oleanPrivateFacetConfig :

ModuleFacetConfig oleanPrivateFacet

The ModuleFacetConfig for the builtin oleanPrivateFacet.

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.irFacetConfig :

ModuleFacetConfig irFacet

The ModuleFacetConfig for the builtin irFacet.

Equations

Lake.Module.irFacetConfig = Lake.mkFacetJobConfig (Lake.Module.fetchOLeanCore✝ "ir" (fun (x : Lake.ModuleOutputArtifacts) => x.ir?) Lake.noIRError✝)

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) true false

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

Top-Level Builds #

Definitions to support lake setup-file and lake lean builds.

def Lake.setupServerModule (fileName : String) (path : System.FilePath) (header? : Option Lean.ModuleHeader) :

FetchM (Job Lean.ModuleSetup)

Computes the module setup of edited Lean code for the Lean language server, building its imports and other dependencies. Used by lake setup-file.

Due to its exclusive use as a top-level build, it does not construct a proper trace state.

Equations

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

def Lake.prepareLeanCommand (leanFile : System.FilePath) (moreArgs : Array String := #[]) :

FetchM (Job IO.Process.SpawnArgs)

Computes the arguments required to evaluate the Lean file with lean, building its imports and other dependencies. Used by lake lean.

Due to its exclusive use as a top-level build, it does not construct a proper trace state.

Equations

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

def Lake.prepareLeanCommand.mkArgs (leanFile : System.FilePath) (setup : Lean.ModuleSetup) (cfgArgs : Array String) :

JobM (Array String)

Equations

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

def Lake.prepareLeanCommand.mkSpawnArgs (moreArgs : Array String := #[]) (leanFile : System.FilePath) (setup : Lean.ModuleSetup) (cfgArgs : Array String) :

JobM IO.Process.SpawnArgs

Equations

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