Documentation Index
Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt
Use this file to discover all available pages before exploring further.
Lake provides a set of CLI commands for compiling Lean source files, running executables, and managing build outputs. All build artefacts are written into the .lake/build/ directory so they never pollute your source tree.
lake build — Build Targets
lake build [<targets>...] [-o <mappings>]
lake build builds all default targets configured in the workspace’s root package (those listed in defaultTargets in lakefile.toml, or tagged @[default_target] in a Lean lakefile). If no default targets are configured, the command exits with an error unless --allow-empty is passed.
Package dependencies are not updated during a build. Run lake update separately to refresh the manifest.
Building Specific Targets
Pass one or more target specifiers to build only those targets:
lake build MyLib # build the library named MyLib
lake build hello # build the executable named hello
lake build @myPkg # build the default targets of package myPkg
lake build +MyModule # build module MyModule (Lean arts: .olean, .ilean, .c)
lake build +MyModule:c # build only the C file for MyModule
lake build MyLib:static # build the static library artifact (.a)
lake build MyLib:shared # build the shared library artifact (.so/.dll/.dylib)
Target Specifier Syntax
[@[<package>]/][<target>|[+]<module>][:<facet>]
| Specifier | What is built |
|---|
a | Default facet(s) of target a |
@a | Default target(s) of package a |
+A | Default facet(s) of module A |
@/a | Default facet(s) of target a in the root package |
@a/b | Default facet(s) of target b in package a |
@a/+A:c | The C file facet of module A in package a |
lake build Foo/Bar.lean:o # compile Foo/Bar.lean into a native object file
Library Facets
| Facet | Produces |
|---|
leanArts | .olean, .ilean, .c files (default) |
static | Static library (.a) |
shared | Shared library (.so, .dll, .dylib) |
Module Facets
| Facet | Produces |
|---|
leanArts | .olean, .ilean, .c files (default) |
olean | Binary blob of Lean data for importers |
ilean | Binary metadata for the Lean LSP server |
c | Compiled C file |
bc | Compiled LLVM bitcode file |
o | Native object file (compiled from C or LLVM backend) |
c.o | Object file compiled from the C file |
bc.o | Object file compiled from the LLVM bitcode file |
dynlib | Shared library (e.g. for --load-dynlib) |
lake exe — Build and Run an Executable
lake exe <exe-target> [<args>...]
lake exe is the most convenient way to build an executable and immediately run it. It:
- Looks up the named executable target in the workspace.
- Builds it if it is out-of-date.
- Runs it in Lake’s environment (with
LEAN_PATH, PATH, and library search paths configured correctly).
lake exe hello # build and run the 'hello' executable
lake exe hello -- arg1 arg2 # pass arguments to the executable
lake exe cache get # run the 'cache' tool (common for Mathlib)
lake exe is also available as lake exec. The tool it runs must be defined as a lean_exe target in the workspace.
lake clean — Remove Build Outputs
lake clean [<package>...]
lake clean # clean everything in the workspace
lake clean hello # clean only the 'hello' package
lake clean hello foo # clean 'hello' and 'foo'
lake clean removes the .lake/build/ directory contents but does not delete downloaded dependencies in .lake/packages/. To also remove dependencies, delete the .lake/packages/ directory manually.
0 if the workspace’s root package has any default targets configured, or code 1 otherwise. This command is useful in CI pipelines to fail early if no targets are set up.
lake check-build only verifies that some default targets are specified — it does not validate that those targets actually exist or build successfully.
Build Output Directory Layout
Lake writes all build outputs inside .lake/build/ (relative to the package root):
.lake/
build/
bin/ # compiled binary executables
lib/ # native libraries (.a, .so, .dll, .dylib)
lib/lean/ # Lean binary artifacts (.olean, .ilean files)
ir/ # intermediate results (.c, .o files)
packages/ # downloaded remote dependencies
lakefile.toml: binDir (default bin), nativeLibDir (default lib), leanLibDir (default lib/lean), and irDir (default ir). The buildDir field controls the top-level build directory (default: .lake/build).
Build Flags
--old — Only Rebuild Modified Modules
With --old, Lake only rebuilds modules whose own source file has changed. Normally, Lake also rebuilds any module that transitively depends on a changed module (i.e. if A imports B, and B changes, A is also rebuilt). The --old flag skips those transitive rebuilds, making incremental builds faster at the cost of potentially leaving some artefacts stale.
Using --old can produce inconsistent build outputs if transitive dependencies have changed. It is most useful during active development when you know your changes are isolated.
--verbose / -v — Show Build Trace
lake build --verbose
lake build -v
--verbose flag shows trace logs (the exact command invocations Lake runs) and prints the path of each successfully built target. This is useful for debugging build issues or inspecting what Lake is doing.
--no-build — Check Without Building
Exits immediately with an error if any build target is not already up-to-date. Useful in CI to verify that committed artefacts are current.
--rehash / -H — Force Hash Recomputation
Forces Lake to recompute hashes for all files rather than trusting cached .hash files. Use this if you suspect trace files have become corrupted.
Forces Lake to re-elaborate the lakefile from source rather than using cached .olean files for the configuration. Useful when the lakefile itself has been changed.
Other Useful Commands
lake query — Build and Print Results
lake query [<targets>...]
lake build, but also outputs the build results to stdout. With --json, results are formatted as JSON.
lake serve — Start the Language Server
lake serve [-- <args>...]
lean --server) with the package’s moreServerArgs configuration applied. This is typically invoked by editors (VS Code, Emacs, etc.) automatically.
lake env — Run a Command in Lake’s Environment
lake env <cmd> [<args>...]
LEAN_PATH, PATH, and library search paths configured for the workspace. A bare lake env prints the environment variables that would be set.
lake lean — Elaborate a File in the Workspace
lake lean <file> [-- <args>...]
lean on it using the workspace configuration. The process runs in Lake’s environment like lake env lean.
Complete Example
# Create and build a new package
lake new myproject
cd myproject
# Build all default targets
lake build
# Run the generated executable
lake exe myproject
# Build only the library's static artifact
lake build MyLib:static
# Check what Lake would do without rebuilding
lake build --verbose --no-build
# Clean all build outputs
lake clean
