Documentation

Lake.Config.Workspace

structure Lake.Workspace :

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

Instances For
    @[implemented_by Lake.OpaqueWorkspace.unsafeMk]
    Equations
    @[implemented_by Lake.OpaqueWorkspace.unsafeGet]
    @[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 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

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

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

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

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