Documentation

Lake.Config.InstallPath

Data Structures #

Standard path of elan in a Elan installation.

Equations
Instances For

    Information about the local Elan setup.

    Instances For
      Equations

      Standard path of lean in a Lean installation.

      Equations
      Instances For

        Standard path of leanc in a Lean installation.

        Equations
        Instances For

          Standard path of llvm-ar in a Lean installation.

          Equations
          Instances For

            Standard path of clang in a Lean installation.

            Equations
            Instances For

              Standard path of libleanshared in a Lean installation.

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

                Path information about the local Lean installation.

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

                  A SearchPath including the Lean installation's shared library directories (i.e., the system library and Lean library directories).

                  Equations
                  Instances For

                    The LEAN_CC of the Lean installation.

                    Equations
                    Instances For

                      Standard path of lake in a Lake installation.

                      Equations
                      Instances For

                        Path information about the local Lake installation.

                        Instances For
                          Equations

                          Construct a Lake installation co-located with the specified Lean installation.

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

                            Detection Functions #

                            Attempt to detect a Elan installation by checking the ELAN_HOME environment variable for a installation location.

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

                              Attempt to find the sysroot of the given lean command (if it exists) by calling lean --print-prefix and returning the path it prints. Defaults to trying the lean in PATH.

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

                                Construct the LeanInstall object for the given Lean sysroot.

                                Does the following:

                                1. Find lean's githash.
                                2. Finds the ar and cc to use with Lean.
                                3. Computes the sub-paths of the Lean install.

                                For (1), If lake is not-collocated with lean, invoke lean --githash; otherwise, use Lake's Lean.githash. If the invocation fails, githash is set to the empty string.

                                For (2), if LEAN_AR or LEAN_CC are defined, it uses those paths. Otherwise, if Lean is packaged with an llvm-ar and/or clang, use them. If not, use the ar and/or cc in the system's PATH. This last step is needed because internal builds of Lean do not bundle these tools (unlike user-facing releases).

                                We also track whether LEAN_CC was set to determine whether it should be set in the future for lake env. This is because if LEAN_CC was not set, it needs to remain not set for leanc to work. Even setting it to the bundled compiler will break leanc -- see leanprover/lean4#1281.

                                For (3), it assumes that the Lean installation is organized the normal way. That is, with its binaries located in /bin, its Lean libraries in /lib/lean, and its system libraries in /lib.

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

                                        Attempt to detect the installation of the given lean command by calling findLeanCmdHome?. See LeanInstall.get for how it assumes the Lean install is organized.

                                        Equations
                                        Instances For

                                          Check if the running Lake's executable is co-located with Lean, and, if so, try to return their joint home by assuming they are both located at /bin.

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

                                            Attempt to detect a specified Lake's executable's home by assuming the executable is located at /build/bin/lake.

                                            Equations
                                            Instances For

                                              Attempt to detect Lean's installation by first checking the LEAN_SYSROOT environment variable and then by trying findLeanCmdHome?. See LeanInstall.get for how it assumes the Lean install is organized.

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

                                                Attempt to detect Lake's installation by first checking the LAKE_HOME environment variable and then by trying the lakePackageHome? of the running executable.

                                                It assumes that the Lake installation is organized the same way it is built. That is, with its binary located at /build/bin/lake and its static library and .olean files in /build/lib, and its source files located directly in .

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

                                                  Attempt to automatically detect an Elan, Lake, and Lean installation.

                                                  First, it calls findElanInstall? to detect a Elan installation. Then it attempts to detect if Lake and Lean are part of a single installation where the lake executable is co-located with the lean executable (i.e., they are in the same directory). If Lean and Lake are not co-located, Lake will attempt to find the their installations separately by calling findLeanInstall? and findLakeInstall?.

                                                  When co-located, Lake will assume that Lean and Lake's binaries are located in /bin, their Lean libraries in /lib/lean, Lean's source files in /src/lean, and Lake's source files in /src/lean/lake, following the pattern of a regular Lean toolchain.

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