structure Lake.Workspace : Type

A Lake workspace -- the top-level package directory.

• root : Lake.Package

  The root package of the workspace.

• lakeEnv : Lake.Env

  The detect Lake.Env of the workspace.

• packages : Array Lake.Package

  The packages within the workspace (in require declaration order).

• packageMap : Lake.DNameMap Lake.NPackage

  Name-package map of packages within the workspace.

• moduleFacetConfigs : Lake.DNameMap Lake.ModuleFacetConfig

  Name-configuration map of module facets defined in the workspace.

• packageFacetConfigs : Lake.DNameMap Lake.PackageFacetConfig

  Name-configuration map of package facets defined in the workspace.

• libraryFacetConfigs : Lake.DNameMap Lake.LibraryFacetConfig

  Name-configuration map of library facets defined in the workspace.

instance Lake.instNonemptyWorkspace : Nonempty Lake.Workspace

Equations

• Lake.instNonemptyWorkspace = ⋯

@[implemented_by Lake.OpaqueWorkspace.unsafeMk]

opaque Lake.OpaqueWorkspace.mk : Lake.Workspace → Lake.OpaqueWorkspace

@[simp]

axiom Lake.OpaqueWorkspace.get_mk : ∀ {x : Lake.Workspace}, Lake.OpaqueWorkspace.get (Lake.OpaqueWorkspace.mk x) = x

instance Lake.OpaqueWorkspace.instCoeOpaqueWorkspaceWorkspace : Coe Lake.OpaqueWorkspace Lake.Workspace

Equations

• Lake.OpaqueWorkspace.instCoeOpaqueWorkspaceWorkspace = { coe := Lake.OpaqueWorkspace.get }

unsafe def Lake.OpaqueWorkspace.unsafeGet : Lake.OpaqueWorkspace → Lake.Workspace

Equations

• Lake.OpaqueWorkspace.unsafeGet = unsafeCast

unsafe def Lake.OpaqueWorkspace.unsafeMk : Lake.Workspace → Lake.OpaqueWorkspace

Equations

• Lake.OpaqueWorkspace.unsafeMk = unsafeCast

instance Lake.OpaqueWorkspace.instInhabitedOpaqueWorkspace [Inhabited Lake.Workspace] : Inhabited Lake.OpaqueWorkspace

Equations

• Lake.OpaqueWorkspace.instInhabitedOpaqueWorkspace = { default := Lake.OpaqueWorkspace.mk default }

@[implemented_by Lake.OpaqueWorkspace.unsafeGet]

opaque Lake.OpaqueWorkspace.get : Lake.OpaqueWorkspace → Lake.Workspace

instance Lake.OpaqueWorkspace.instCoeWorkspaceOpaqueWorkspace : Coe Lake.Workspace Lake.OpaqueWorkspace

Equations

• Lake.OpaqueWorkspace.instCoeWorkspaceOpaqueWorkspace = { coe := Lake.OpaqueWorkspace.mk }

@[inline]

def Lake.Workspace.dir (self : Lake.Workspace) : Lake.FilePath

The path to the workspace's directory (i.e., the directory of the root package).

Equations

• Lake.Workspace.dir self = self.root.dir

@[inline]

def Lake.Workspace.config (self : Lake.Workspace) : Lake.WorkspaceConfig

The workspace's configuration.

Equations

• Lake.Workspace.config self = self.root.config.toWorkspaceConfig

@[inline]

def Lake.Workspace.relLakeDir (self : Lake.Workspace) : Lake.FilePath

The path to the workspace' Lake directory relative to dir.

Equations

• Lake.Workspace.relLakeDir self = Lake.Package.relLakeDir self.root

@[inline]

def Lake.Workspace.lakeDir (self : Lake.Workspace) : Lake.FilePath

The the full path to the workspace's Lake directory (e.g., .lake).

Equations

• Lake.Workspace.lakeDir self = Lake.Package.lakeDir self.root

@[inline]

def Lake.Workspace.relPkgsDir (self : Lake.Workspace) : Lake.FilePath

The path to the workspace's remote packages directory relative to dir.

Equations

• Lake.Workspace.relPkgsDir self = Lake.Package.relPkgsDir self.root

@[inline]

def Lake.Workspace.pkgsDir (self : Lake.Workspace) : Lake.FilePath

The workspace's dir joined with its relPkgsDir.

Equations

• Lake.Workspace.pkgsDir self = Lake.Package.pkgsDir self.root

@[inline]

def Lake.Workspace.manifestFile (self : Lake.Workspace) : Lake.FilePath

The workspace's Lake manifest.

Equations

• Lake.Workspace.manifestFile self = Lake.Package.manifestFile self.root

def Lake.Workspace.addPackage (pkg : Lake.Package) (self : Lake.Workspace) : Lake.Workspace

Add a package to the workspace.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Workspace.findPackage? (name : Lake.Name) (self : Lake.Workspace) : Option (Lake.NPackage name)

Try to find a package within the workspace with the given name.

Equations

• Lake.Workspace.findPackage? name self = Lake.DRBMap.find? self.packageMap name

def Lake.Workspace.findScript? (script : Lake.Name) (self : Lake.Workspace) : Option Lake.Script

Try to find a script in the workspace with the given name.

Equations

• Lake.Workspace.findScript? script self = Array.findSomeRev? self.packages fun (x : Lake.Package) => Lean.NameMap.find? x.scripts script

def Lake.Workspace.isLocalModule (mod : Lake.Name) (self : Lake.Workspace) : Bool

Check if the module is local to any package in the workspace.

Equations

• Lake.Workspace.isLocalModule mod self = Array.any self.packages (fun (pkg : Lake.Package) => Lake.Package.isLocalModule mod pkg) 0

def Lake.Workspace.isBuildableModule (mod : Lake.Name) (self : Lake.Workspace) : Bool

Check if the module is buildable by any package in the workspace.

Equations

• Lake.Workspace.isBuildableModule mod self = Array.any self.packages (fun (pkg : Lake.Package) => Lake.Package.isBuildableModule mod pkg) 0

def Lake.Workspace.findModule? (mod : Lake.Name) (self : Lake.Workspace) : Option Lake.Module

Locate the named, buildable, importable, local module in the workspace.

Equations

• Lake.Workspace.findModule? mod self = Array.findSomeRev? self.packages fun (x : Lake.Package) => Lake.Package.findModule? mod x

def Lake.Workspace.findTargetModule? (mod : Lake.Name) (self : Lake.Workspace) : Option Lake.Module

Locate the named, buildable, but not necessarily importable, module in the workspace.

Equations

• Lake.Workspace.findTargetModule? mod self = Array.findSomeRev? self.packages fun (x : Lake.Package) => Lake.Package.findTargetModule? mod x

def Lake.Workspace.findLeanLib? (name : Lake.Name) (self : Lake.Workspace) : Option Lake.LeanLib

Try to find a Lean library in the workspace with the given name.

Equations

• Lake.Workspace.findLeanLib? name self = Array.findSomeRev? self.packages fun (pkg : Lake.Package) => Lake.Package.findLeanLib? name pkg

def Lake.Workspace.findLeanExe? (name : Lake.Name) (self : Lake.Workspace) : Option Lake.LeanExe

Try to find a Lean executable in the workspace with the given name.

Equations

• Lake.Workspace.findLeanExe? name self = Array.findSomeRev? self.packages fun (pkg : Lake.Package) => Lake.Package.findLeanExe? name pkg

def Lake.Workspace.findExternLib? (name : Lake.Name) (self : Lake.Workspace) : Option Lake.ExternLib

Try to find an external library in the workspace with the given name.

Equations

• Lake.Workspace.findExternLib? name self = Array.findSomeRev? self.packages fun (pkg : Lake.Package) => Lake.Package.findExternLib? name pkg

def Lake.Workspace.findTargetConfig? (name : Lake.Name) (self : Lake.Workspace) : Option ((pkg : Lake.Package) × Lake.TargetConfig (Lake.Package.name pkg) name)

Try to find a target configuration in the workspace with the given name.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Workspace.addModuleFacetConfig {name : Lake.Name} (cfg : Lake.ModuleFacetConfig name) (self : Lake.Workspace) : Lake.Workspace

Add a module facet to the workspace.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Workspace.findModuleFacetConfig? (name : Lake.Name) (self : Lake.Workspace) : Option (Lake.ModuleFacetConfig name)

Try to find a module facet configuration in the workspace with the given name.

Equations

• Lake.Workspace.findModuleFacetConfig? name self = Lake.DRBMap.find? self.moduleFacetConfigs name

def Lake.Workspace.addPackageFacetConfig {name : Lake.Name} (cfg : Lake.PackageFacetConfig name) (self : Lake.Workspace) : Lake.Workspace

Add a package facet to the workspace.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Workspace.findPackageFacetConfig? (name : Lake.Name) (self : Lake.Workspace) : Option (Lake.PackageFacetConfig name)

Try to find a package facet configuration in the workspace with the given name.

Equations

• Lake.Workspace.findPackageFacetConfig? name self = Lake.DRBMap.find? self.packageFacetConfigs name

def Lake.Workspace.addLibraryFacetConfig {name : Lake.Name} (cfg : Lake.LibraryFacetConfig name) (self : Lake.Workspace) : Lake.Workspace

Add a library facet to the workspace.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Workspace.findLibraryFacetConfig? (name : Lake.Name) (self : Lake.Workspace) : Option (Lake.LibraryFacetConfig name)

Try to find a library facet configuration in the workspace with the given name.

Equations

• Lake.Workspace.findLibraryFacetConfig? name self = Lake.DRBMap.find? self.libraryFacetConfigs name

def Lake.Workspace.binPath (self : Lake.Workspace) : Lake.SearchPath

The workspace's binary directories (which are added to Path).

Equations

• Lake.Workspace.binPath self = Array.foldr (fun (pkg : Lake.Package) (dirs : Lake.SearchPath) => Lake.Package.binDir pkg :: dirs) [] self.packages (Array.size self.packages)

def Lake.Workspace.leanPath (self : Lake.Workspace) : Lake.SearchPath

The workspace's Lean library directories (which are added to LEAN_PATH).

Equations

• Lake.Workspace.leanPath self = Array.foldr (fun (pkg : Lake.Package) (dirs : Lake.SearchPath) => Lake.Package.leanLibDir pkg :: dirs) [] self.packages (Array.size self.packages)

def Lake.Workspace.leanSrcPath (self : Lake.Workspace) : Lake.SearchPath

The workspace's source directories (which are added to LEAN_SRC_PATH).

Equations

• One or more equations did not get rendered due to their size.

def Lake.Workspace.sharedLibPath (self : Lake.Workspace) : Lake.SearchPath

The workspace's shared library path (e.g., for --load-dynlib). This is added to the sharedLibPathEnvVar by lake env.

Equations

• Lake.Workspace.sharedLibPath self = Array.foldr (fun (pkg : Lake.Package) (dirs : Lake.SearchPath) => Lake.Package.nativeLibDir pkg :: dirs) [] self.packages (Array.size self.packages)

def Lake.Workspace.augmentedPath (self : Lake.Workspace) : Lake.SearchPath

The detected PATH of the environment augmented with the workspace's binDir and Lean and Lake installations' binDir.

Equations

• Lake.Workspace.augmentedPath self = Lake.Workspace.binPath self ++ Lake.Env.path self.lakeEnv

def Lake.Workspace.augmentedLeanPath (self : Lake.Workspace) : Lake.SearchPath

The detected LEAN_PATH of the environment augmented with the workspace's leanPath and Lake's libDir.

Equations

• Lake.Workspace.augmentedLeanPath self = Lake.Workspace.leanPath self ++ Lake.Env.leanPath self.lakeEnv

def Lake.Workspace.augmentedLeanSrcPath (self : Lake.Workspace) : Lake.SearchPath

The detected LEAN_SRC_PATH of the environment augmented with the workspace's leanSrcPath and Lake's srcDir.

Equations

• Lake.Workspace.augmentedLeanSrcPath self = Lake.Workspace.leanSrcPath self ++ Lake.Env.leanSrcPath self.lakeEnv

def Lake.Workspace.augmentedSharedLibPath (self : Lake.Workspace) : Lake.SearchPath

Equations

• Lake.Workspace.augmentedSharedLibPath self = Lake.Workspace.sharedLibPath self ++ Lake.Env.sharedLibPath self.lakeEnv

def Lake.Workspace.augmentedEnvVars (self : Lake.Workspace) : Array (String × Option String)

The detected environment augmented with Lake's and the workspace's paths. These are the settings use by lake env / Lake.env to run executables.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Workspace.clean (self : Lake.Workspace) : IO Unit

Remove all packages' build outputs (i.e., delete their build directories).

Equations

• Lake.Workspace.clean self = Array.forM (fun (pkg : Lake.Package) => Lake.Package.clean pkg) self.packages 0