Lake Configuration Monads #
Definitions and helpers for interacting with the Lake configuration monads.
A monad equipped with a (read-only) detected environment for Lake.
Equations
Instances For
A monad equipped with a (read-only) Lake Workspace
.
Equations
Instances For
A monad equipped with a (read-only) Lake context.
Equations
Instances For
Make a Lake.Context
from a Workspace
.
Equations
- Lake.mkLakeContext ws = { opaqueWs := Lake.OpaqueWorkspace.mk ws }
Instances For
Equations
- Lake.instMonadLake = { read := (fun x => Lake.mkLakeContext x) <$> read }
Equations
- Lake.Context.workspace self = Lake.OpaqueWorkspace.get self.opaqueWs
Instances For
Equations
- Lake.instMonadWorkspace = { read := (fun x => Lake.Context.workspace x) <$> read }
Workspace Helpers #
Get the root package of the context's workspace.
Instances For
Try to find a package within the workspace with the given name.
Equations
- Lake.findPackage? name = (fun x => Lake.Workspace.findPackage? name x) <$> Lake.getWorkspace
Instances For
Locate the named module in the workspace (if it is local to it).
Equations
- Lake.findModule? name = (fun x => Lake.Workspace.findModule? name x) <$> Lake.getWorkspace
Instances For
Try to find a Lean executable in the workspace with the given name.
Equations
- Lake.findLeanExe? name = (fun x => Lake.Workspace.findLeanExe? name x) <$> Lake.getWorkspace
Instances For
Try to find a Lean library in the workspace with the given name.
Equations
- Lake.findLeanLib? name = (fun x => Lake.Workspace.findLeanLib? name x) <$> Lake.getWorkspace
Instances For
Try to find an external library in the workspace with the given name.
Equations
- Lake.findExternLib? name = (fun x => Lake.Workspace.findExternLib? name x) <$> Lake.getWorkspace
Instances For
Get the paths added to LEAN_PATH
by the context's workspace.
Equations
- Lake.getLeanPath = (fun x => Lake.Workspace.leanPath x) <$> Lake.getWorkspace
Instances For
Get the paths added to LEAN_SRC_PATH
by the context's workspace.
Equations
- Lake.getLeanSrcPath = (fun x => Lake.Workspace.leanSrcPath x) <$> Lake.getWorkspace
Instances For
Get the augmented LEAN_PATH
set by the context's workspace.
Equations
- Lake.getAugmentedLeanPath = (fun x => Lake.Workspace.augmentedLeanPath x) <$> Lake.getWorkspace
Instances For
Get the augmented LEAN_SRC_PATH
set by the context's workspace.
Equations
- Lake.getAugmentedLeanSrcPath = (fun x => Lake.Workspace.augmentedLeanSrcPath x) <$> Lake.getWorkspace
Instances For
Get the augmented environment variables set by the context's workspace.
Equations
- Lake.getAugmentedEnv = (fun x => Lake.Workspace.augmentedEnvVars x) <$> Lake.getWorkspace
Instances For
Environment Helpers #
Get the name of Elan toolchain for the Lake environment. Empty if none.
Equations
- Lake.getElanToolchain = (fun x => Lake.Env.toolchain x) <$> Lake.getLakeEnv
Instances For
Search Path Helpers #
Get the detected LEAN_PATH
value of the Lake environment.
Equations
- Lake.getEnvLeanPath = (fun x => Lake.Env.leanPath x) <$> Lake.getLakeEnv
Instances For
Get the detected LEAN_SRC_PATH
value of the Lake environment.
Equations
- Lake.getEnvLeanSrcPath = (fun x => Lake.Env.leanSrcPath x) <$> Lake.getLakeEnv
Instances For
Elan Install Helpers #
Get the detected Elan installation (if one).
Instances For
Get the root directory of the detected Elan installation (i.e., ELAN_HOME
).
Equations
- Lake.getElanHome? = (fun x => Option.map (fun x => x.home) x) <$> Lake.getElanInstall?
Instances For
Get the path of the elan
binary in the detected Elan installation.
Equations
- Lake.getElan? = (fun x => Option.map (fun x => x.elan) x) <$> Lake.getElanInstall?
Instances For
Lean Install Helpers #
Get the detected Lean installation.
Instances For
Get the root directory of the detected Lean installation.
Instances For
Get the Lean source directory of the detected Lean installation.
Instances For
Get the Lean library directory of the detected Lean installation.
Instances For
Get the C include directory of the detected Lean installation.
Instances For
Get the system library directory of the detected Lean installation.
Instances For
Get the path of the lean
binary in the detected Lean installation.
Instances For
Get the path of the leanc
binary in the detected Lean installation.
Instances For
Get the path of the ar
binary in the detected Lean installation.
Instances For
Get the path of C compiler in the detected Lean installation.
Instances For
Get the optional LEAN_CC
compiler override of the detected Lean installation.
Equations
- Lake.getLeanCc? = (fun x => Lake.LeanInstall.leanCc? x) <$> Lake.getLeanInstall
Instances For
Lake Install Helpers #
Get the detected Lake installation.
Instances For
Get the root directory of the detected Lake installation (e.g., LAKE_HOME
).
Instances For
Get the source directory of the detected Lake installation.
Instances For
Get the Lean library directory of the detected Lake installation.
Instances For
Get the path of the lake
binary in the detected Lake installation.