def Lake.envToBool? (o : String) : Option Bool

Convert the string value of an environment variable to a boolean.

Equations

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

Data Structures

structure Lake.ElanInstall : Type

Information about the local Elan setup.

• home : System.FilePath
• elan : System.FilePath
• binDir : System.FilePath
• toolchainsDir : System.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 : System.FilePath) : System.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 : System.FilePath) : System.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 : System.FilePath) : System.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 : System.FilePath) : System.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 : System.FilePath) : System.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 : System.FilePath

libleanshared file name.

Equations

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

def Lake.initSharedLib : System.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 : System.FilePath
• githash : String
• srcDir : System.FilePath
• leanLibDir : System.FilePath
• includeDir : System.FilePath
• systemLibDir : System.FilePath
• binDir : System.FilePath
• lean : System.FilePath
• leanc : System.FilePath
• sharedLib : System.FilePath
• initSharedLib : System.FilePath
• ar : System.FilePath
• cc : System.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) : System.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 : System.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 : System.FilePath
• srcDir : System.FilePath
• binDir : System.FilePath
• libDir : System.FilePath
• lake : System.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 an Elan installation by checking the ELAN and ELAN_HOME environment variables. If ELAN is set but empty, Elan is considered disabled.

Equations

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

def Lake.findLeanSysroot? (lean : String := "lean") : BaseIO (Option System.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 : System.FilePath) (collocated : 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 from the AR / CC environment variables or 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 : System.FilePath) : BaseIO String

Equations

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

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

Equations

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

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

Equations

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

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

Attempt to detect the installation of the given lean command by calling findLeanSysroot?. 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 System.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 : System.FilePath) : Option System.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 : System.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 using the LEAN and LEAN_SYSROOT environment variables.

If LEAN_SYSROOT is set, use it. Otherwise, check LEAN for the lean executable. If LEAN is set but empty, Lean will be considered disabled. Otherwise, Lean's location will be determined by trying findLeanSysroot? using value of LEAN or, if unset, the lean in PATH.

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?. Setting LAKE_OVERRIDE_LEAN to true will force Lake to use findLeanInstall? even if co-located.

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.