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 shared libraries in a Lean installation.

              Equations
              Instances For

                libleanshared file name.

                Equations
                Instances For

                  Init shared library file name.

                  Equations
                  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
                        • self.leanCc? = if self.customCc = true then some self.cc.toString else none
                        Instances For

                          Lake executable file name.

                          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
                              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 <lean-sysroot>/bin, its Lean libraries in <lean-sysroot>/lib/lean, and its system libraries in <lean-sysroot>/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 <home>/bin.

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

                                                Get the root of Lake's installation by assuming the executable is located at <lake-home>/.lake/build/bin/lake.

                                                Equations
                                                • Lake.lakeBuildHome? lake = do let __do_liftlake.parent let __do_lift__do_lift.parent let __do_lift__do_lift.parent __do_lift.parent
                                                Instances For

                                                  Heuristically validate that getLakeBuildHome? is a proper Lake installation by check for Lake.olean in the installation's lib directory.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  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 lakeBuildHome? of the running executable, then trying the LAKE_HOME environment variable.

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

                                                      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 <sysroot>/bin, their Lean libraries in <sysroot>/lib/lean, Lean's source files in <sysroot>/src/lean, and Lake's source files in <sysroot>/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