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.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
            • Lake.instMonadLakeEnv = { read := (fun x => x.lakeEnv) <$> read }

            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
              • Lake.getRootPackage = (fun x => x.root) <$> read
              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 module in the workspace (if it is local to it).

                  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 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 => x.elan?) <$> Lake.getLakeEnv
                                                  Instances For
                                                    @[inline]

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

                                                    Equations
                                                    • Lake.getElanHome? = (fun x => Option.map (fun x => x.home) x) <$> Lake.getElanInstall?
                                                    Instances For
                                                      @[inline]

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

                                                      Equations
                                                      • Lake.getElan? = (fun x => Option.map (fun x => x.elan) x) <$> Lake.getElanInstall?
                                                      Instances For

                                                        Lean Install Helpers #

                                                        @[inline]

                                                        Get the detected Lean installation.

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

                                                          Get the root directory of the detected Lean installation.

                                                          Equations
                                                          • Lake.getLeanSysroot = (fun x => x.sysroot) <$> Lake.getLeanInstall
                                                          Instances For
                                                            @[inline]

                                                            Get the Lean source directory of the detected Lean installation.

                                                            Equations
                                                            • Lake.getLeanSrcDir = (fun x => x.srcDir) <$> Lake.getLeanInstall
                                                            Instances For
                                                              @[inline]

                                                              Get the Lean library directory of the detected Lean installation.

                                                              Equations
                                                              • Lake.getLeanLibDir = (fun x => x.leanLibDir) <$> Lake.getLeanInstall
                                                              Instances For
                                                                @[inline]

                                                                Get the C include directory of the detected Lean installation.

                                                                Equations
                                                                • Lake.getLeanIncludeDir = (fun x => x.includeDir) <$> Lake.getLeanInstall
                                                                Instances For
                                                                  @[inline]

                                                                  Get the system library directory of the detected Lean installation.

                                                                  Equations
                                                                  • Lake.getLeanSystemLibDir = (fun x => x.systemLibDir) <$> Lake.getLeanInstall
                                                                  Instances For
                                                                    @[inline]

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

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

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

                                                                      Equations
                                                                      • Lake.getLeanc = (fun x => x.leanc) <$> Lake.getLeanInstall
                                                                      Instances For
                                                                        @[inline]

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

                                                                        Equations
                                                                        • Lake.getLeanSharedLib = (fun x => x.sharedLib) <$> Lake.getLeanInstall
                                                                        Instances For
                                                                          @[inline]

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

                                                                          Equations
                                                                          • Lake.getLeanAr = (fun x => x.ar) <$> Lake.getLeanInstall
                                                                          Instances For
                                                                            @[inline]

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

                                                                            Equations
                                                                            • Lake.getLeanCc = (fun x => x.cc) <$> Lake.getLeanInstall
                                                                            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 => x.lake) <$> Lake.getLakeEnv
                                                                                Instances For
                                                                                  @[inline]

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

                                                                                  Equations
                                                                                  • Lake.getLakeHome = (fun x => x.home) <$> Lake.getLakeInstall
                                                                                  Instances For
                                                                                    @[inline]

                                                                                    Get the source directory of the detected Lake installation.

                                                                                    Equations
                                                                                    • Lake.getLakeSrcDir = (fun x => x.srcDir) <$> Lake.getLakeInstall
                                                                                    Instances For
                                                                                      @[inline]

                                                                                      Get the Lean library directory of the detected Lake installation.

                                                                                      Equations
                                                                                      • Lake.getLakeLibDir = (fun x => x.libDir) <$> Lake.getLakeInstall
                                                                                      Instances For
                                                                                        @[inline]

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

                                                                                        Equations
                                                                                        • Lake.getLake = (fun x => x.lake) <$> Lake.getLakeInstall
                                                                                        Instances For