Data Structures

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

Standard path of elan in a Elan installation.

Equations

• Lake.elanExe home = System.FilePath.addExtension (home / { toString := "bin" } / { toString := "elan" }) 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 = System.FilePath.addExtension (sysroot / { toString := "bin" } / { toString := "lean" }) System.FilePath.exeExtension

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

Standard path of leanc in a Lean installation.

Equations

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

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

Standard path of llvm-ar in a Lean installation.

Equations

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

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

Standard path of clang in a Lean installation.

Equations

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

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

Standard path of libleanshared in a Lean installation.

Equations

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

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

• Lake.LeanInstall.sharedLibPath self = 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

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

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

Standard path of lake in a Lake installation.

Equations

• Lake.lakeExe buildHome = System.FilePath.addExtension (buildHome / { toString := "bin" } / { toString := "lake" }) 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

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

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 = OptionT.run do let __do_lift ← Lake.findLeanSysroot? lean liftM (Lake.LeanInstall.get __do_lift false)

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.lakePackageHome? (lake : Lake.FilePath) : Option Lake.FilePath

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

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