Documentation

Lake.Config.Monad

Lake Configuration Monads #

Definitions and helpers for interacting with the Lake configuration monads.

@[inline, reducible]
abbrev Lake.MonadLakeEnv (m : TypeType u) :

A monad equipped with a (read-only) detected environment for Lake.

Equations
Instances For
    @[inline, reducible]
    abbrev Lake.LakeEnvT (m : TypeType u_1) (α : Type) :
    Type u_1

    A transformer to equip a monad with a Lake.Env.

    Equations
    Instances For
      @[inline]
      def Lake.LakeEnvT.run {m : TypeType u_1} {α : Type} (env : Lake.Env) (self : Lake.LakeEnvT m α) :
      m α
      Equations
      Instances For
        @[inline, reducible]
        abbrev Lake.MonadWorkspace (m : TypeType u) :

        A monad equipped with a (read-only) Lake Workspace.

        Equations
        Instances For
          @[inline, reducible]
          abbrev Lake.MonadLake (m : TypeType u) :

          A monad equipped with a (read-only) Lake context.

          Equations
          Instances For
            @[inline]

            Make a Lake.Context from a Workspace.

            Equations
            Instances For
              Equations
              @[inline]
              Equations
              Instances For
                Equations
                Equations

                Workspace Helpers #

                @[inline]

                Get the workspace of the context.

                Equations
                • Lake.getWorkspace = read
                Instances For
                  @[inline]

                  Get the root package of the context's workspace.

                  Equations
                  Instances For
                    @[inline]
                    def Lake.findPackage? {m : TypeType u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lake.Name) :

                    Try to find a package within the workspace with the given name.

                    Equations
                    Instances For
                      @[inline]

                      Locate the named, buildable, importable, local module in the workspace.

                      Equations
                      Instances For
                        @[inline]

                        Try to find a Lean executable in the workspace with the given name.

                        Equations
                        Instances For
                          @[inline]

                          Try to find a Lean library in the workspace with the given name.

                          Equations
                          Instances For
                            @[inline]

                            Try to find an external library in the workspace with the given name.

                            Equations
                            Instances For
                              @[inline]

                              Get the paths added to LEAN_PATH by the context's workspace.

                              Equations
                              Instances For
                                @[inline]

                                Get the paths added to LEAN_SRC_PATH by the context's workspace.

                                Equations
                                Instances For
                                  @[inline]

                                  Get the paths added to the shared library path by the context's workspace.

                                  Equations
                                  Instances For
                                    @[inline]

                                    Get the augmented LEAN_PATH set by the context's workspace.

                                    Equations
                                    Instances For
                                      @[inline]

                                      Get the augmented LEAN_SRC_PATH set by the context's workspace.

                                      Equations
                                      Instances For
                                        @[inline]

                                        Get the augmented shared library path set by the context's workspace.

                                        Equations
                                        Instances For
                                          @[inline]

                                          Get the augmented environment variables set by the context's workspace.

                                          Equations
                                          Instances For

                                            Environment Helpers #

                                            @[inline]
                                            Equations
                                            • Lake.getLakeEnv = read
                                            Instances For
                                              @[inline]

                                              Get the LAKE_PACKAGE_URL_MAP for the Lake environment. Empty if none.

                                              Equations
                                              • Lake.getPkgUrlMap = (fun (x : Lake.Env) => x.pkgUrlMap) <$> Lake.getLakeEnv
                                              Instances For
                                                @[inline]

                                                Get the name of Elan toolchain for the Lake environment. Empty if none.

                                                Equations
                                                Instances For

                                                  Search Path Helpers #

                                                  @[inline]

                                                  Get the detected LEAN_PATH value of the Lake environment.

                                                  Equations
                                                  Instances For
                                                    @[inline]

                                                    Get the detected LEAN_SRC_PATH value of the Lake environment.

                                                    Equations
                                                    Instances For
                                                      @[inline]

                                                      Get the detected sharedLibPathEnvVar value of the Lake environment.

                                                      Equations
                                                      Instances For

                                                        Elan Install Helpers #

                                                        @[inline]

                                                        Get the detected Elan installation (if one).

                                                        Equations
                                                        • Lake.getElanInstall? = (fun (x : Lake.Env) => x.elan?) <$> Lake.getLakeEnv
                                                        Instances For
                                                          @[inline]

                                                          Get the root directory of the detected Elan installation (i.e., ELAN_HOME).

                                                          Equations
                                                          Instances For
                                                            @[inline]

                                                            Get the path of the elan binary in the detected Elan installation.

                                                            Equations
                                                            Instances For

                                                              Lean Install Helpers #

                                                              @[inline]

                                                              Get the detected Lean installation.

                                                              Equations
                                                              • Lake.getLeanInstall = (fun (x : Lake.Env) => x.lean) <$> Lake.getLakeEnv
                                                              Instances For
                                                                @[inline]

                                                                Get the root directory of the detected Lean installation.

                                                                Equations
                                                                Instances For
                                                                  @[inline]

                                                                  Get the Lean source directory of the detected Lean installation.

                                                                  Equations
                                                                  Instances For
                                                                    @[inline]

                                                                    Get the Lean library directory of the detected Lean installation.

                                                                    Equations
                                                                    Instances For
                                                                      @[inline]

                                                                      Get the C include directory of the detected Lean installation.

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]

                                                                        Get the system library directory of the detected Lean installation.

                                                                        Equations
                                                                        Instances For
                                                                          @[inline]

                                                                          Get the path of the lean binary in the detected Lean installation.

                                                                          Equations
                                                                          Instances For
                                                                            @[inline]

                                                                            Get the path of the leanc binary in the detected Lean installation.

                                                                            Equations
                                                                            Instances For
                                                                              @[inline]

                                                                              Get the path of the libleanshared library in the detected Lean installation.

                                                                              Equations
                                                                              Instances For
                                                                                @[inline]

                                                                                Get the path of the ar binary in the detected Lean installation.

                                                                                Equations
                                                                                Instances For
                                                                                  @[inline]

                                                                                  Get the path of C compiler in the detected Lean installation.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[inline]

                                                                                    Get the optional LEAN_CC compiler override of the detected Lean installation.

                                                                                    Equations
                                                                                    Instances For

                                                                                      Lake Install Helpers #

                                                                                      @[inline]

                                                                                      Get the detected Lake installation.

                                                                                      Equations
                                                                                      • Lake.getLakeInstall = (fun (x : Lake.Env) => x.lake) <$> Lake.getLakeEnv
                                                                                      Instances For
                                                                                        @[inline]

                                                                                        Get the root directory of the detected Lake installation (e.g., LAKE_HOME).

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline]

                                                                                          Get the source directory of the detected Lake installation.

                                                                                          Equations
                                                                                          Instances For
                                                                                            @[inline]

                                                                                            Get the Lean library directory of the detected Lake installation.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline]

                                                                                              Get the path of the lake binary in the detected Lake installation.

                                                                                              Equations
                                                                                              Instances For