Documentation

Lake.Config.Workspace

structure Lake.Workspace :

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

  • root : Package

    The root package of the workspace.

  • lakeEnv : Env

    The detected Lake.Env of the workspace.

  • lakeArgs? : Option (Array String)

    The CLI arguments Lake was run with. Used by lake update to perform a restart of Lake on a toolchain update. A value of none means that Lake is not restartable via the CLI.

  • packages : Array Package

    The packages within the workspace (in require declaration order).

  • packageMap : DNameMap NPackage

    Name-package map of packages within the workspace.

  • facetConfigs : DNameMap FacetConfig

    Configuration map of facets defined in the workspace.

Instances For
    @[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
    Instances For
      @[inline]

      The workspace's configuration.

      Equations
      Instances For
        @[inline]

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

        Equations
        Instances For
          @[inline]

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

          Equations
          Instances For
            @[inline]

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

            Equations
            Instances For
              @[inline]

              The workspace's dir joined with its relPkgsDir.

              Equations
              Instances For
                @[inline]

                The workspace's Lake manifest.

                Equations
                Instances For
                  @[inline]

                  The path to the workspace file used to configure automatic package overloads.

                  Equations
                  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
                                          def Lake.Workspace.findTargetDecl? (name : Lean.Name) (self : Workspace) :
                                          Option ((pkg : Package) × NConfigDecl pkg.name name)

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

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

                                            Add a facet to the workspace.

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

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

                                              Equations
                                              Instances For

                                                Add a module facet to the workspace.

                                                Equations
                                                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
                                                    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
                                                        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. On Windows, also adds the workspace shared library path.

                                                                    Equations
                                                                    Instances For

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

                                                                      Equations
                                                                      Instances For

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

                                                                        Equations
                                                                        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