Lake CLI Reference: All Commands and Flags for Lean 4

Lake is the official build system and package manager for Lean 4. It manages dependencies, orchestrates builds, runs tests, handles caching, and integrates with the Lean language server. Every Lake project is defined by a configuration file (lakefile.toml or lakefile.lean) at the root of the package directory. Access the built-in help at any time with:

lake --help          # print top-level usage
lake help <command>  # print help for a specific command
lake <command> -h    # same as above

Global options

These options can be placed before the subcommand name and apply to all commands.

Basic options

Flag	Description
`--version`	Print the Lake version and exit
`--help`, `-h`	Print help for the program or the current command and exit
`--dir`, `-d=<path>`	Use the package configuration found in the specified directory
`--file`, `-f=<path>`	Use a specific file as the package configuration
`-K key[=value]`	Set a configuration file option (key/value pair)
`--old`	Only rebuild modified modules; ignore transitive dependency changes
`--rehash`, `-H`	Hash all files for build traces; do not trust cached `.hash` files
`--update`	Update dependencies on load (e.g., before a build)
`--packages=<file>`	JSON file of package entries that override the manifest
`--reconfigure`, `-R`	Re-elaborate configuration files instead of using pre-built OLeans
`--keep-toolchain`	Do not update the toolchain when updating the workspace
`--allow-empty`	Accept bare builds with no default targets configured
`--no-build`	Exit immediately if a build target is not already up-to-date
`--no-cache`	Build packages locally; do not download build caches
`--try-cache`	Attempt to download build caches for supported packages
`--json`, `-J`	Output JSON-formatted results (used with `lake query`)
`--text`	Output results as plain text (used with `lake query`)

Output options

Flag	Description
`--quiet`, `-q`	Hide informational logs and the progress indicator
`--verbose`, `-v`	Show trace logs (command invocations) and built targets
`--ansi` / `--no-ansi`	Toggle ANSI escape codes for prettified terminal output
`--log-level=<lv>`	Minimum log level to output on success (`trace`, `info`, `warning`, `error`)
`--fail-level=<lv>`	Minimum log level that causes a build failure (default: `error`)
`--iofail`	Fail the build if any I/O or info log is emitted (equivalent to `--fail-level=info`)
`--wfail`	Fail the build if any warning is logged (equivalent to `--fail-level=warning`)

Package creation

`lake new`

Create a new Lean package in a new directory.

lake [+<lean-version>] new <name> [<template>][.<language>]

Scaffolds a new package named <name> inside a freshly-created directory with the same name. The optional +<lean-version> prefix (provided by Elan) pins the package to a specific Lean version. Templates

Template	Contents
`std` (default)	Library + executable
`exe`	Executable only
`lib`	Library only
`math-lax`	Library with a Mathlib dependency
`math`	Library with Mathlib standards for linting and workflows

Append .lean or .toml to choose the config file language (default: .toml).

# Create a standard package (TOML config, latest Lean)
lake new MyProject

# Create a math library using Lean 4.x.0
lake +leanprover/lean4:v4.x.0 new MyMathLib math.lean

# Create an executable-only project with a TOML config
lake new MyApp exe.toml

`lake init`

Create a Lean package in the current directory.

lake [+<lean-version>] init [<name>] [<template>][.<language>]

Behaves like lake new but initialises the package inside the working directory rather than a subdirectory. Use lake init . or a bare lake init to derive the package name from the directory name.

# Init using the current directory's name
lake init

# Init with an explicit name and exe template
lake init MyProject exe

Templates can be suffixed with .lean or .toml to control the config language. The default config language is TOML.

Building

`lake build`

Build one or more targets.

lake build [<targets>...] [-o <mappings-file>]

A bare lake build builds the default target(s) of the root package. Package dependencies are not automatically updated during a build; run lake update first if needed. Target syntax

[@[<package>]/][<target>|[+]<module>][:<facet>]

Syntax	Meaning
`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` inside package `a`
`@a/+A:c`	C file of module `A` inside package `a`
`:foo`	Facet `foo` of the root package
`Foo/Bar.lean:o`	Object file compiled from the module whose source is `Foo/Bar.lean`

Library facets

Facet	Output
`leanArts` (default)	Lean artifacts (`.olean`, `.ilean`, `*.c` files)
`static`	Static archive (`*.a`)
`shared`	Shared library (`.so` / `.dll` / `*.dylib`)

Module facets

Facet	Output
`deps`	Module dependencies (imports, shared libraries, etc.)
`leanArts` (default)	Lean artifacts (`.olean`, `.ilean`, `*.c`)
`olean`	OLean binary blob (for importers)
`ilean`	ILean binary blob (for the LSP server)
`c`	Compiled C file
`bc`	Compiled LLVM bitcode file
`c.o`	Object file compiled from the C file
`bc.o`	Object file compiled from the LLVM bitcode file
`o`	Object file compiled from the configured backend
`dynlib`	Shared library (e.g., for `--load-dynlib`)

# Build default targets
lake build

# Build a specific library target
lake build MyLib

# Build module MyLib.Core as an olean
lake build +MyLib.Core:olean

# Build C file for a module using its source path
lake build Foo/Bar.lean:c

# Build and write output mappings (for use with lake cache put)
lake build -o outputs.jsonl

Use --no-build to check whether everything is already up-to-date without actually building anything.

`lake query`

Build targets and print their results to stdout.

lake query [<targets>...]

Works like lake build but outputs the build results on standard output and reports progress on standard error. Results are printed in the same order as specified on the command line, each ending with a newline. Targets with no output configured are printed as an empty string (or null in JSON mode). Use --json / -J for machine-readable JSON output, or --text for raw strings.

# Query the default targets
lake query

# Query a specific target and get JSON output
lake query --json MyLib

`lake check-build`

Check whether any default build targets are configured.

lake check-build

Exits with code 0 if the root package has at least one default target configured, or code 1 otherwise. Does not verify that the configured targets are actually valid or buildable — it only checks that some targets are specified.

lake check-build && echo "Default targets exist"

Running executables

`lake exe`

Build an executable target and run it in Lake’s environment.

lake exe <exe-target> [<args>...]

Alias: lake exec Looks up the named executable in the workspace, builds it if it is out of date, and then executes it with the given arguments inside Lake’s environment. The target can be specified as <name> or <package>/<name>.

# Run the executable named `myapp`
lake exe myapp

# Pass arguments to the executable
lake exe myapp --input data.json

# Run an executable from a specific package
lake exe mypackage/mytool --verbose

lake exe sets up the same environment variables as lake env, ensuring the executable can find Lean libraries and other workspace resources.

Testing

`lake test`

Test the root package using its configured test driver.

lake test [-- <args>...]

A test driver is configured by either:

Setting the testDriver field in the package configuration, or
Tagging a script, executable, or library with @[test_driver].

A definition in a dependency can be used as a test driver via the <pkg>/<name> syntax for testDriver.

Driver type	Behaviour
Script	Run with `testDriverArgs` from config plus CLI `args`
Executable	Built first, then run like a script
Library	Only built (arguments cannot be passed)

# Run the configured test driver
lake test

# Pass extra arguments to the test driver
lake test -- --filter MyTest

`lake check-test`

Check whether a test driver is properly configured.

lake check-test

Exits with code 0 if the root package has a test driver specified, or code 1 otherwise. Does not verify that the driver actually exists in the package or its dependencies.

lake check-test && echo "Test driver configured"

Linting

`lake lint`

Lint the root package.

lake lint [OPTIONS] [<MODULE>...] [-- <args>...]

By default, runs the package’s configured lint driver. If builtinLint = true is set in the package configuration, builtin lints also run. Options

Option	Description
`--builtin-lint`	Run builtin environment and text linters
`--builtin-only`	Run only builtin linters; skip the external lint driver
`--linters <spec>`	Override linter options for the lint build. `<spec>` is a comma-separated list of linter names, optionally prefixed with `-` to disable. A `.` prefix is shorthand for `linter.` (e.g., `.foo` → `linter.foo`). Repeatable; later entries override earlier ones for the same linter
`--lint-only <spec>`	Like `--linters`, but report only the linters the spec positively enables, suppressing all others (including default-on linters not named). Switches between `--linters` and `--lint-only` replace the prior spec
`--record-exceptions`	Record each linter warning as a `set_option <linter> false in` exception by editing the offending source files in place. Implies `--builtin-lint`
`--code-quality`	Record each linter warning as a code quality check result and run registered code quality checks. Skips the lint driver

Positional MODULE arguments narrow the scope of builtin lints only; if omitted, the default target roots are used. The lint driver is invoked with lintDriverArgs from the package config plus any arguments after --; the MODULE list is not passed to it.

# Run the configured lint driver
lake lint

# Run builtin lints only on specific modules
lake lint --builtin-only MyLib.Core MyLib.Utils

# Enable a specific linter and report only its output
lake lint --lint-only .unusedVariables

# Automatically silence warnings by editing source files
lake lint --record-exceptions

# Pass extra args to an external lint driver
lake lint -- --strict

`lake check-lint`

Check whether a lint driver is properly configured.

lake check-lint

Exits with code 0 if the root package has a lint driver specified (or builtinLint = true), or code 1 otherwise.

lake check-lint && echo "Lint driver configured"

Cleaning

`lake clean`

Remove build outputs.

lake clean [<package>...]

If no package names are specified, deletes the build directories of every package in the workspace. Otherwise, only the build directories of the named packages are removed.

# Clean all packages in the workspace
lake clean

# Clean only specific packages
lake clean MyLib MyApp

Dependency management

`lake update`

Update dependencies and save them to the manifest.

lake update [<package>...]

Alias: lake upgrade Updates lake-manifest.json, downloading and upgrading packages as needed. For each new (transitive) git dependency, the appropriate commit is cloned into a subdirectory of packagesDir. Local dependencies are not copied.

If package names are specified, only those dependencies are upgraded to the latest version compatible with the configuration (or removed if they were dropped from the config).
A bare lake update upgrades all dependencies.

# Upgrade all dependencies
lake update

# Upgrade only specific packages
lake update mathlib std

# Update deps and immediately build
lake update && lake build

If there are dependencies on multiple versions of the same package, the materialized version is undefined.

Scripts

`lake script`

Manage and run workspace scripts.

lake script <COMMAND>

Subcommand	Description
`list`	List all available scripts in the workspace
`run [<package>/]<script> [<args>...]`	Run a script, optionally from a specific package
`doc [<package>/]<script>`	Print the docstring of a script

# List all scripts
lake script list
lake scripts        # shorthand

# Run a script named `generate`
lake script run generate
lake run generate   # shorthand

# Run with arguments
lake run generate -- --output dist/

# Run the default script(s)
lake run

# Print a script's documentation
lake script doc generate

`lake run`

Shorthand for lake script run.

lake run [[<package>/]<script>] [<args>...]

A bare lake run executes the default script(s) of the root package with no arguments.

Environment

`lake env`

Execute a command in Lake’s environment.

lake env [<cmd>] [<args>...]

Spawns a new process running <cmd> with its environment set up according to the detected Lean/Lake installations and workspace configuration (if present). Environment variables set by lake env

Variable	Value
`LAKE`	Path to the detected Lake executable
`LAKE_HOME`	Path to the Lake home directory
`LEAN_SYSROOT`	Path to the Lean toolchain directory
`LEAN_AR`	Path to the Lean `ar` binary
`LEAN_CC`	Path to the detected C compiler (if not using the bundled one)
`LEAN_PATH`	Lake’s and the workspace’s Lean library directories (appended)
`LEAN_SRC_PATH`	Lake’s and the workspace’s source directories (appended)
`PATH`	Lean’s, Lake’s, and the workspace’s binary directories (appended)
`PATH`	Lean’s and the workspace’s library directories (Windows)
`DYLD_LIBRARY_PATH`	Lean’s and the workspace’s library directories (macOS)
`LD_LIBRARY_PATH`	Lean’s and the workspace’s library directories (Linux/other)

A bare lake env (no <cmd>) prints all set variables in NAME=VALUE format.

# Print all environment variables Lake would set
lake env

# Run a custom script in Lake's environment
lake env bash my-script.sh

# Check the Lean version available in the workspace
lake env lean --version

`lake lean`

Elaborate a Lean file in the context of the Lake workspace.

lake lean <file> [-- <args>...]

Builds the imports of the given file, then runs lean on it using the root package’s additional Lean arguments plus any <args> passed after --. The lean process is executed inside Lake’s environment.

# Elaborate a standalone file using workspace context
lake lean scripts/Generate.lean

# Pass extra arguments to lean
lake lean MyFile.lean -- --profile

Language server

`lake serve`

Start the Lean language server.

lake serve [-- <args>...]

Runs lean --server using the package configuration’s moreServerArgs field plus any additional <args> provided after --. This is the command editors and IDEs use when starting the Lean language server for a project.

# Start the language server (typically called by your editor extension)
lake serve

# Pass extra arguments to the server
lake serve -- --memory-heartbeat=200000

Most users do not need to run lake serve directly. Editor extensions such as the VS Code Lean 4 extension invoke it automatically when you open a Lean project.

Cloud cache

`lake cache`

Manage the Lake build artifact cache.

lake cache <COMMAND>

Subcommand	Description
`get [<mappings>]`	Download build outputs from a remote service into the local cache
`put <mappings>`	Upload build outputs from the local cache to a remote service
`add <mappings>`	Add input-to-output mappings to the local cache
`clean`	Remove all files from the local Lake cache
`services`	Print configured remote cache services
`stage <mappings> <staging-directory>`	Copy build outputs from the cache to a staging directory
`unstage <staging-directory>`	Copy build outputs from a staging directory back into the cache
`put-staged <staging-directory>`	Upload build outputs from a staging directory to a remote service

lake cache get

Download build outputs from a remote service into the local Lake cache.

lake cache get [<mappings>]

Options

Option	Description
`--max-revs=<n>`	Backtrack up to `n` Git revisions when searching for cached outputs (default: 100; set `0` for unlimited)
`--rev=<commit-hash>`	Use this exact Git revision for artifact lookup
`--service=<name>`	Cache service to fetch from
`--repo=<github-repo>`	GitHub repository for scope (Reservoir or custom endpoint)
`--platform=<triple>`	Override the target platform triple
`--toolchain=<name>`	Override the Lean toolchain identifier
`--scope=<remote-scope>`	Set a fixed scope for a custom endpoint
`--mappings-only`	Only download input-to-output mappings; delay artifact downloads
`--force-download`	Re-download artifacts even if they already exist locally

Without a mappings file or --scope/--repo, Lake uses Reservoir to download caches for each dependency in the workspace. Non-Reservoir dependencies are skipped.

# Download caches for all Reservoir dependencies
lake cache get

# Download caches using a specific mappings file and scope
lake cache get outputs.jsonl --scope leanprover/lean4

# Download from a fork on Reservoir
lake cache get --repo myfork/mathlib4

# Fetch only the mapping index, not the artifacts yet
lake cache get --mappings-only

lake cache put

Upload build outputs from the local cache to a remote service.

lake cache put <mappings> <scope-option>

Reads the input-to-output mappings from <mappings> (produced by lake build -o <mappings>) and uploads the corresponding artifacts to a remote cache. Files are uploaded using the AWS Signature Version 4 protocol via curl; the authentication key must be set in the LAKE_CACHE_KEY environment variable.At least one of --scope or --repo must be provided.Scope options

Option	Description
`--scope=<remote-scope>`	Use this verbatim scope
`--repo=<github-repo>`	Derive scope from the repository + toolchain + platform
`--toolchain=<name>`	With `--repo`, override the toolchain identifier
`--platform=<triple>`	With `--repo`, override the platform triple

# Build and capture output mappings, then upload
lake build -o outputs.jsonl
lake cache put outputs.jsonl --repo leanprover/lean4

# Upload with a fixed scope
lake cache put outputs.jsonl --scope my-org/my-package

Artifacts are uploaded before mappings so that if a mapping exists, the corresponding artifacts can be assumed to exist too.

lake cache add

Add input-to-output mappings to the local cache.

lake cache add <mappings>

Reads a list of mappings from the file and adds them to the local Lake cache. Existing mappings are overwritten unless --no-overwrite is specified.Options

Option	Description
`--service=<name>`	Cache service from which artifacts can be fetched lazily
`--scope=<remote-scope>`	Prefix of artifacts within the service
`--repo=<github-repo>`	For Reservoir, a GitHub repository scope
`--no-overwrite`	Do not overwrite mappings that already exist in the cache

lake cache add outputs.jsonl --service reservoir

lake cache clean

Remove all files from the local Lake cache.

lake cache clean

Deletes the configured Lake cache directory. If a workspace configuration exists, deletes the cache directory it uses; otherwise deletes the default system cache directory.

lake cache clean

lake cache services

Print configured remote cache services.

lake cache services

Prints the name of each configured remote cache service, one per line. Additional services can be added by editing the Lake system configuration (usually ~/.lake/config.toml, configurable via LAKE_CONFIG).Example system configuration:

cache.defaultService = "my-s3"
cache.defaultUploadService = "my-s3"

[[cache.service]]
name = "my-s3"
kind = "s3"
artifactEndpoint = "https://my-s3.com/a0"
revisionEndpoint = "https://my-s3.com/r0"

If no cache.defaultService is configured, Lake uses Reservoir by default.

lake cache services

Staging commands

The staging commands allow a two-step upload workflow useful in CI pipelines that separate build and upload steps.lake cache stage <mappings> <staging-directory> [--force-overwrite]Copy build outputs from the local cache into a staging directory. Artifacts already present in the staging directory are not overwritten unless --force-overwrite is specified.

lake cache stage outputs.jsonl ./staging

lake cache unstage <staging-directory> [--force-overwrite]Copy build outputs from a staging directory back into the local cache. Mappings and artifacts already in the cache are not overwritten unless --force-overwrite is specified.

lake cache unstage ./staging

lake cache put-staged <staging-directory>Upload build outputs from a staging directory directly to a remote service (does not load workspace configuration, so platform and toolchain must be set manually if required).

lake cache put-staged ./staging --repo leanprover/lean4 \
  --platform x86_64-linux --toolchain leanprover/lean4:v4.x.0

Import minimization

`lake shake`

Minimize imports in Lean source files.

lake shake [OPTIONS] [<MODULE>...]

Analyzes generated .olean files to find unused imports and suggests (or applies) removals. If no modules are specified, the package’s default targets are used. Options

Option	Description
`--force`	Skip the `lake build --no-build` sanity check that oleans are up-to-date
`--keep-implied`	Preserve imports that are implied by other imports
`--keep-prefix`	Prefer parent module imports over specific submodule imports
`--keep-public`	Preserve all `public` imports for API stability
`--add-public`	Add new imports as `public` if they were in the original public closure
`--explain`	Show which constants require each import
`--fix`	Apply suggested fixes directly to source files
`--gh-style`	Output diagnostics in GitHub problem matcher format

Source annotations You can embed annotations in source files to control shake behavior:

Annotation	Effect
`module -- shake: keep-downstream`	Preserve this module in all downstream modules
`module -- shake: keep-all`	Preserve all existing imports in this module
`import X -- shake: keep`	Preserve this specific import

# Check for unused imports in default targets (dry run)
lake shake

# Check a specific module tree
lake shake MyLib

# Apply fixes automatically
lake shake --fix

# Explain why each import is needed
lake shake --explain MyLib.Core

# Output in GitHub Actions annotation format
lake shake --gh-style

lake shake requires up-to-date .olean files. Run lake build first (or use --force to skip the check).

Build artifact distribution

`lake pack`

Pack build artifacts into a distributable archive.

lake pack [<file.tgz>]

Packs the root package’s buildDir into a gzip tar archive using tar. If no output path is given, the archive is created in the package’s .lake directory using the name from the buildArchive configuration setting.

lake pack does not build anything. It only archives already-built artifacts.

# Pack into the default archive location
lake pack

# Pack into a custom file
lake pack release/mypackage-v1.0.tar.gz

`lake unpack`

Unpack build artifacts from a distributed archive.

lake unpack [<file.tgz>]

Extracts a gzip tar archive into the root package’s buildDir. If no file path is provided, uses the package’s buildArchive in its .lake directory.

# Unpack from the default archive location
lake unpack

# Unpack from a specific file
lake unpack release/mypackage-v1.0.tar.gz

`lake upload`

Upload build artifacts to a GitHub release.

lake upload <tag>

Packs the root package’s buildDir into a tar.gz archive and uploads it as an asset to the pre-existing GitHub release identified by <tag>, using the gh CLI tool.

# Upload artifacts to the v1.0.0 release
lake upload v1.0.0

This command requires the GitHub CLI (gh) to be installed and authenticated. The release must already exist before running lake upload.

Configuration translation

`lake translate-config`

Translate the package configuration file to a different language.

lake translate-config <lang> [<out-file>]

Translates the loaded package configuration into another of Lake’s supported languages:

Language	Extension
`lean`	`.lean`
`toml`	`.toml`

If <out-file> is not specified, the translated file is written alongside the original using the new extension, and the original is renamed with a .bak suffix. If the output file already exists, Lake will error rather than overwrite it.

Translation is lossy: comments and formatting are not preserved, and non-declarative configuration will be discarded.

# Convert a TOML config to Lean
lake translate-config lean

# Convert a Lean config to TOML, writing to a specific file
lake translate-config toml lakefile.toml

Getting Started with Lake

Configuration

CLI Reference

Documentation Index

​Global options

​Basic options

​Output options

​Package creation

​lake new

​lake init

​Building

​lake build

​lake query

​lake check-build

​Running executables

​lake exe

​Testing

​lake test

​lake check-test

​Linting

​lake lint

​lake check-lint

​Cleaning

​lake clean

​Dependency management

​lake update

​Scripts

​lake script

​lake run

​Environment

​lake env

​lake lean

​Language server

​lake serve

​Cloud cache

​lake cache

​Import minimization

​lake shake

​Build artifact distribution

​lake pack

​lake unpack

​lake upload

​Configuration translation

​lake translate-config

Build docs developers (and LLMs) love

Global options

Basic options

Output options

Package creation

`lake new`

`lake init`

Building

`lake build`

`lake query`

`lake check-build`

Running executables

`lake exe`

Testing

`lake test`

`lake check-test`

Linting

`lake lint`

`lake check-lint`

Cleaning

`lake clean`

Dependency management

`lake update`

Scripts

`lake script`

`lake run`

Environment

`lake env`

`lake lean`

Language server

`lake serve`

Cloud cache

`lake cache`

Import minimization

`lake shake`

Build artifact distribution

`lake pack`

`lake unpack`

`lake upload`

Configuration translation

`lake translate-config`