# Lake Configuration Monads #

Definitions and helpers for interacting with the Lake configuration monads.

source
@[reducible, inline]
abbrev Lake.MonadLakeEnv (m : Type → Type u) :
Type u

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

Equations

- Lake.MonadLakeEnv m = MonadReaderOf Lake.Env m

Instances For

source
@[reducible, inline]
abbrev Lake.LakeEnvT (m : Type → Type u_1) (α : Type) :
Type u_1

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

Equations

- Lake.LakeEnvT = ReaderT Lake.Env

Instances For

source
@[inline]
def Lake.LakeEnvT.run {m : Type → Type u_1} {α : Type} (env : Env) (self : LakeEnvT m α) :
m α
Equations

- Lake.LakeEnvT.run env self = ReaderT.run self env

Instances For

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

Instances

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

- Lake.instMonadWorkspaceOfMonadReaderOfWorkspace = { getWorkspace := read }

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

- Lake.instMonadWorkspaceOfMonadStateOfWorkspace = { getWorkspace := get }

source
@[reducible, inline]
abbrev Lake.MonadLake (m : Type → Type u) :
Type u

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

Equations

- Lake.MonadLake m = MonadReaderOf Lake.Context m

Instances For

source
@[inline]
def Lake.mkLakeContext (ws : Workspace) :
Context

Make a `Lake.Context` from a `Workspace`.

Equations

- Lake.mkLakeContext ws = { opaqueWs := Lake.OpaqueWorkspace.mk ws }

Instances For

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

Equations

- ws.runLakeT x = Lake.LakeT.run (Lake.mkLakeContext ws) x

Instances For

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

- Lake.instMonadLakeOfMonadWorkspaceOfFunctor = { read := (fun (x : Lake.Workspace) => Lake.mkLakeContext x) <$> Lake.getWorkspace }

source
@[inline]
def Lake.Context.workspace (self : Context) :
Workspace
Equations

- self.workspace = self.opaqueWs.get

Instances For

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

- Lake.instMonadWorkspaceOfMonadLakeOfFunctor = { getWorkspace := (fun (x : Lake.Context) => x.workspace) <$> read }

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

- Lake.instMonadLakeEnvOfMonadWorkspaceOfFunctor = { read := (fun (x : Lake.Workspace) => x.lakeEnv) <$> Lake.getWorkspace }

## Workspace Helpers #

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

Get the root package of the context's workspace.

Equations

- Lake.getRootPackage = (fun (x : Lake.Workspace) => x.root) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.findPackage? name = (fun (x : Lake.Workspace) => Lake.Workspace.findPackage? name x) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.findModule? name = (fun (x : Lake.Workspace) => Lake.Workspace.findModule? name x) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.findModuleBySrc? path = (fun (x : Lake.Workspace) => Lake.Workspace.findModuleBySrc? path x) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.findLeanExe? name = (fun (x : Lake.Workspace) => Lake.Workspace.findLeanExe? name x) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.findLeanLib? name = (fun (x : Lake.Workspace) => Lake.Workspace.findLeanLib? name x) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.findExternLib? name = (fun (x : Lake.Workspace) => Lake.Workspace.findExternLib? name x) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getServerOptions = (fun (x : Lake.Workspace) => x.serverOptions) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getLeanOptions = (fun (x : Lake.Workspace) => x.leanOptions) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getLeanArgs = (fun (x : Lake.Workspace) => x.leanArgs) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getLeanPath = (fun (x : Lake.Workspace) => x.leanPath) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getLeanSrcPath = (fun (x : Lake.Workspace) => x.leanSrcPath) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getSharedLibPath = (fun (x : Lake.Workspace) => x.sharedLibPath) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getAugmentedLeanPath = (fun (x : Lake.Workspace) => x.augmentedLeanPath) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getAugmentedLeanSrcPath = (fun (x : Lake.Workspace) => x.augmentedLeanSrcPath) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getAugmentedSharedLibPath = (fun (x : Lake.Workspace) => x.augmentedSharedLibPath) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getAugmentedEnv = (fun (x : Lake.Workspace) => x.augmentedEnvVars) <$> Lake.getWorkspace

Instances For

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

Returns the Lake cache for the environment.

Equations

- Lake.getLakeCache = (fun (x : Lake.Workspace) => x.lakeCache) <$> Lake.getWorkspace

Instances For

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

Equations

- Lake.getArtifact? descr = do let x ← Lake.getLakeCache liftM (x.getArtifact? descr)

Instances For

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

Returns whether the package the artifact cache is enabled for the package.

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

Equations

- self.isArtifactCacheEnabled = (fun (x : Lake.Workspace) => self.enableArtifactCache?.getD x.enableArtifactCache) <$> Lake.getWorkspace

Instances For

## Environment Helpers #

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

Gets the current Lake environment.

Equations

- Lake.getLakeEnv = read

Instances For

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

Equations

- Lake.getNoCache = (fun (x : Lake.Env) => x.noCache) <$> Lake.getLakeEnv

Instances For

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

Equations

- Lake.getTryCache = (fun (x : Lake.Env) => !x.noCache) <$> Lake.getLakeEnv

Instances For

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

Equations

- Lake.getPkgUrlMap = (fun (x : Lake.Env) => x.pkgUrlMap) <$> Lake.getLakeEnv

Instances For

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

Equations

- Lake.getElanToolchain = (fun (x : Lake.Env) => x.toolchain) <$> Lake.getLakeEnv

Instances For

### Search Path Helpers #

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

Equations

- Lake.getEnvLeanPath = (fun (x : Lake.Env) => x.leanPath) <$> Lake.getLakeEnv

Instances For

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

Equations

- Lake.getEnvLeanSrcPath = (fun (x : Lake.Env) => x.leanSrcPath) <$> Lake.getLakeEnv

Instances For

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

Equations

- Lake.getEnvSharedLibPath = (fun (x : Lake.Env) => x.sharedLibPath) <$> Lake.getLakeEnv

Instances For

### Elan Install Helpers #

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

Get the detected Elan installation (if one).

Equations

- Lake.getElanInstall? = (fun (x : Lake.Env) => x.elan?) <$> Lake.getLakeEnv

Instances For

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

Equations

- Lake.getElanHome? = (fun (x : Option Lake.ElanInstall) => Option.map (fun (x : Lake.ElanInstall) => x.home) x) <$> Lake.getElanInstall?

Instances For

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

Equations

- Lake.getElan? = (fun (x : Option Lake.ElanInstall) => Option.map (fun (x : Lake.ElanInstall) => x.elan) x) <$> Lake.getElanInstall?

Instances For

### Lean Install Helpers #

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

Get the detected Lean installation.

Equations

- Lake.getLeanInstall = (fun (x : Lake.Env) => x.lean) <$> Lake.getLakeEnv

Instances For

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

Equations

- Lake.getLeanSysroot = (fun (x : Lake.LeanInstall) => x.sysroot) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanSrcDir = (fun (x : Lake.LeanInstall) => x.srcDir) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanLibDir = (fun (x : Lake.LeanInstall) => x.leanLibDir) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanIncludeDir = (fun (x : Lake.LeanInstall) => x.includeDir) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanSystemLibDir = (fun (x : Lake.LeanInstall) => x.systemLibDir) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLean = (fun (x : Lake.LeanInstall) => x.lean) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanc = (fun (x : Lake.LeanInstall) => x.leanc) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanSharedLib = (fun (x : Lake.LeanInstall) => x.sharedLib) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanAr = (fun (x : Lake.LeanInstall) => x.ar) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanCc = (fun (x : Lake.LeanInstall) => x.cc) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanCc? = (fun (x : Lake.LeanInstall) => x.leanCc?) <$> Lake.getLeanInstall

Instances For

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

Equations

- Lake.getLeanLinkSharedFlags = (fun (x : Lake.LeanInstall) => x.ccLinkSharedFlags) <$> Lake.getLeanInstall

Instances For

### Lake Install Helpers #

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

Get the detected Lake installation.

Equations

- Lake.getLakeInstall = (fun (x : Lake.Env) => x.lake) <$> Lake.getLakeEnv

Instances For

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

Equations

- Lake.getLakeHome = (fun (x : Lake.LakeInstall) => x.home) <$> Lake.getLakeInstall

Instances For

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

Equations

- Lake.getLakeSrcDir = (fun (x : Lake.LakeInstall) => x.srcDir) <$> Lake.getLakeInstall

Instances For

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

Equations

- Lake.getLakeLibDir = (fun (x : Lake.LakeInstall) => x.libDir) <$> Lake.getLakeInstall

Instances For

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

Equations

- Lake.getLake = (fun (x : Lake.LakeInstall) => x.lake) <$> Lake.getLakeInstall

Instances For