Data Structures

def Lake.elanExe (home : Lake.FilePath) : Lake.FilePath

Standard path of elan in a Elan installation.

Equations

• Lake.elanExe home = (home / { toString := "bin" } / { toString := "elan" }).addExtension System.FilePath.exeExtension

structure Lake.ElanInstall : Type

Information about the local Elan setup.

• home : Lake.FilePath
• elan : Lake.FilePath
• binDir : Lake.FilePath
• toolchainsDir : Lake.FilePath

instance Lake.instInhabitedElanInstall : Inhabited Lake.ElanInstall

Equations

• Lake.instInhabitedElanInstall = { default := { home := default, elan := default, binDir := default, toolchainsDir := default } }

instance Lake.instReprElanInstall : Repr Lake.ElanInstall

Equations

• Lake.instReprElanInstall = { reprPrec := Lake.reprElanInstall✝ }

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

Standard path of lean in a Lean installation.

Equations

• Lake.leanExe sysroot = (sysroot / { toString := "bin" } / { toString := "lean" }).addExtension System.FilePath.exeExtension

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

Standard path of leanc in a Lean installation.

Equations

• Lake.leancExe sysroot = (sysroot / { toString := "bin" } / { toString := "leanc" }).addExtension System.FilePath.exeExtension

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

Standard path of llvm-ar in a Lean installation.

Equations

• Lake.leanArExe sysroot = (sysroot / { toString := "bin" } / { toString := "llvm-ar" }).addExtension System.FilePath.exeExtension

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

Standard path of clang in a Lean installation.

Equations

• Lake.leanCcExe sysroot = (sysroot / { toString := "bin" } / { toString := "clang" }).addExtension System.FilePath.exeExtension

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

Standard path of shared libraries in a Lean installation.

Equations

• Lake.leanSharedLibDir sysroot = if System.Platform.isWindows = true then sysroot / { toString := "bin" } else sysroot / { toString := "lib" } / { toString := "lean" }

def Lake.leanSharedLib : Lake.FilePath

libleanshared file name.

Equations

• Lake.leanSharedLib = { toString := "libleanshared" }.addExtension Lake.sharedLibExt

def Lake.initSharedLib : Lake.FilePath

Init shared library file name.

Equations

• Lake.initSharedLib = { toString := "libInit_shared" }.addExtension Lake.sharedLibExt

structure Lake.LeanInstall : Type

Path information about the local Lean installation.

• 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
• initSharedLib : Lake.FilePath
• ar : Lake.FilePath
• cc : Lake.FilePath
• customCc : Bool

instance Lake.instInhabitedLeanInstall : Inhabited Lake.LeanInstall

Equations

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

instance Lake.instReprLeanInstall : Repr Lake.LeanInstall

Equations

• Lake.instReprLeanInstall = { reprPrec := Lake.reprLeanInstall✝ }

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

Equations

• self.sharedLibPath = if System.Platform.isWindows = true then [self.binDir] else [self.leanLibDir, self.systemLibDir]

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

The LEAN_CC of the Lean installation.

Equations

• self.leanCc? = if self.customCc = true then some self.cc.toString else none

def Lake.lakeExe : Lake.FilePath

Lake executable file name.

Equations

• Lake.lakeExe = { toString := "lake" }.addExtension System.FilePath.exeExtension

structure Lake.LakeInstall : Type

Path information about the local Lake installation.

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

instance Lake.instInhabitedLakeInstall : Inhabited Lake.LakeInstall

Equations

• Lake.instInhabitedLakeInstall = { default := { home := default, srcDir := default, binDir := default, libDir := default, lake := default } }

instance Lake.instReprLakeInstall : Repr Lake.LakeInstall

Equations

• Lake.instReprLakeInstall = { reprPrec := Lake.reprLakeInstall✝ }

def Lake.LakeInstall.ofLean (lean : Lake.LeanInstall) : Lake.LakeInstall

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

Equations

• Lake.LakeInstall.ofLean lean = { home := lean.sysroot, srcDir := lean.srcDir / { toString := "lake" }, binDir := lean.binDir, libDir := lean.leanLibDir, lake := lean.binDir / Lake.lakeExe }

Detection Functions

def Lake.findElanInstall? : BaseIO (Option Lake.ElanInstall)

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.

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

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.

def Lake.LeanInstall.get (sysroot : Lake.FilePath) (collocated : optParam Bool false) : BaseIO Lake.LeanInstall

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.

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

• Lake.findLeanCmdInstall? lean = (do let __do_lift ← Lake.findLeanSysroot? lean liftM (Lake.LeanInstall.get __do_lift)).run

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 <home>/bin.

Equations

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

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

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_lift ← lake.parent let __do_lift ← __do_lift.parent let __do_lift ← __do_lift.parent __do_lift.parent

def Lake.getLakeInstall? (lake : Lake.FilePath) : BaseIO (Option Lake.LakeInstall)

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.

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.

Equations

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

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

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.

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