Documentation

Lake.Config.Env

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 :

A Lake environment.

  • The Lake installation of the environment.

  • The Lean installation of the environment.

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

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

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

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

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

    Equations
      Instances For
        @[macro_inline]
        Equations
          Instances For

            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
              Instances For

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

                Equations
                  Instances For

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

                    Equations
                      Instances For

                        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
                          Instances For

                            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
                              Instances For

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

                                Equations
                                  Instances For

                                    Unset toolchain-specific environment variables.

                                    Equations
                                      Instances For

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

                                        Equations
                                          Instances For

                                            Environment variable settings for the Lake.Env.

                                            Equations
                                              Instances For

                                                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
                                                  Instances For