Lake Configuration Monads

Definitions and helpers for interacting with the Lake configuration monads.

@[inline, reducible]

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

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

@[inline, reducible]

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

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

@[inline, reducible]

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

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

@[inline]

def Lake.mkLakeContext (ws : Lake.Workspace) : Lake.Context

Make a Lake.Context from a Workspace.

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

@[inline]

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

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

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

Workspace Helpers

@[inline]

def Lake.getWorkspace {m : Type → Type u_1} [Lake.MonadWorkspace m] : m Lake.Workspace

Get the workspace of the context.

@[inline]

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

Get the root package of the context's workspace.

@[inline]

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

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

@[inline]

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

Locate the named module in the workspace (if it is local to it).

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

def Lake.getAugmentedEnv {m : Type → Type u_1} [Lake.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} [Lake.MonadLakeEnv m] : m Lake.Env

@[inline]

def Lake.getElanToolchain {m : Type → Type u_1} [Lake.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} [Lake.MonadLakeEnv m] [Functor m] : m Lake.SearchPath

Get the detected LEAN_PATH value of the Lake environment.

@[inline]

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

Get the detected LEAN_SRC_PATH value of the Lake environment.

@[inline]

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

Get the detected sharedLibPathEnvVar value of the Lake environment.

Elan Install Helpers

@[inline]

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

Get the detected Elan installation (if one).

@[inline]

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

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

@[inline]

def Lake.getElan? {m : Type → Type u_1} [Lake.MonadLakeEnv m] [Functor m] : m (Option Lake.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} [Lake.MonadLakeEnv m] [Functor m] : m Lake.LeanInstall

Get the detected Lean installation.

@[inline]

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

Get the root directory of the detected Lean installation.

@[inline]

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

Get the Lean source directory of the detected Lean installation.

@[inline]

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

Get the Lean library directory of the detected Lean installation.

@[inline]

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

Get the C include directory of the detected Lean installation.

@[inline]

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

Get the system library directory of the detected Lean installation.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

Lake Install Helpers

@[inline]

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

Get the detected Lake installation.

@[inline]

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

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

@[inline]

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

Get the source directory of the detected Lake installation.

@[inline]

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

Get the Lean library directory of the detected Lake installation.

@[inline]

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

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