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.

• lakeConfig : LoadedLakeConfig

  The Lake configuration from the system configuration file.

• lakeCache : Cache

  The Lake cache.

• 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 with the root coming first).

• 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

@[implicit_reducible]

instance Lake.OpaqueWorkspace.instCoeGet : Coe OpaqueWorkspace Workspace

@[implemented_by _private.Lake.Config.Workspace.0.Lake.OpaqueWorkspace.unsafeGet]

opaque Lake.OpaqueWorkspace.get : OpaqueWorkspace → Workspace

@[implicit_reducible]

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

@[implemented_by _private.Lake.Config.Workspace.0.Lake.OpaqueWorkspace.unsafeMk]

opaque Lake.OpaqueWorkspace.mk : Workspace → OpaqueWorkspace

@[implicit_reducible]

instance Lake.OpaqueWorkspace.instCoeMk : Coe Workspace OpaqueWorkspace

def Lake.Package.defaultTargetRoots (self : Package) : Array Lean.Name

Returns the names of the root modules of the package's default targets.

@[inline]

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

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

@[inline]

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

The workspace's configuration.

@[inline]

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

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

@[inline]

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

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

@[inline]

def Lake.Workspace.enableArtifactCache? (ws : Workspace) : Option Bool

Whether the Lake artifact cache should be enabled by default for packages in the workspace.

@[deprecated Lake.Workspace.enableArtifactCache? (since := "2026-02-03")]

def Lake.Workspace.enableArtifactCache (ws : Workspace) : Bool

Whether the Lake artifact cache should be enabled by default for packages in the workspace.

def Lake.Workspace.isRootArtifactCacheWritable (ws : Workspace) : Bool

Whether the Lake artifact cache should is enabled for workspace's root package.

@[reducible, inline, deprecated Lake.Workspace.isRootArtifactCacheWritable (since := "2026-02-03")]

abbrev Lake.Workspace.isRootArtifactCacheEnabled (ws : Workspace) : Bool

Whether the Lake artifact cache should is enabled for workspace's root package.

@[inline]

def Lake.Workspace.defaultCacheService (ws : Workspace) : CacheService

Returns the cache service used by default for downloads (e.g., for lake cache get).

This is configured through cache.defaultService in the system Lake configuration. If unconfigured, Lake defaults to using Reservoir.

@[inline]

def Lake.Workspace.defaultCacheUploadService? (ws : Workspace) : Option CacheService

Returns the cache service (if any) used by default for uploads (e.g., for lake cache put).

This is configured through cache.defaultUploadService in the system Lake configuration.

@[inline]

def Lake.Workspace.findCacheService? (ws : Workspace) (service : String) : Option CacheService

Returns the configured cache service with the given name.

This is configured through cache.service entries in the global Lake configuration.

@[inline]

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

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

@[inline]

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

The workspace's dir joined with its relPkgsDir.

@[inline]

def Lake.Workspace.leanArgs (self : Workspace) : Array String

Arguments to pass to lean for files outside a library (e.g., via lake lean).

@[inline]

def Lake.Workspace.leanOptions (self : Workspace) : Lean.LeanOptions

Options to pass to lean for files outside a library (e.g., via lake lean).

@[inline]

def Lake.Workspace.serverOptions (self : Workspace) : Lean.LeanOptions

Options to pass to the Lean server when editing Lean files outside a library.

@[inline]

def Lake.Workspace.defaultTargetRoots (self : Workspace) : Array Lean.Name

Returns the names of the root modules of the workpace root's default targets.

@[inline]

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

The workspace's Lake manifest.

@[inline]

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

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

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

Add a package to the workspace.

@[inline]

def Lake.Workspace.findPackageByKey? (keyName : Lean.Name) (self : Workspace) : Option (NPackage keyName)

Returns the unique package in the workspace (if any) that is identified by keyName.

@[inline]

def Lake.Workspace.findPackageByName? (name : Lean.Name) (self : Workspace) : Option Package

Returns the first package in the workspace (if any) that has been assigned the name.

This can be used to find the package corresponding to a user-provided name. If the package's unique identifier is already available, use findPackageByKey? instead.

@[reducible, inline, deprecated "Use `findPackageByKey?` or `findPackageByName?` instead" (since := "2025-12-03")]

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

Deprecated. If attempting to find the package corresponding to a user-provided name, use findPackageByName?. Otherwise, if the package's unique identifier is available, use findPackageByKey?.

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

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

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

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

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

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

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

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

def Lake.Workspace.findModules (mod : Lean.Name) (self : Workspace) : Array Module

For each package in the workspace, locate the named, buildable, importable, local module.

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

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

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

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

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

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

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

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

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

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

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

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

def Lake.Workspace.findTargetDecl? (name : Lean.Name) (self : Workspace) : Option ((pkg : Package) × NConfigDecl pkg.keyName name)

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

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

Add a facet to the workspace.

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.

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

Add a module facet to the workspace.

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.

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

Add a package facet to the workspace.

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.

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

Add a library facet to the workspace.

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.

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

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

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

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

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

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

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.

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

The augmented PATH of the workspace environment.

This prepends the detected self.lakeEnv.path of the system environment with the workspace's binPath. On Windows, it also adds the workspace's sharedLibPath.

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.

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.

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

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

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

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

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