lev documentation

Why lev exists

lev came out of one boring failure that repeated often enough to deserve a tool. The checkout had the right Lean files, but the surrounding state was fuzzy again: maybe the toolchain drifted, maybe Mathlib moved, maybe the build cache came from another run, maybe nobody remembered which exact sequence of commands had actually passed.

lev records and verifies that surrounding state. Lake still owns packages and builds, and Lean still checks the proofs.

The mental model

lev prepares the environment, then Lake and Lean handle the build and proof work.

lev adds the operational layer around a Lean project without claiming ownership of the language.

You or CIlev build

levselect, lock, cache, run

Lakeresolve targets and build

Leanelaborate and kernel-check

What still belongs to Lake and Lean

Package descriptions, manifests, and build targets.
Elaboration, kernel checking, code generation, and Lake's job graph.
The compiler and profiler evidence lev later reads back.

What lev adds around them

Environment locks that say what another checkout should reproduce.
Shared cache and local-workspace coordination that stays reviewable.
Import, profiling, verification, upgrade, bundle, and watch workflows with stable reports.

A clean first pass

After cloning a project that already commits lev.lock and lake-manifest.json, separate project facts from machine state before spending time on a build. Deleting .lake at this point throws away evidence that the inspection commands can use.

A locked project's first session

lev inspect
lev doctor
lev lock --check
lev sync --frozen
lev build
lev verify --offline --test

First-time adoption. If the project has no lev.lock yet, start with lev inspect, lev doctor, and lev build. Create and review the lock separately when the project is ready to adopt it. The --test flag also expects the Lakefile to define a test driver; omit it when the project has none.

lev inspect

Make sure lev found the project you meant

Read the Lakefile, manifest, lock, and selected toolchain before changing the checkout.

lev doctor

Check the machine-facing side

If Git, elan, Lean, Lake, cache paths, or workspace state are off, every later failure gets louder and less informative.

lev lock --check

Reject drift without rewriting anything

This is where an intentional toolchain or dependency edit should show itself. If the lock disagrees, decide whether you meant to change the environment before you sync or build.

lev sync --frozen

Prove the locked environment can still materialize

A frozen sync checks that the checkout still describes one reproducible setup. Follow it with one build or verification pass.

Documentation

Guide	Covers
Environments and cache	Toolchain selection, locks, offline operation, shared caches, local workspaces, and version matrices.
Import minimization	Replacing broad imports with compiler-derived imports, validating rewrites, and preserving public API intent.
Profiling	Phase timings, repeated samples, file ranking, baselines, and Lean's native profiler.
Inspection	Environment diagnosis, dependency revisions, build traces, declaration lookup, and trust analysis.
Automation	Verification gates, dependency upgrades, workspaces, bundles, watch mode, and named tasks.
Command reference	The full command map, common recipes, JSON contracts, and exit behavior.

Where lev stops

If a Lean release breaks source compatibility, lev can keep the old and new environments isolated. It cannot migrate proofs for you.
If Lake cannot build the project, lev cannot repair Lake's target graph. It reports the delegated failure and preserves the child exit code.
Import analysis can discover declaration dependencies, but public re-exports and namespace-only effects still need human policy. The rewrite path therefore stays conservative and rebuild-backed.
A cache hit is an optimization, never the source of truth. Locks, manifests, and successful delegated commands remain the evidence that matters.