Getting started

Install and smoke-test the binary

Terminal

cargo install --git https://github.com/Robertboy18/lev --locked lev-cli
lev --version
lev --help

If Rust is not installed, install it with rustup. The Cargo package is lev-cli; the executable is lev.

lev --version

Check that the shell is seeing the binary you just installed.

lev --help

Make sure the curated top-level surface is present: doctor, shake, profile, and verify should be visible.

lev doctor --help

Confirm that command-specific help is available before you use lev on a large checkout.

lev inspect

Outside a project, this still tells you what lev can establish from the current directory.

Project diagnosis and environment diagnosis are different reports. Bare lev inspect summarizes project files, lock state, and selected runtime. lev doctor checks the machine-facing side: Git, elan, Lean, Lake, cache paths, and workspace state. lev inspect environment is the grouped spelling of the same environment report.

Run the first project check

A new lev user and a project with a committed lev.lock need slightly different first runs. Start with the path that works for any Lake project:

Any Lake project

lev --version
lev inspect
lev doctor
lev sync
lev build

lev inspect

Read the project before you blame the build

This report gives you the Lakefile, manifest, lock, optional lev.toml, selected toolchain, and any build metadata lev can already see on disk.

lev doctor

Check the local runtime

If this machine cannot resolve the selected Lean and Lake, everything after this point fails for the wrong reason.

lev sync

Prepare the environment

On first adoption this resolves the existing Lake project and writes the lev state needed for later frozen runs. Plain sync may refresh an existing lock; use lev sync --frozen when the committed lock must remain unchanged.

lev build

Let Lake and Lean check the project

lev selects the prepared environment and delegates the build. Lean errors and Lake target failures remain the source of truth.

When the repository already commits lev.lock

A locked checkout can make stronger claims. Check that project inputs still match the lock, materialize without refreshing anything, then run the fixed verification gate offline:

Locked checkout

lev lock --check
lev sync --frozen
lev verify --offline

Add --test or --lint when the project defines those Lake drivers. A generic Lean package is not required to have either one.

Abridged project diagnosis

Lev 1.0.0 diagnosis
Project
  toolchain: leanprover/lean4:v4.18.0
  manifest: .../lake-manifest.json (0 packages)
  runtime: elan

Checks
  PASS  project    found .../project
  PASS  lakefile   parsed .../lakefile.toml
  PASS  manifest   parsed .../lake-manifest.json
  PASS  lock       .../lev.lock matches the project

Summary: 4 passed, 0 warnings, 0 errors

Abridged environment diagnosis

Lev 1.0.0 environment
Findings
  PASS  system.git                    git is available
  PASS  system.elan                   elan is available
  PASS  environment.runtime.selected  leanprover/lean4:v4.18.0 will run through elan
  PASS  environment.lean.version      Lean reports the selected version
  PASS  environment.lake.version      Lake reports the matching version

Summary: 5 passed, 0 warnings, 0 errors

The paths and versions will differ. The project report covers files and lock state; the environment report covers the local runtime.

Shell completions

lev completions prints the completion definition to stdout. Install it wherever your shell already loads completions, then start a new shell session.

Install completions

# Bash
lev completions bash > ~/.local/share/bash-completion/completions/lev

# Zsh
lev completions zsh > ~/.zfunc/_lev

# Fish
lev completions fish > ~/.config/fish/completions/lev.fish

Adopt lev in an existing Lake project

Adoption should be uneventful. lev reads the files a normal Lake project already has and adds one lock file of its own. You are not switching package formats or moving the project into a lev-only layout.

What stays exactly the same

lean-toolchain still names the Lean toolchain.
Your Lakefile still defines packages, targets, and dependencies.
lake-manifest.json is still Lake's resolved dependency graph.

What lev adds

lev.lock records environment identity and integrity data around that project.
Short commands such as lev build, lev doctor, and lev verify attach the right environment automatically.
lev.toml is optional and only matters when you want workspace members or named tasks.

lev sync

Discover, install, and materialize

Run lev from the project root or any subdirectory. It selects the nearest Lake project, resolves the toolchain, and prepares dependency state.

lev build

Build through the same Lake project

The common preflight happens first, then lev delegates to Lake. If Lake fails, you still read the Lean or Lake diagnostic first.

lev lock

Commit the environment state you meant

Review lev.lock the same way you review a manifest change. From that point on, another checkout and CI can prove they are using the same environment.

Typical adoption pass

cd my-formalization
lev sync
lev build
lev lock
git add lev.lock lean-toolchain lake-manifest.json
git commit -m "Lock Lean environment"

Create a new project

Create

lev init theorem-playground --lean stable
cd theorem-playground
lev build

Project shape

theorem-playground/
├── TheoremPlayground/
├── Main.lean
├── lakefile.toml
├── lean-toolchain
└── lev.lock

lev init creates a standard Lake package and pins the requested Lean selector in the ordinary lean-toolchain file. The project is still a normal Lean project; it just starts life with a lock.

When the first run fails, sort it by layer

Similar terminal failures can come from different layers. Use the first command that fails to classify the problem.

First failure	What it means	What to inspect
`lev doctor`	Git, elan, Lean, Lake, paths, or workspace state is unavailable or inconsistent.	Fix the local runtime before changing project sources or caches.
`lev lock --check` or `lev sync --frozen`	A project input changed after `lev.lock` was written.	Decide whether the edit was intentional, then regenerate the lock or restore the project file.
`lev build` after Lake starts	The selected environment ran, but Lake or Lean rejected the project.	Read the compiler or Lake diagnostic above lev's summary line.
The cause is still unclear	The initial report does not contain enough evidence.	Run `lev inspect dependencies` and one verbose timed build before deleting `.lake`.

Lock drift

$ lev sync --frozen
error: effective Lake configuration for
leanprover/lean4:v4.19.0 does not match lev.lock

Delegated build failure

$ lev build --no-sync --offline MissingTarget
error: unknown target `MissingTarget`
lev: Lake build failed under leanprover/lean4:v4.18.0 with exit code 1

A focused follow-up

lev inspect
lev inspect dependencies
lev lock --check
lev -v --timings build

What lev adds to the checkout

File	Written by	Commit	Purpose
`lean-toolchain`	Project	Yes	The toolchain selector Lake and elan already understand.
`lakefile.toml` / `lakefile.lean`	Project	Yes	Lake package configuration. Declarative TOML files can be edited transactionally by `lev deps add` and `lev deps remove`.
`lake-manifest.json`	Lake	Yes	The resolved dependency graph. Treat it as generated state, but commit it.
`lev.lock`	lev	Yes	Environment identity and integrity data for reproduction and review.
`lev.toml`	You	When used	Optional workspace members, named tasks, and project automation policy.
`lev-workspace.lock`	lev	In workspaces	An aggregate snapshot over configured workspace members.

None of these replaces a Lake file. If you remove lev.lock, the project falls back to ordinary elan-and-Lake behavior. Recreate it with lev lock when you want the reproducibility layer back.

Related guides

Guide	Covers
Environments and cache	Multiple Lean versions, lock modes, offline work, shared caches, and local workspaces.
Import minimization	Broad imports, compiler-derived replacements, repository policy, and project-wide checks.