Lake Configuration Monads #

Definitions and helpers for interacting with the Lake configuration monads.

source

@[inline, reducible]

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

Type u

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

Instances For

source

@[inline, reducible]

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

Type u

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

Instances For

source

@[inline, reducible]

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

Type u

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

Instances For

source

@[inline]

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

Lake.Context

Make a Lake.Context from a Workspace.

Instances For

source

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

Lake.MonadLake m

source

@[inline]

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

Lake.Workspace

Instances For

source

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

Lake.MonadWorkspace m

source

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

Lake.MonadLakeEnv m

Workspace Helpers #

source

@[inline]

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

m Lake.Workspace

Get the workspace of the context.

Instances For

source

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

Instances For

source

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

Instances For

source

@[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).

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

Environment Helpers #

source

@[inline]

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

m Lake.Env

Instances For

Search Path Helpers #

source

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

Instances For

source

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

Instances For

source

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

Instances For

Lean Install Helpers #

source

@[inline]

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

m Lake.LeanInstall

Get the detected Lean installation.

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

Lake Install Helpers #

source

@[inline]

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

m Lake.LakeInstall

Get the detected Lake installation.

Instances For

source

@[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).

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For