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
    Equations
      Instances For
        Equations
          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
                                              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
                                                                                          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
                                                                                              Instances For

                                                                                                Add a facet to the workspace.

                                                                                                Equations
                                                                                                  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
                                                                                                                                          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
                                                                                                                                                              Instances For

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

                                                                                                                                                                Equations
                                                                                                                                                                  Instances For