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 : Env) (self : 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 Workspace

  Gets the current Lake workspace.

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

Equations

• Lake.instMonadWorkspaceOfMonadReaderOfWorkspace = { getWorkspace := read }

instance Lake.instMonadWorkspaceOfMonadStateOfWorkspace {m : Type → Type u_1} [MonadStateOf Workspace m] : 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 : Workspace) : Context

Make a Lake.Context from a Workspace.

Equations

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

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

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 }

@[inline]

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

Equations

• self.workspace = self.opaqueWs.get

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 }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Environment Helpers

@[inline]

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

Gets the current Lake environment.

Equations

• Lake.getLakeEnv = read

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

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

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

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

@[inline]

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

Returns the Lake cache for the environment. May be disabled.

Equations

• Lake.getLakeCache = (fun (x : Lake.Env) => x.lakeCache) <$> Lake.getLakeEnv

@[inline]

def Lake.getArtifact? {m : Type → Type u_1} [MonadLakeEnv m] [Bind m] [MonadLiftT BaseIO m] (contentHash : Hash) (ext : String := "art") : m (Option Artifact)

Returns the path to the artifact in the Lake cache with extension ext if it exists.

If the Lake cache is disabled, the behavior of this function is undefined.

Equations

• Lake.getArtifact? contentHash ext = do let x ← Lake.getLakeEnv liftM (x.lakeCache.getArtifact? contentHash ext)

Search Path Helpers

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

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

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

Elan Install Helpers

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

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

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

Lean Install Helpers

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

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

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

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

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

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

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

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

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

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

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

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

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

Lake Install Helpers

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

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

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

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

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