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

@[implicit_reducible]

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

@[implicit_reducible]

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

Constructs a Lake.Context from the workspace ws.

@[inline]

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

Runs a LakeT monad in the context of the workspace ws.

@[implicit_reducible]

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

@[inline]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[inline]

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

Returns the root package of the context's workspace.

@[inline]

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

Returns the unique package in the workspace (if any) that is identified by keyName.

@[inline]

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

Returns the first package in the workspace (if any) that has been assigned the name.

This can be used to find the package corresponding to a user-provided name. If the package's unique identifier is already available, use findPackageByKey?instead.

@[reducible, inline, deprecated "Use `findPackageByKey?` or `findPackageByName?` instead" (since := "2025-12-03")]

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

Deprecated. If attempting to find the package corresponding to a user-provided name, use findPackageByName?. Otherwise, if the package's unique identifier is available, use findPackageByKey?.

@[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.findModules {m : Type → Type u_1} [MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Array Module)

For each package in the workspace, locate the named, buildable, importable, local module.

@[inline]

def Lake.findModuleBySrc? {m : Type → Type u_1} [MonadWorkspace m] [Functor m] (path : System.FilePath) : m (Option Module)

Returns the buildable module in the workspace whose source file is path.

@[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.getServerOptions {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m Lean.LeanOptions

Options to pass to the Lean server when editing Lean files outside a library.

@[inline]

def Lake.getLeanOptions {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m Lean.LeanOptions

Options to pass to lean for files outside a library (e.g., via lake lean).

@[inline]

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

Arguments to pass to lean for files outside a library (e.g., via lake lean).

@[inline]

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

Returns 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

Returns 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

Returns 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

Returns 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

Returns 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

Returns 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))

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

@[inline]

def Lake.getLakeCache {m : Type → Type u_1} [MonadWorkspace m] [Functor m] : m Cache

Returns the Lake cache for the environment.

@[inline]

def Lake.getArtifact? {m : Type → Type u_1} [MonadWorkspace m] [Functor m] [Bind m] [MonadLiftT BaseIO m] (descr : ArtifactDescr) : m (Option Artifact)

Returns the artifact in the Lake cache corresponding the given artifact description.

@[inline]

def Lake.Package.isArtifactCacheReadable {m : Type → Type u_1} [Functor m] [MonadWorkspace m] (self : Package) : m Bool

Returns whether the package should store its artifacts in the Lake artifact cache.

If the package has not configured the artifact cache itself through Package.enableArtifactCache?, this will default to the workspace configuration.

@[inline]

def Lake.Package.isArtifactCacheWritable {m : Type → Type u_1} [Functor m] [MonadWorkspace m] (self : Package) : m Bool

Returns whether the package should restore its artifacts from the Lake artifact cache.

If the package has not configured the artifact cache itself through Package.enableArtifactCache?, this will default to the workspace configuration.

@[reducible, inline, deprecated Lake.Package.isArtifactCacheWritable (since := "2026-02-03")]

abbrev Lake.Package.isArtifactCacheEnabled {m : Type → Type u_1} [Functor m] [MonadWorkspace m] (self : Package) : m Bool

Returns whether the package should restore its artifacts from the Lake artifact cache.

If the package has not configured the artifact cache itself through Package.enableArtifactCache?, this will default to the workspace configuration.

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

Returns 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

Returns 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)

Returns 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

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

@[inline]

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

Returns 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

Returns 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

Returns the detected sharedLibPathEnvVar value of the Lake environment.

@[inline]

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

Returns the detected Elan installation (if one).

@[inline]

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

Returns 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)

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

@[inline]

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

Returns the detected Lean installation.

@[inline]

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

Returns the root directory of the detected Lean installation.

@[inline]

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

Returns 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

Returns 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

Returns 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

Returns 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

Returns 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

Returns 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

Returns 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.

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