Documentation

lev

A uv-inspired project, dependency, cache, and toolchain manager for Lean.

lev is for the point where one Lean checkout turns into several. It keeps each project's normal Lean and Lake files, then coordinates toolchains, locked environments, shared Git data, and compatible build artifacts around them.

Project format: Standard Lake files
Build engine: Lake
Best fit: Several Lean environments

Start here

Five-minute setup

Install lev

Terminal

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

To remove it later, run lev self uninstall --dry-run to preview the exact executable, then lev self uninstall. Cargo installs are handed back to Cargo, and lev keeps your cache and toolchain data.

01

Use an existing project

No conversion step. Run lev beside the Lake files that are already there.

Existing checkout

cd my-lean-project
lev sync
lev build

02

Start a project

Any toolchain selector supported by the configured source can be used. There is no release list compiled into lev.

New checkout

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

There is nothing to activate. lev run prepares the selected environment and starts the command inside it.

Architecture

How it fits

lev coordinates existing tools; it is not another Lean compiler or a private package ecosystem.

One command, with the normal Lean stack underneath

You, CI, or a benchmark runner lev build

lev lock, sync, select, cache, run

elan or lev's store obtain the toolchain

Lake resolve and build

Lean compiler + ordinary project files the same files still work without lev

lean-toolchain, the Lakefile, and lake-manifest.json remain authoritative. lev.lock records extra integrity and environment data; it does not replace Lake's manifest.

Normal work

Daily use

The short commands do the preflight first, then hand control to Lake or the requested process.

What happens before a build starts

1 Select toolchain and lock
2 Sync exact dependencies
3 Attach compatible cache
4 Run Lake or your command

Common commands

lev sync
lev build
lev test
lev run lean --version
lev run lake env my-tool

Use --offline when a run must not touch the network. Use --frozen when configuration, manifest, platform, and toolchain drift should be an error too.

Reproducible run

lev lock --check
lev sync --frozen
lev build --offline

Several environments

Switch toolchains without flattening your workspace

A project can retain more than one resolved environment. Each one gets its own manifest and workspace, so returning to an earlier selection does not ask one build directory to become two incompatible things.

Resolve and revisit environments

lev lock --lean "$PAPER_TOOLCHAIN" --lean "$CURRENT_TOOLCHAIN"
lev build --lean "$PAPER_TOOLCHAIN"
lev build --lean "$CURRENT_TOOLCHAIN"
lev build --lean "$PAPER_TOOLCHAIN"

Switching selects an environment; it does not overwrite the other one

paper toolchain its manifest + workspace

current toolchain its manifest + workspace

lev selects one the other stays intact

active run matching Lean + Lake

shared storage only compatible data is reused

lev use "$TOOLCHAIN" makes a resolved environment the project default. Passing --lean "$TOOLCHAIN" selects one run without changing lean-toolchain.

Reuse

Share the expensive parts, isolate the risky parts

Repositories can share immutable Git objects and Lake artifacts that match exactly. Their source trees, manifests, and active build workspaces remain separate.

Three checkouts using the same lev storage

proof main

review worktree

evaluation repo

Git object store exact locked revisions

Lake artifact cache namespaced by toolchain

What lev guarantees

Different toolchains do not share an artifact namespace.
Frozen and offline modes validate before running.
Cache deletion is a dry run unless --apply is present.

What it cannot promise

The first build is still cold.
Changed source or options can require compilation.
An incompatible project does not become compatible by switching Lean.

Inspect and maintain storage

lev cache status
lev cache verify --full
lev cache gc --max-age-days 7
lev cache gc --max-age-days 7 --apply
lev --local build

Machine learning benchmarking

Keep the full benchmark environment together

This is personal: I was testing an LLM on miniF2F, and the version question kept getting in the way. Different papers used different Lean, Mathlib, project, and REPL snapshots. I would move to another baseline, work out the matching set again, and wait for another checkout to rebuild things I had already built.

lev treats that matched set as the useful unit. Each repository can keep the versions it actually expects, while compatible objects and artifacts are available to the next run.

Compare runs without pretending their source environments are interchangeable

Paper baseline its toolchain its Mathlib + REPL revisions same evaluation protocol

lev run results lock identifies environment

Current model its toolchain its Mathlib + REPL revisions same evaluation protocol

Two frozen project checkouts

cd paper-baseline
lev sync --locked
lev build
lev run python evaluate.py

cd ../current-baseline
lev sync --locked
lev build
lev run python evaluate.py

If one checkout genuinely supports several Lean environments, lock them there and select each run with --lean. If the source differs between papers, keep separate checkouts. lev can reuse matching data across them without mixing their locks.

Formalization workflows

Move between proofs without repeating setup

A main theorem checkout, a review worktree, and an older release branch can all be ordinary Lake projects. lev gives them the same cache policy and lets matching revisions reuse work.

Two worktrees

cd theorem-main
lev build

cd ../theorem-review
lev build
lev audit

The second build may reuse exact dependency objects and compatible outputs. It still elaborates anything whose inputs changed. lev sync --frozen --offline is a useful final check when the environment should already be complete.

Beyond one build

More things lev can do

These use the same lock, toolchain, and cache machinery as lev build. They are separate commands because each solves a different workflow, not because they introduce another project format.

01 / Matrix

Run the same check in isolated Lean environments

The matrix preflights every selector and dependency environment before the first command starts. Each run gets a separate workspace, and the project's lean-toolchain file is left alone.

One-off matrix

lev matrix \
  --lean "$PAPER_TOOLCHAIN" \
  --lean "$CURRENT_TOOLCHAIN" \
  --keep-going \
  -- lake build --wfail

Save the matrix in lev.toml

lev matrix --init \
  --lean "$PAPER_TOOLCHAIN" \
  --lean "$CURRENT_TOOLCHAIN" \
  -- lake build --wfail

lev matrix --keep-going

One source checkout, one command, isolated workspaces

lev matrix validate the complete plan

paper toolchain sync, then run command

current toolchain sync, then run command

02 / Workspace

Operate on every Lake project in a monorepo

Members keep their own lean-toolchain, Lakefile, manifest, and lock. The aggregate workspace lock is published only after every selected member succeeds.

lev.toml

[workspace]
members = ["packages/*"]
exclude = ["packages/experimental"]

Workspace commands

lev workspace list
lev workspace sync --locked
lev workspace build --keep-going
lev workspace lock --check

03 / Scripts

Run one Lean file with its environment attached

A standalone file can declare its toolchain and dependencies in a comment-delimited TOML block. lev caches the generated environment by metadata, so editing the Lean body does not rebuild unchanged dependencies.

Hello.lean

-- /// lev
-- lean = "stable"
-- ///

def main : IO Unit :=
  IO.println "hello from lev"

Run or elaborate

lev script run Hello.lean
lev script check Hello.lean
lev script run --offline Hello.lean

04 / Shared CI cache

Move authenticated Lake artifacts between machines

A directory, file:// location, or HTTPS object host can store immutable compressed blobs and a signed snapshot manifest. Pulls verify the explicit public key, paths, signatures, and hashes before publishing anything locally.

Create a trust key once

lev cache remote keygen \
  --private-key "$LEV_SIGNING_KEY" \
  --public-key ./lev-cache.pub

Push in one job, pull in another

lev cache remote push "$CACHE_REMOTE" \
  --signing-key "$LEV_SIGNING_KEY" \
  --namespace team/project

lev cache remote pull "$CACHE_REMOTE" \
  --public-key ./lev-cache.pub \
  --namespace team/project

Inspect what is actually locked

These are useful in CI or before publishing a reproducibility bundle:

Graph, integrity, and SBOM

lev tree
lev why PACKAGE
lev audit --strict
lev export --format cyclonedx --output project.cdx.json

Pick the smallest tool that solves the problem

elan, Lake, and lev

Need	elan	Lake	lev
Install or select Lean	Yes	No	Store or elan fallback
Resolve and build a package	No	Yes	Delegates to Lake
Share Lake artifacts	No	When configured	Configured automatically
Share dependency Git objects	No	No	Yes
Retain several project environments	Toolchains only	One active manifest	Separate locks and workspaces
Frozen full-environment check	Toolchain	Manifest	Toolchain, platform, manifest, and checkouts

Use elan when you only need a compiler selector. Use Lake when you only need to build one workspace. Add lev when the repeated work is between environments.

Honest boundaries

What happens when upstream breaks?

Lake breaks

Builds break too. lev does not reimplement Lake's build graph, target logic, or compiler integration.

elan is unavailable

Verified toolchains already in lev's store can run directly. Aliases and custom channels that need the elan fallback cannot.

A Lean upgrade breaks source

lev keeps the environments apart; it does not migrate proofs, tactics, Mathlib code, or a version-specific REPL.

Reference

Command map

lev initCreate a standard Lake project.

lev syncMaterialize the selected locked environment.

lev lockRecord or verify one or more environments.

lev buildPrepare the environment, then run Lake build.

lev runRun any command in the selected environment.

lev addEdit a declarative dependency transactionally.

lev toolchainInstall, inspect, or remove toolchains.

lev cacheInspect, verify, or clean shared state.

lev doctorCheck Lean, Lake, Git, and cache setup.

lev auditCheck lock and checkout integrity.

lev matrixRun one command across isolated toolchains.

lev workspaceOperate on a configured set of Lake projects.

lev scriptRun one Lean file in a cached inline environment.

lev exportWrite a dependency inventory or CycloneDX SBOM.

Run lev -h for the everyday surface and lev --help for every command.

Agentic coding

Using lev with your coding agent :)

Want Codex, Claude Code, or another coding agent to use lev too? It is easy :) Point it at the .agents folder in the repository. That folder includes an Agent Skill for lev. It explains the normal sync, lock, build, offline, toolchain, and cache workflow so the agent does not have to guess from whatever happens to be installed globally.

Tell your agent

Read .agents/skills/lev/SKILL.md, then use lev for this project.

That is usually all you need to say. Agents that support Agent Skills can discover it directly, and other agents can read the Markdown file as ordinary project instructions. It is an easy way to keep automated edits on the same reproducible path as a human contributor.