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.

  • lakeCache : Cache

    The Lake cache.

  • 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 with the root coming first).

  • 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 _private.Lake.Config.Workspace.0.Lake.OpaqueWorkspace.unsafeGet]
    @[implemented_by _private.Lake.Config.Workspace.0.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]

            Whether the Lake artifact cache should be enabled by default for packages in the workspace.

            Equations
            Instances For

              Whether the Lake artifact cache should is enabled for workspace's root package.

              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]

                    Arguments to pass to lean for files outside a library (e.g., via lake lean).

                    Equations
                    Instances For
                      @[inline]

                      Options to pass to lean for files outside a library (e.g., via lake lean).

                      Equations
                      Instances For
                        @[inline]

                        Options to pass to the Lean server when editing Lean files outside a library.

                        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

                                            Returns the buildable module in the workspace whose source file is path.

                                            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 configuration. 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