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.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.importsFacetConfig : ModuleFacetConfig importsFacet

The ModuleFacetConfig for the builtin importsFacet.

Equations

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

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.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.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.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) : IO PUnit

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) : 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.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.coExportFacetConfig : ModuleFacetConfig coExportFacet

The ModuleFacetConfig for the builtin coExportFacet.

Equations

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

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