Lake's Environment

Definitions related to a Lake environment. A Lake environment is computed on Lake's startup from user-specified CLI options and the process environment.

structure Lake.Env : Type

A Lake environment.

• lake : LakeInstall

  The Lake installation of the environment.

• lean : LeanInstall

  The Lean installation of the environment.

• elan? : Option ElanInstall

  The Elan installation (if any) of the environment.

• reservoirApiUrl : String

  The Reservoir API endpoint URL (e.g., https://reservoir.lean-lang.org/api).

• githashOverride : String

  Overrides the detected Lean's githash as the string Lake uses for Lean traces.

• pkgUrlMap : Lean.NameMap String

  A name-to-URL mapping of URL overrides for the named packages.

• noCache : Bool

  Whether to disable downloading build caches for packages. Set via LAKE_NO_CACHE. Can be overridden on a per-command basis with--try-cache.

• enableArtifactCache : Bool

  Whether the Lake artifact cache should be enabled by default (i.e., LAKE_ARTIFACT_CACHE).

• lakeCache : Cache

  The directory of the Lake cache. Set by LAKE_CACHE_DIR. If none, the cache is disabled.

• initToolchain : String

  The initial Elan toolchain of the environment (i.e., ELAN_TOOLCHAIN).

• initLeanPath : System.SearchPath

  The initial Lean library search path of the environment (i.e., LEAN_PATH).

• initLeanSrcPath : System.SearchPath

  The initial Lean source search path of the environment (i.e., LEAN_SRC_PATH).

• initSharedLibPath : System.SearchPath

  The initial shared library search path of the environment.

• initPath : System.SearchPath

  The initial binary search path of the environment (i.e., PATH).

• toolchain : String

  The preferred toolchain of the environment. May be empty.

  Either initToolchain or, if none, Lake's Lean.toolchain.

instance Lake.instInhabitedEnv : Inhabited Env

Equations

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

def Lake.getUserHome? : BaseIO (Option System.FilePath)

Returns the home directory of the current user (if possible).

Equations

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

def Lake.getSystemCacheHome? : BaseIO (Option System.FilePath)

Returns the system directory that can be used to store caches (if one exists).

Equations

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

def Lake.Env.computeToolchain : BaseIO String

Compute the Lean toolchain string used by Lake from the process environment.

Equations

• Lake.Env.computeToolchain = do let __do_lift ← IO.getEnv "ELAN_TOOLCHAIN" pure (__do_lift.getD Lean.toolchain)

def Lake.Env.computeCache (elan? : Option ElanInstall) (toolchain : String) : BaseIO Cache

Compute the cache location used by Lake from the process environment. May be disabled.

Equations

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

def Lake.Env.compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstall) (noCache : Option Bool := none) : EIO String Env

Compute a Lake.Env object from the given installs and the set environment variables.

Equations

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

def Lake.Env.compute.computePkgUrlMap : EIO String (Lean.NameMap String)

Equations

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

@[macro_inline]

def Lake.Env.compute.getUrlD (var default : String) : EIO String String

Equations

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

def Lake.Env.leanGithash (env : Env) : String

The string Lake uses to identify Lean in traces. Either the environment-specified LEAN_GITHASH or the detected Lean's githash.

The override allows one to replace the Lean version used by a library (e.g., Mathlib) without completely rebuilding it, which is useful for testing custom builds of Lean.

Equations

• env.leanGithash = if env.githashOverride.isEmpty = true then env.lean.githash else env.githashOverride

def Lake.Env.path (env : Env) : System.SearchPath

The binary search path of the environment (i.e., PATH). Combines the initial path of the environment with that of the Lake installation.

Equations

• env.path = if env.lake.binDir = env.lean.binDir then env.lean.binDir :: env.initPath else env.lake.binDir :: env.lean.binDir :: env.initPath

def Lake.Env.leanPath (env : Env) : System.SearchPath

The Lean library search path of the environment (i.e., LEAN_PATH). Combines the initial path of the environment with that of the Lake installation.

Equations

• env.leanPath = env.lake.libDir :: env.initLeanPath

def Lake.Env.leanSrcPath (env : Env) : System.SearchPath

The Lean source search path of the environment (i.e., LEAN_SRC_PATH). Combines the initial path of the environment with that of the Lake and Lean installations.

Equations

• env.leanSrcPath = env.lake.srcDir :: env.initLeanSrcPath

def Lake.Env.sharedLibPath (env : Env) : System.SearchPath

The shared library search path of the environment. Combines the initial path of the environment with that of the Lean installation.

Equations

• env.sharedLibPath = env.lean.sharedLibPath ++ env.initSharedLibPath

def Lake.Env.noToolchainVars : Array (String × Option String)

Unset toolchain-specific environment variables.

Equations

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

def Lake.Env.baseVars (env : Env) : Array (String × Option String)

Environment variable settings that are not augmented by a Lake workspace.

Equations

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

def Lake.Env.vars (env : Env) : Array (String × Option String)

Environment variable settings for the Lake.Env.

Equations

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

def Lake.Env.leanSearchPath (env : Env) : System.SearchPath

The default search path the Lake executable uses when interpreting package configuration files.

In order to use the Lean stdlib (e.g., Init), the executable needs the search path to include the directory with the stdlib's .olean files (e.g., from <lean-sysroot>/lib/lean). In order to use Lake's modules as well, the search path also needs to include Lake's .olean files (e.g., from build).

While this can be done by having the user augment LEAN_PATH with the necessary directories, Lake also intelligently augments the initial search path with the .olean directories of the provided Lean and Lake installations.

See findInstall? for more information on how Lake determines those directories. If everything is configured as expected, the user will not need to augment LEAN_PATH. Otherwise, they will need to provide Lake with more information (either through LEAN_PATH or through other options).

Equations

• env.leanSearchPath = env.lake.libDir :: env.lean.leanLibDir :: env.leanPath