Lake.Config.InstallPath

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.

Instances For

source

def Lake.LeanInstall.get (sysroot : Lake.FilePath) :

BaseIO Lake.LeanInstall

Construct the LeanInstall object for the given Lean sysroot.

Does the following:

Invokes lean to find out its githash and Lean.toolchain
Finds the ar and cc to use with Lean.
Computes the sub-paths of the Lean install.

For (1), if the invocation fails, githash and toolchain are 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.

Instances For

source

def Lake.LeanInstall.get.getGithash (sysroot : Lake.FilePath) :

BaseIO String

Instances For

source

def Lake.LeanInstall.get.findAr (sysroot : Lake.FilePath) :

BaseIO Lake.FilePath

Instances For

source

def Lake.LeanInstall.get.findCc (sysroot : Lake.FilePath) :

BaseIO (Lake.FilePath × Bool)

Instances For

source

def Lake.findLeanCmdInstall? (lean : optParam String "lean") :

BaseIO (Option Lake.LeanInstall)

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.

Instances For

source

def Lake.findLakeLeanJointHome? :

BaseIO (Option Lake.FilePath)

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.

Instances For

source

def Lake.lakePackageHome? (lake : Lake.FilePath) :

Option Lake.FilePath

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

Instances For

source

def Lake.findLeanInstall? :

BaseIO (Option Lake.LeanInstall)

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.

Instances For

source

def Lake.findLakeInstall? :

BaseIO (Option Lake.LakeInstall)

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 .

Instances For

source

def Lake.findInstall? :

BaseIO (Option Lake.ElanInstall × Option Lake.LeanInstall × Option Lake.LakeInstall)

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.

Instances For