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.

Equations

• Lake.MonadLakeEnv m = MonadReaderOf Lake.Env m

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

@[inline]

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

Equations

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

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

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

• getWorkspace : m Lake.Workspace

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

Equations

• Lake.instMonadWorkspaceOfMonadReaderOfWorkspace = { getWorkspace := read }

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

Equations

• Lake.instMonadWorkspaceOfMonadStateOfWorkspace = { getWorkspace := get }

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

@[inline]

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

Make a Lake.Context from a Workspace.

Equations

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

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

Equations

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

@[inline]

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

Equations

• self.workspace = self.opaqueWs.get

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

Equations

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

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

Equations

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

Workspace Helpers

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

Equations

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

@[inline]

def Lake.findPackage? {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option (Lake.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

@[inline]

def Lake.findModule? {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.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

@[inline]

def Lake.findLeanExe? {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.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

@[inline]

def Lake.findLeanLib? {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.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

@[inline]

def Lake.findExternLib? {m : Type → Type u_1} [Lake.MonadWorkspace m] [Functor m] (name : Lean.Name) : m (Option Lake.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

@[inline]

def Lake.getLeanPath {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanSrcPath {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getSharedLibPath {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getAugmentedLeanPath {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getAugmentedLeanSrcPath {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getAugmentedSharedLibPath {m : Type → Type u_1} [Lake.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

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

Equations

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

Environment Helpers

@[inline]

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

Equations

• Lake.getLakeEnv = read

@[inline]

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

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

Equations

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

@[inline]

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

@[inline]

def Lake.getPkgUrlMap {m : Type → Type u_1} [Lake.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

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

Equations

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

Search Path Helpers

@[inline]

def Lake.getEnvLeanPath {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getEnvLeanSrcPath {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getEnvSharedLibPath {m : Type → Type u_1} [Lake.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

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

Equations

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

@[inline]

def Lake.getElanHome? {m : Type → Type u_1} [Lake.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?

@[inline]

def Lake.getElan? {m : Type → Type u_1} [Lake.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?

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.

Equations

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

@[inline]

def Lake.getLeanSysroot {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanSrcDir {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanLibDir {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanIncludeDir {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanSystemLibDir {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLean {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanc {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanSharedLib {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanAr {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLeanCc {m : Type → Type u_1} [Lake.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

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

Equations

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

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.

Equations

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

@[inline]

def Lake.getLakeHome {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLakeSrcDir {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLakeLibDir {m : Type → Type u_1} [Lake.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

@[inline]

def Lake.getLake {m : Type → Type u_1} [Lake.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