Reference
Command map
This page lists lev commands by task and command family. The linked guides contain complete examples, edge cases, and behavior.
Common entry points
| Task | Commands | Guide |
|---|---|---|
| Verify a locked checkout | lev inspect, lev doctor, lev sync --frozen | Getting started |
| Minimize broad imports | lev shake, lev inspect imports | Import minimization |
| Investigate a slow build | lev --timings build, lev profile, lev inspect performance --files | Profiling |
| Define repository checks | lev verify, lev check, lev task | Automation |
lev sync --frozen is for a checkout that already contains matching lev.lock and lake-manifest.json files. A project adopting lev for the first time needs to create and review its lock before using the frozen workflow.
Help, top-level surface, and direct shortcuts
Discover commands
lev --help
lev inspect --help
lev inspect performance --help
lev workspace --help
lev completions bashThe visible curated top level has fourteen commands: init, sync, lock, deps, inspect, run, build, toolchain, cache, doctor, check, shake, profile, and verify. Advanced roots such as workspace, task, matrix, script, watch, project, test, and lint remain available without crowding the first screen.
Direct familiar commands
lev doctorlev shakelev profilelev verify
Grouped counterparts
lev inspect environmentlev inspect importslev inspect performancelev check
| Global option | Meaning |
|---|---|
--project PATH | Start project discovery from an explicit path. |
-q, --quiet | Suppress lev informational output; delegated command behavior remains its own. |
-v, --verbose | Show cache reuse and orchestration details. |
--no-progress | Hide progress updates from long-running operations. |
--local | Run eligible commands in a persistent local workspace. |
--timings | Print total and recorded phase durations to stderr. |
--cache-dir PATH | Override LEV_CACHE_DIR. |
--data-dir PATH | Override LEV_DATA_DIR for persistent toolchain objects. |
Environment variables
Every variable has a command-line equivalent, so scripts can choose whichever form is easier to review. Command-line flags win when both are present.
| Variable | Flag | Meaning |
|---|---|---|
LEV_CACHE_DIR | --cache-dir | Shared cache location for Git objects, dependency environments, Lake artifacts, and local workspaces. |
LEV_DATA_DIR | --data-dir | Persistent verified toolchain object store. |
Project lifecycle
lev initCreate a standard Lake project pinned to a Lean toolchain.lev syncMaterialize the toolchain and revisions from lake-manifest.json, then refresh lev.lock.lev lockGenerate or verify base and version-specific environment locks.lev project pinChange the project's lean-toolchain selector.lev project useMake an already resolved environment the project default.lev inspectSummarize the project, toolchain, lock, stores, and available build metadata.lev project auditCheck local lock, toolchain, and dependency checkout integrity.lev project exportWrite dependency inventory or CycloneDX SBOM data.lev selfCheck for updates, install a released binary, or uninstall lev.lev completionsGenerate completion definitions for a supported shell.See adopting an existing project and lock modes and drift recovery for complete examples.
Build and execution
lev buildSynchronize, then invoke lake build.lev runRun an arbitrary process in the selected environment.lev run lake testRun the project's Lake test driver.lev run lake lintRun the project's Lake lint driver.lev check --file FILE.leanElaborate one Lean source file through Lake.lev check [TARGET...]Run the ordered project verification gate.lev taskList or run commands configured in lev.toml.lev scriptRun or check one Lean file with inline dependency metadata.lev watchDebounce project file events and rerun a command.lev matrixRun one command in several isolated Lean environments.lev check --file FILE.lean is the explicit new-script form for single-file elaboration. The older positional form still works in compatibility cases, but --file avoids ambiguity with project build targets. Put Lean flags after --, as in lev check --file Root.lean -- -Dpp.universes=true.
Dependencies and tools
lev deps addAdd or replace a dependency in lakefile.toml.lev deps removeRemove a declarative dependency.lev deps updateUpdate locked dependencies through Lake.lev deps outdatedReport newer compatible Reservoir releases.lev deps upgradePreview or apply a direct-dependency upgrade transaction.lev depsInspect dependencies recorded by the Lake manifest.lev deps treePrint the resolved dependency tree.lev deps whyExplain why a package occurs in the dependency graph.lev toolchainInstall, list, garbage-collect, and remove Lean toolchains.lev toolInstall and run Lean package executables outside a project.See reviewable upgrades and toolchain selection.
Analysis and reproducibility
lev shake / lev inspect importsInfer, check, and transactionally apply minimal imports. Hidden compatibility spelling: lev imports.lev inspect graphRender project module imports as text, JSON, or Graphviz DOT.lev profile / lev inspect performanceMeasure repeated commands directly, or rank project files and compare baselines through the inspector.lev inspect buildRun a verbose Lake build and report changed trace inputs.lev doctor / lev inspect environmentCheck local tools, paths, project files, caches, and workspace state without creating cache state or walking build trees.lev inspect dependenciesExplain each selected revision from requests in materialized parent manifests.lev inspect declarationFind a declaration's module, source range, import, and Lean-checked type.lev inspect trustReport project declarations that reach axioms or are marked unsafe.lev verify / lev checkRun the fixed published phases, or add configured tasks and project policy.lev project bundleCreate a deterministic archive of locked project sources.lev project publishVerify and upload Lake artifacts to an existing GitHub release.lev cacheInspect, verify, transfer, and clean shared state.lev workspaceList, lock, sync, build, run, or shake configured Lake roots.lev inspect build reports observed changes around a real Lake build. Its reverse-import analysis describes potential source impact, not a claim about Lake's full internal job DAG.
Common recipes
| Need | Command |
|---|---|
| Reproduce CI without network | lev sync --frozen --offline |
| See where one build spent time | lev --timings build |
| Compare five warm builds | lev profile --warmup 1 --repeat 5 |
| Preserve current public imports | lev shake --check --keep-public --keep-implied |
| Apply Mathlib-style import policy | lev shake --fix --add-public --keep-implied --keep-prefix |
| Render an external import graph | lev inspect graph My.Main --external --format dot -o imports.dot |
| Explain transitive revision choices | lev inspect dependencies |
| Check the selected local environment | lev doctor |
| Run the fixed release gate | lev verify --clean --offline --strict --test --lint --imports |
| Preview direct dependency updates | lev deps upgrade --dry-run |
| Build every workspace member | lev workspace build --keep-going |
| Archive verified source | lev project bundle -o project.lev.tar.zst |
| Explain a failed build layer | lev -v --timings build |
| Recover intentional lock drift | lev lock && lev lock --check |
| Keep valid import edits from a failed batch | lev shake --fix --isolate --keep-public --keep-implied |
Contracts and diagnostics
- JSON contracts documents the outer envelope and the relationship between grouped and direct commands.
- Schema inventory lists every documented schema string by command family.
- Diagnostics and exits distinguishes observational commands, policy failures, and preserved child exit codes.
- Troubleshooting maps common symptoms to a focused follow-up command.
- Agent guidance links the repository skill and its operating assumptions.