Documentation

Lake.Config.Workspace

structure Lake.Workspace :

A Lake workspace -- the top-level package directory.

Instances For
    Equations
    @[implemented_by Lake.OpaqueWorkspace.unsafeGet]
    @[implemented_by Lake.OpaqueWorkspace.unsafeMk]
    @[inline]

    The path to the workspace's directory (i.e., the directory of the root package).

    Equations
    • self.dir = self.root.dir
    Instances For
      @[inline]

      The workspace's configuration.

      Equations
      • self.config = self.root.config.toWorkspaceConfig
      Instances For
        @[inline]

        The path to the workspace' Lake directory relative to dir.

        Equations
        • self.relLakeDir = self.root.relLakeDir
        Instances For
          @[inline]

          The full path to the workspace's Lake directory (e.g., .lake).

          Equations
          • self.lakeDir = self.root.lakeDir
          Instances For
            @[inline]

            The path to the workspace's remote packages directory relative to dir.

            Equations
            • self.relPkgsDir = self.root.relPkgsDir
            Instances For
              @[inline]

              The workspace's dir joined with its relPkgsDir.

              Equations
              • self.pkgsDir = self.root.pkgsDir
              Instances For
                @[inline]

                The workspace's Lake manifest.

                Equations
                • self.manifestFile = self.root.manifestFile
                Instances For

                  Add a package to the workspace.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline]

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

                    Equations
                    Instances For

                      Try to find a script in the workspace with the given name.

                      Equations
                      Instances For

                        Check if the module is local to any package in the workspace.

                        Equations
                        Instances For

                          Check if the module is buildable by any package in the workspace.

                          Equations
                          Instances For

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

                            Equations
                            Instances For

                              Locate the named, buildable, but not necessarily importable, module in the workspace.

                              Equations
                              Instances For

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

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For

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

                                    Equations
                                    Instances For

                                      Try to find a target configuration in the workspace with the given name.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Add a module facet to the workspace.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Try to find a module facet configuration in the workspace with the given name.

                                          Equations
                                          Instances For

                                            Add a package facet to the workspace.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

                                              Try to find a package facet configuration in the workspace with the given name.

                                              Equations
                                              Instances For

                                                Add a library facet to the workspace.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

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

                                                  Equations
                                                  Instances For

                                                    The workspace's binary directories (which are added to Path).

                                                    Equations
                                                    Instances For

                                                      The workspace's Lean library directories (which are added to LEAN_PATH).

                                                      Equations
                                                      Instances For

                                                        The workspace's source directories (which are added to LEAN_SRC_PATH).

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For

                                                          The workspace's shared library path (e.g., for --load-dynlib). This is added to the sharedLibPathEnvVar by lake env.

                                                          Equations
                                                          Instances For

                                                            The detected PATH of the environment augmented with the workspace's binDir and Lean and Lake installations' binDir.

                                                            Equations
                                                            • self.augmentedPath = self.binPath ++ self.lakeEnv.path
                                                            Instances For

                                                              The detected LEAN_PATH of the environment augmented with the workspace's leanPath and Lake's libDir.

                                                              Equations
                                                              • self.augmentedLeanPath = self.leanPath ++ self.lakeEnv.leanPath
                                                              Instances For

                                                                The detected LEAN_SRC_PATH of the environment augmented with the workspace's leanSrcPath and Lake's srcDir.

                                                                Equations
                                                                • self.augmentedLeanSrcPath = self.leanSrcPath ++ self.lakeEnv.leanSrcPath
                                                                Instances For
                                                                  Equations
                                                                  • self.augmentedSharedLibPath = self.sharedLibPath ++ self.lakeEnv.sharedLibPath
                                                                  Instances For

                                                                    The detected environment augmented with Lake's and the workspace's paths. These are the settings use by lake env / Lake.env to run executables.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For

                                                                      Remove all packages' build outputs (i.e., delete their build directories).

                                                                      Equations
                                                                      Instances For