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

source
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/v1`).

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

- noSystemCache : Bool

  Whether the system cache has been disabled (`LAKE_CACHE_DIR` is set but empty).

- lakeCache? : Option Cache

  The directory for the Lake cache. Customized by `LAKE_CACHE_DIR`.

  If `none`, no suitable system directory for the cache exists.

- lakeSystemCache? : Option Cache

  The directory for the Lake cache. Customized by `LAKE_CACHE_DIR`.

  Unlike `lakeCache?`, this excludes the toolchain directory from consideration.

  If `none`, no suitable system directory for the cache exists.

- cacheKey? : Option String

  The authentication key for cache uploads (i.e., `LAKE_CACHE_KEY`).

- cacheArtifactEndpoint? : Option String

  The base URL for artifact uploads and downloads from the cache (i.e., `LAKE_CACHE_ARTIFACT_ENDPOINT`).

- cacheRevisionEndpoint? : Option String

  The base URL for revision uploads and downloads from the cache (i.e., `LAKE_CACHE_REVISION_ENDPOINT`).

- 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 `ELAN_TOOLCHAIN` or, if none, Lake's `Lean.toolchain`.

Instances For

source
def Lake.instInhabitedEnv.default :
Env
Equations

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

Instances For

source
instance Lake.instInhabitedEnv :
Inhabited Env
Equations

- Lake.instInhabitedEnv = { default := Lake.instInhabitedEnv.default }

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

Instances For

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

Instances For

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

Instances For

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

Compute the system cache location from the process environment. If `none`, no system directory for workspace the cache exists.

Equations

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

Unset toolchain-specific environment variables.

Equations

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For