Documentation

Lake.Config.Monad

Lake Configuration Monads #

Definitions and helpers for interacting with the Lake configuration monads.

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

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

Equations
Instances For
    @[reducible, inline]
    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
        class Lake.MonadWorkspace (m : TypeType u) :

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

        Instances
          Equations
          • Lake.instMonadWorkspaceOfMonadReaderOfWorkspace = { getWorkspace := read }
          Equations
          • Lake.instMonadWorkspaceOfMonadStateOfWorkspace = { getWorkspace := get }
          @[reducible, inline]
          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
              • self.workspace = self.opaqueWs.get
              Instances For
                Equations
                • Lake.instMonadWorkspaceOfMonadLakeOfFunctor = { getWorkspace := (fun (x : Lake.Context) => x.workspace) <$> read }
                Equations
                • Lake.instMonadLakeEnvOfMonadWorkspaceOfFunctor = { read := (fun (x : Lake.Workspace) => x.lakeEnv) <$> Lake.getWorkspace }

                Workspace Helpers #

                @[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
                                • Lake.getSharedLibPath = (fun (x : Lake.Workspace) => x.sharedLibPath) <$> Lake.getWorkspace
                                Instances For
                                  @[inline]

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

                                  Equations
                                  • Lake.getAugmentedLeanPath = (fun (x : Lake.Workspace) => x.augmentedLeanPath) <$> Lake.getWorkspace
                                  Instances For
                                    @[inline]

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

                                    Equations
                                    • Lake.getAugmentedLeanSrcPath = (fun (x : Lake.Workspace) => x.augmentedLeanSrcPath) <$> Lake.getWorkspace
                                    Instances For
                                      @[inline]

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

                                      Equations
                                      • Lake.getAugmentedSharedLibPath = (fun (x : Lake.Workspace) => x.augmentedSharedLibPath) <$> Lake.getWorkspace
                                      Instances For
                                        @[inline]

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

                                        Equations
                                        • Lake.getAugmentedEnv = (fun (x : Lake.Workspace) => x.augmentedEnvVars) <$> Lake.getWorkspace
                                        Instances For

                                          Environment Helpers #

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

                                            Get the LAKE_NO_CACHE/--no-cache Lake configuration.

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

                                              Get whether the LAKE_NO_CACHE/--no-cache Lake configuration is NOT set.

                                              Equations
                                              • Lake.getTryCache = (fun (x : Lake.Env) => !x.noCache) <$> Lake.getLakeEnv
                                              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
                                                  • Lake.getElanToolchain = (fun (x : Lake.Env) => x.toolchain) <$> Lake.getLakeEnv
                                                  Instances For

                                                    Search Path Helpers #

                                                    @[inline]

                                                    Get the detected LEAN_PATH value of the Lake environment.

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

                                                      Get the detected LEAN_SRC_PATH value of the Lake environment.

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

                                                        Get the detected sharedLibPathEnvVar value of the Lake environment.

                                                        Equations
                                                        • Lake.getEnvSharedLibPath = (fun (x : Lake.Env) => x.sharedLibPath) <$> Lake.getLakeEnv
                                                        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