Lake Configuration Monads #
Definitions and helpers for interacting with the Lake configuration monads.
A monad equipped with a (read-only) detected environment for Lake.
Instances For
A monad equipped with a (read-only) Lake Workspace.
Instances For
A monad equipped with a (read-only) Lake context.
Instances For
Workspace Helpers #
Get the workspace of the context.
Instances For
Get the root package of the context's workspace.
Instances For
Try to find a package within the workspace with the given name.
Instances For
Locate the named module in the workspace (if it is local to it).
Instances For
Try to find a Lean executable in the workspace with the given name.
Instances For
Try to find a Lean library in the workspace with the given name.
Instances For
Try to find an external library in the workspace with the given name.
Instances For
Get the paths added to LEAN_PATH by the context's workspace.
Instances For
Get the paths added to LEAN_SRC_PATH by the context's workspace.
Instances For
Get the augmented LEAN_PATH set by the context's workspace.
Instances For
Get the augmented LEAN_SRC_PATH set by the context's workspace.
Instances For
Environment Helpers #
Instances For
Get the name of Elan toolchain for the Lake environment. Empty if none.
Instances For
Search Path Helpers #
Get the detected LEAN_PATH value of the Lake environment.
Instances For
Get the detected LEAN_SRC_PATH value of the Lake environment.
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).
Instances For
Get the path of the elan binary in the detected Elan installation.
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.
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.