def Lake.leanExe (sysroot : Lake.FilePath) : Lake.FilePath

Standard path of lean in a Lean installation.

def Lake.leancExe (sysroot : Lake.FilePath) : Lake.FilePath

Standard path of leanc in a Lean installation.

def Lake.leanArExe (sysroot : Lake.FilePath) : Lake.FilePath

Standard path of llvm-ar in a Lean installation.

def Lake.leanCcExe (sysroot : Lake.FilePath) : Lake.FilePath

Standard path of clang in a Lean installation.

def Lake.leanSharedLib (sysroot : Lake.FilePath) : Lake.FilePath

Standard path of libleanshared in a Lean installation.

structure Lake.LeanInstall : Type

• sysroot : Lake.FilePath
• githash : String
• srcDir : Lake.FilePath
• leanLibDir : Lake.FilePath
• includeDir : Lake.FilePath
• systemLibDir : Lake.FilePath
• binDir : Lake.FilePath
• lean : Lake.FilePath
• leanc : Lake.FilePath
• sharedLib : Lake.FilePath
• ar : Lake.FilePath
• cc : Lake.FilePath
• customCc : Bool

Path information about the local Lean installation.

instance Lake.instInhabitedLeanInstall : Inhabited Lake.LeanInstall

instance Lake.instReprLeanInstall : Repr Lake.LeanInstall

def Lake.LeanInstall.sharedLibPath (self : Lake.LeanInstall) : Lake.SearchPath

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

def Lake.LeanInstall.leanCc? (self : Lake.LeanInstall) : Option String

The LEAN_CC of the Lean installation.

def Lake.lakeExe (buildHome : Lake.FilePath) : Lake.FilePath

Standard path of lake in a Lake installation.

structure Lake.LakeInstall : Type

• home : Lake.FilePath
• srcDir : Lake.FilePath
• binDir : Lake.FilePath
• libDir : Lake.FilePath
• lake : Lake.FilePath

Path information about the local Lake installation.

instance Lake.instInhabitedLakeInstall : Inhabited Lake.LakeInstall

instance Lake.instReprLakeInstall : Repr Lake.LakeInstall

def Lake.findLeanSysroot? (lean : optParam String "lean") : BaseIO (Option Lake.FilePath)

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

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

Construct the LeanInstall object for the given Lean sysroot.

Does the following:

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

For (1), 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.

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

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

def Lake.LeanInstall.get.findCc (sysroot : Lake.FilePath) : BaseIO (Lake.FilePath × Bool)

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

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

def Lake.findLakeLeanJointHome? : BaseIO (Option Lake.FilePath)

Check if 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.

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

Try to get Lake's home by assuming the executable is located at /build/bin/lake.

def Lake.findLeanInstall? : BaseIO (Option Lake.LeanInstall)

Try to find 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.

def Lake.findLakeInstall? : BaseIO (Option Lake.LakeInstall)

Try to find 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 .

def Lake.findInstall? : BaseIO (Option Lake.LeanInstall × Option Lake.LakeInstall)

Try to get Lake's install path by first trying findLakeLeanHome? then by running findLeanInstall? and findLakeInstall?.

If Lake is co-located with lean (i.e., there is lean executable in the same directory as itself), it will assume it was installed with Lean and that both Lake's and Lean's files are all located their shared sysroot. In particular, their 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.