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

• lake : Lake.LakeInstall

  The Lake installation of the environment.

• lean : Lake.LeanInstall

  The Lean installation of the environment.

• elan? : Option Lake.ElanInstall

  The Elan installation (if any) of the environment.

• initToolchain : String

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

• initLeanPath : Lake.SearchPath

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

• initLeanSrcPath : Lake.SearchPath

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

• initSharedLibPath : Lake.SearchPath

  The initial shared library search path of the environment.

• initPath : Lake.SearchPath

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

A Lake environment.

instance Lake.instInhabitedEnv : Inhabited Lake.Env

instance Lake.instReprEnv : Repr Lake.Env

def Lake.Env.compute (lake : Lake.LakeInstall) (lean : Lake.LeanInstall) (elan? : Option Lake.ElanInstall) : BaseIO Lake.Env

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

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

The preferred toolchain of the environment. May be empty. Tries env.initToolchain first and then Lake's Lean.toolchain.

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

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

def Lake.Env.leanPath (env : Lake.Env) : Lake.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.

def Lake.Env.leanSrcPath (env : Lake.Env) : Lake.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 abd Lean installations.

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

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

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

Environment variable settings based only on the Elan/Lean/Lake installations.

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

Environment variable settings for the Lake.Env.

def Lake.Env.leanSearchPath (env : Lake.Env) : Lake.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 /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).