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. The CLI arguments Lake was run with. Used by
lake update
to perform a restart of Lake on a toolchain update. A value ofnone
means that Lake is not restartable via the CLI.The packages within the workspace (in
require
declaration order).Name-package map of packages within the workspace.
- facetConfigs : DNameMap FacetConfig
Configuration map of facets defined in the workspace.
Instances For
Equations
The path to the workspace's directory (i.e., the directory of the root package).
Equations
Instances For
The workspace's configuration.
Equations
Instances For
The full path to the workspace's Lake directory (e.g., .lake
).
Equations
Instances For
The path to the workspace's remote packages directory relative to dir
.
Equations
Instances For
The workspace's Lake manifest.
Equations
Instances For
The path to the workspace file used to configure automatic package overloads.
Equations
Instances For
Add a package to the workspace.
Equations
Instances For
Check if the module is local to any package in the workspace.
Equations
Instances For
Check if the module is buildable by any package in the workspace.
Equations
Instances For
Returns the buildable module in the workspace whose source file is path
.
Equations
Instances For
Try to find a target configuration in the workspace with the given name.
Equations
Instances For
Try to find a target declaration in the workspace with the given name.
Equations
Instances For
Add a facet to the workspace.
Equations
Instances For
Try to find a facet configuration in the workspace with the given name.
Equations
Instances For
Add a module facet to the workspace.
Equations
Instances For
Try to find a module facet configuration in the workspace with the given name.
Equations
Instances For
Add a package facet to the workspace.
Equations
Instances For
Try to find a package facet configuration in the workspace with the given name.
Equations
Instances For
Add a library facet to the workspace.
Equations
Instances For
Try to find a library facet configuration in the workspace with the given name.
Equations
Instances For
The workspace's binary directories (which are added to Path
).
Equations
Instances For
The workspace's Lean library directories (which are added to LEAN_PATH
).
Equations
Instances For
The workspace's source directories (which are added to LEAN_SRC_PATH
).
Equations
Instances For
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
Instances For
The detected LEAN_PATH
of the environment augmented with
the workspace's leanPath
and Lake's libDir
.
Equations
Instances For
The detected LEAN_SRC_PATH
of the environment augmented with
the workspace's leanSrcPath
and Lake's srcDir
.
Equations
Instances For
Remove all packages' build outputs (i.e., delete their build directories).