Lake Configuration Monads

Definitions and helpers for interacting with the Lake configuration monads.

@[reducible, inline]

abbrev Lake.MonadLakeEnv (m : Type → Type u) : Type u

A monad equipped with a (read-only) detected environment for Lake.

@[reducible, inline]

abbrev Lake.LakeEnvT (m : Type → Type u_1) (α : Type) : Type u_1

A transformer to equip a monad with a Lake.Env.

@[inline]

def Lake.LakeEnvT.run {m : Type → Type u_1} {α : Type} (env : Env) (self : LakeEnvT m α) : m α

class Lake.MonadWorkspace (m : Type → Type u) : Type u

A monad equipped with a (read-only) Lake Workspace.

• getWorkspace : m Workspace

  Gets the current Lake workspace.

instance Lake.instMonadWorkspaceOfMonadReaderOfWorkspace {m : Type → Type u_1} [MonadReaderOf Workspace m] : MonadWorkspace m

instance Lake.instMonadWorkspaceOfMonadStateOfWorkspace {m : Type → Type u_1} [MonadStateOf Workspace m] : MonadWorkspace m

@[reducible, inline]

abbrev Lake.MonadLake (m : Type → Type u) : Type u

A monad equipped with a (read-only) Lake context.

@[inline]

def Lake.mkLakeContext (ws : Workspace) : Context

Make a Lake.Context from a Workspace.

@[inline]

def Lake.Workspace.runLakeT {m : Type → Type u_1} {α : Type} (ws : Workspace) (x : LakeT m α) : m α

Run a LakeT monad in the context of this workspace.

instance Lake.instMonadLakeOfMonadWorkspaceOfFunctor {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : MonadLake m

@[inline]

def Lake.Context.workspace (self : Context) : Workspace

instance Lake.instMonadWorkspaceOfMonadLakeOfFunctor {m : Type → Type u_1} [MonadLake m] [Functor m] : MonadWorkspace m

instance Lake.instMonadLakeEnvOfMonadWorkspaceOfFunctor {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : MonadLakeEnv m

Workspace Helpers

@[inline]

def Lake.getRootPackage {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m Package

Get the root package of the context's workspace.

@[inline]

def Lake.findPackage? {m : Type → Type u_1} [MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option (NPackage name))

Try to find a package within the workspace with the given name.

@[inline]

def Lake.findModule? {m : Type → Type u_1} [MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Module)

Locate the named, buildable, importable, local module in the workspace.

@[inline]

def Lake.findLeanExe? {m : Type → Type u_1} [MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option LeanExe)

Try to find a Lean executable in the workspace with the given name.

@[inline]

def Lake.findLeanLib? {m : Type → Type u_1} [MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option LeanLib)

Try to find a Lean library in the workspace with the given name.

@[inline]

def Lake.findExternLib? {m : Type → Type u_1} [MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option ExternLib)

Try to find an external library in the workspace with the given name.

@[inline]

def Lake.getLeanPath {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m System.SearchPath

Get the paths added to LEAN_PATH by the context's workspace.

@[inline]

def Lake.getLeanSrcPath {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m System.SearchPath

Get the paths added to LEAN_SRC_PATH by the context's workspace.

@[inline]

def Lake.getSharedLibPath {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m System.SearchPath

Get the paths added to the shared library path by the context's workspace.

@[inline]

def Lake.getAugmentedLeanPath {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m System.SearchPath

Get the augmented LEAN_PATH set by the context's workspace.

@[inline]

def Lake.getAugmentedLeanSrcPath {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m System.SearchPath

Get the augmented LEAN_SRC_PATH set by the context's workspace.

@[inline]

def Lake.getAugmentedSharedLibPath {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m System.SearchPath

Get the augmented shared library path set by the context's workspace.

@[inline]

def Lake.getAugmentedEnv {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m (Array (String × Option String))

Get the augmented environment variables set by the context's workspace.

Environment Helpers

@[inline]

def Lake.getLakeEnv {m : Type → Type u_1} [MonadLakeEnv m] : m Env

Gets the current Lake environment.

@[inline]

def Lake.getNoCache {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] [MonadBuild m] : m Bool

Get the LAKE_NO_CACHE/--no-cache Lake configuration.

@[inline]

def Lake.getTryCache {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] [MonadBuild m] : m Bool

Get whether the LAKE_NO_CACHE/--no-cache Lake configuration is NOT set.

@[inline]

def Lake.getPkgUrlMap {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m (Lean.NameMap String)

Get the LAKE_PACKAGE_URL_MAP for the Lake environment. Empty if none.

@[inline]

def Lake.getElanToolchain {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m String

Get the name of Elan toolchain for the Lake environment. Empty if none.

Search Path Helpers

@[inline]

def Lake.getEnvLeanPath {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.SearchPath

Get the detected LEAN_PATH value of the Lake environment.

@[inline]

def Lake.getEnvLeanSrcPath {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.SearchPath

Get the detected LEAN_SRC_PATH value of the Lake environment.

@[inline]

def Lake.getEnvSharedLibPath {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.SearchPath

Get the detected sharedLibPathEnvVar value of the Lake environment.

Elan Install Helpers

@[inline]

def Lake.getElanInstall? {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m (Option ElanInstall)

Get the detected Elan installation (if one).

@[inline]

def Lake.getElanHome? {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m (Option System.FilePath)

Get the root directory of the detected Elan installation (i.e., ELAN_HOME).

@[inline]

def Lake.getElan? {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m (Option System.FilePath)

Get the path of the elan binary in the detected Elan installation.

Lean Install Helpers

@[inline]

def Lake.getLeanInstall {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m LeanInstall

Get the detected Lean installation.

@[inline]

def Lake.getLeanSysroot {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the root directory of the detected Lean installation.

@[inline]

def Lake.getLeanSrcDir {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the Lean source directory of the detected Lean installation.

@[inline]

def Lake.getLeanLibDir {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the Lean library directory of the detected Lean installation.

@[inline]

def Lake.getLeanIncludeDir {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the C include directory of the detected Lean installation.

@[inline]

def Lake.getLeanSystemLibDir {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the system library directory of the detected Lean installation.

@[inline]

def Lake.getLean {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the path of the lean binary in the detected Lean installation.

@[inline]

def Lake.getLeanc {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the path of the leanc binary in the detected Lean installation.

@[inline]

def Lake.getLeanSharedLib {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the path of the libleanshared library in the detected Lean installation.

@[inline]

def Lake.getLeanAr {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the path of the ar binary in the detected Lean installation.

@[inline]

def Lake.getLeanCc {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the path of C compiler in the detected Lean installation.

@[inline]

def Lake.getLeanCc? {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m (Option String)

Get the optional LEAN_CC compiler override of the detected Lean installation.

@[inline]

def Lake.getLeanLinkSharedFlags {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m (Array String)

Get the flags required to link shared libraries using the detected Lean installation.

Lake Install Helpers

@[inline]

def Lake.getLakeInstall {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m LakeInstall

Get the detected Lake installation.

@[inline]

def Lake.getLakeHome {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the root directory of the detected Lake installation (e.g., LAKE_HOME).

@[inline]

def Lake.getLakeSrcDir {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the source directory of the detected Lake installation.

@[inline]

def Lake.getLakeLibDir {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the Lean library directory of the detected Lake installation.

@[inline]

def Lake.getLake {m : Type → Type u_1} [MonadLakeEnv m] [Functor m] : m System.FilePath

Get the path of the lake binary in the detected Lake installation.