structure Lake.Workspace : Type

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

• root : Package

  The root package of the workspace.

• lakeEnv : Env

  The detected Lake.Env of the workspace.

• lakeArgs? : Option (Array String)

  The CLI arguments Lake was run with. Used by lake update to perform a restart of Lake on a toolchain update. A value of none means that Lake is not restartable via the CLI.

• packages : Array Package

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

• packageMap : DNameMap NPackage

  Name-package map of packages within the workspace.

• facetConfigs : DNameMap FacetConfig

  Configuration map of facets defined in the workspace.

instance Lake.instNonemptyWorkspace : Nonempty Workspace

unsafe def Lake.OpaqueWorkspace.unsafeMk : Workspace → OpaqueWorkspace

Equations

• Lake.OpaqueWorkspace.unsafeMk = unsafeCast

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

Equations

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

instance Lake.OpaqueWorkspace.instCoeWorkspace : Coe Workspace OpaqueWorkspace

Equations

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

unsafe def Lake.OpaqueWorkspace.unsafeGet : OpaqueWorkspace → Workspace

Equations

• Lake.OpaqueWorkspace.unsafeGet = unsafeCast

@[implemented_by Lake.OpaqueWorkspace.unsafeGet]

opaque Lake.OpaqueWorkspace.get : OpaqueWorkspace → Workspace

@[implemented_by Lake.OpaqueWorkspace.unsafeMk]

opaque Lake.OpaqueWorkspace.mk : Workspace → OpaqueWorkspace

instance Lake.OpaqueWorkspace.instCoeWorkspace_1 : Coe OpaqueWorkspace Workspace

Equations

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

@[inline]

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

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

Equations

• self.dir = self.root.dir

@[inline]

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

The workspace's configuration.

Equations

• self.config = self.root.config.toWorkspaceConfig

@[inline]

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

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

Equations

• self.relLakeDir = self.root.relLakeDir

@[inline]

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

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

Equations

• self.lakeDir = self.root.lakeDir

@[inline]

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

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

Equations

• self.relPkgsDir = self.root.relPkgsDir

@[inline]

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

The workspace's dir joined with its relPkgsDir.

Equations

• self.pkgsDir = self.root.pkgsDir

@[inline]

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

The workspace's Lake manifest.

Equations

• self.manifestFile = self.root.manifestFile

@[inline]

def Lake.Workspace.packageOverridesFile (self : Workspace) : System.FilePath

The path to the workspace file used to configure automatic package overloads.

Equations

• self.packageOverridesFile = self.lakeDir / { toString := "package-overrides.json" }

def Lake.Workspace.addPackage (pkg : Package) (self : Workspace) : 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 : Lean.Name) (self : Workspace) : Option (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 : Lean.Name) (self : Workspace) : Option Script

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def Lake.Workspace.findModuleBySrc? (path : System.FilePath) (self : Workspace) : Option Module

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

Equations

• Lake.Workspace.findModuleBySrc? path self = Array.findSome? (fun (x : Lake.Package) => Lake.Package.findModuleBySrc? path x) self.packages

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def Lake.Workspace.findTargetConfig? (name : Lean.Name) (self : Workspace) : Option ((pkg : Package) × TargetConfig pkg.name 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.findTargetDecl? (name : Lean.Name) (self : Workspace) : Option ((pkg : Package) × NConfigDecl pkg.name name)

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

Equations

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

def Lake.Workspace.addFacetConfig {name : Lean.Name} (cfg : FacetConfig name) (self : Workspace) : Workspace

Add a facet to the workspace.

Equations

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

def Lake.Workspace.findFacetConfig? (name : Lean.Name) (self : Workspace) : Option (FacetConfig name)

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

Equations

• Lake.Workspace.findFacetConfig? name self = Lake.DRBMap.find? self.facetConfigs name

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

Add a module facet to the workspace.

Equations

• Lake.Workspace.addModuleFacetConfig cfg self = Lake.Workspace.addFacetConfig cfg.toFacetConfig self

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

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

Equations

• Lake.Workspace.findModuleFacetConfig? name self = (Lake.Workspace.findFacetConfig? name self).bind fun (x : Lake.FacetConfig name) => Lake.FacetConfig.toKind? Lake.Module.facetKind x

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

Add a package facet to the workspace.

Equations

• Lake.Workspace.addPackageFacetConfig cfg self = Lake.Workspace.addFacetConfig cfg.toFacetConfig self

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

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

Equations

• Lake.Workspace.findPackageFacetConfig? name self = (Lake.Workspace.findFacetConfig? name self).bind fun (x : Lake.FacetConfig name) => Lake.FacetConfig.toKind? Lake.Package.facetKind x

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

Add a library facet to the workspace.

Equations

• Lake.Workspace.addLibraryFacetConfig cfg self = Lake.Workspace.addFacetConfig cfg.toFacetConfig self

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

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

Equations

• Lake.Workspace.findLibraryFacetConfig? name self = (Lake.Workspace.findFacetConfig? name self).bind fun (x : Lake.FacetConfig name) => Lake.FacetConfig.toKind? Lake.LeanLib.facetKind x

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

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

Equations

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

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

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

Equations

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

def Lake.Workspace.leanSrcPath (self : Workspace) : System.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 : Workspace) : System.SearchPath

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

Equations

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

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

The detected PATH of the environment augmented with the workspace's binDir and Lean and Lake installations' binDir. On Windows, also adds the workspace shared library path.

Equations

• self.augmentedPath = if System.Platform.isWindows = true then self.binPath ++ self.sharedLibPath ++ self.lakeEnv.path else self.binPath ++ self.lakeEnv.path

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

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

Equations

• self.augmentedLeanPath = self.leanPath ++ self.lakeEnv.leanPath

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

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

Equations

• self.augmentedLeanSrcPath = self.leanSrcPath ++ self.lakeEnv.leanSrcPath

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

Equations

• self.augmentedSharedLibPath = self.lakeEnv.lean.sharedLibPath ++ self.sharedLibPath ++ self.lakeEnv.initSharedLibPath

def Lake.Workspace.augmentedEnvVars (self : 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 : Workspace) : IO Unit

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

Equations

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