- root : Lake.PackageThe root package of the workspace. 
- lakeEnv : Lake.EnvThe detect Lake.Envof the workspace.
- packages : Array Lake.PackageThe packages within the workspace (in requiredeclaration order).
- packageMap : Lake.DNameMap Lake.NPackageName-package map of packages within the workspace. 
- moduleFacetConfigs : Lake.DNameMap Lake.ModuleFacetConfigName-configuration map of module facets defined in the workspace. 
- packageFacetConfigs : Lake.DNameMap Lake.PackageFacetConfigName-configuration map of package facets defined in the workspace. 
- libraryFacetConfigs : Lake.DNameMap Lake.LibraryFacetConfigName-configuration map of library facets defined in the workspace. 
A Lake workspace -- the top-level package directory.
Instances For
The path to the workspace's directory (i.e., the directory of the root package).
Instances For
The workspace's configuration.
Instances For
The workspace's Lake manifest.
Instances For
Add a package to the workspace.
Instances For
Try to find a package within the workspace with the given name.
Instances For
Try to find a script in the workspace with the given name.
Instances For
Check if the module is local to any package in the workspace.
Instances For
Check if the module is buildable by any package in the workspace.
Instances For
Locate the named module in the workspace (if it is local to it).
Instances For
Try to find a Lean library in the workspace with the given name.
Instances For
Try to find a Lean executable in the workspace with the given name.
Instances For
Try to find an external library in the workspace with the given name.
Instances For
Try to find a target configuration in the workspace with the given name.
Instances For
Add a module facet to the workspace.
Instances For
Try to find a module facet configuration in the workspace with the given name.
Instances For
Add a package facet to the workspace.
Instances For
Try to find a package facet configuration in the workspace with the given name.
Instances For
Add a library facet to the workspace.
Instances For
Try to find a library facet configuration in the workspace with the given name.
Instances For
The workspace's binary directories (which are added to Path).
Instances For
The workspace's Lean library directories (which are added to LEAN_PATH).
Instances For
The workspace's source directories (which are added to LEAN_SRC_PATH).
Instances For
The detected PATH of the environment augmented with
the workspace's binDir and Lean and Lake installations' binDir.
Instances For
The detected LEAN_PATH of the environment augmented with
the workspace's leanPath and Lake's libDir.
Instances For
The detected LEAN_SRC_PATH of the environment augmented with
the workspace's leanSrcPath and Lake's srcDir.
Instances For
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.
Instances For
Remove all packages' build outputs (i.e., delete their build directories).