lev

The same setup, over and over

A normal week can leave me with one Mathlib checkout for current work, another pinned to a paper or experiment, and a third that I made just to test a change. They are all ordinary Lake projects, and they may intentionally use different Lean and dependency versions.

There is nothing unusual about building two of them:

git clone https://github.com/leanprover-community/mathlib4.git mathlib-main
git clone https://github.com/leanprover-community/mathlib4.git mathlib-review

cd mathlib-main
lake build

cd ../mathlib-review
lake build

This works. elan finds the requested compiler and Lake builds the project. The annoying part appears when I come back to the first checkout a week later, or clone the same revision elsewhere. I may download another package tree, rebuild files that already exist on the machine, or discover that a helper script assumed whichever Lean happened to be active.

I also do not want the checkouts quietly converging. The paper snapshot should keep its old compiler and package graph; current work should be free to move on. I wanted both environments to remain ordinary Lean projects, but I wanted returning to either one to be uneventful.

After going through Lean Zulip conversations, this felt less like a personal quirk and more like a recurring theme. Threads about elan, lake update, lake exe cache get, toolchain pinning, and package management often circle the same question: how do I get back into the exact Lean environment I meant to use, quickly, without accidentally changing the project?

elan, Lake, and lev solve different problems

Before writing lev, I already used elan and Lake every day. They were not the problem, and replacing either one would have made lev harder to trust. The missing part for me was a small layer that remembered the whole environment around them.

elan chooses the Lean distribution

elan manages toolchains. It reads lean-toolchain, installs distributions, selects one for the current directory, and provides the lean and lake shims. If I only need the Lean release requested by a repository, elan is enough.

On a fresh machine, lake build can send me through elan's proxy, install the release named by the nearest lean-toolchain, and run the Lake bundled with it. That behavior is useful, so lev keeps it. Aliases, channels, overrides, and the +toolchain selector remain elan's job.

Lake understands the project

Lake is the package manager and build system. The Lakefile describes packages, libraries, executables, facets, and dependencies. Lake resolves dependencies into lake-manifest.json, creates package workspaces, and defines the build.

If I edit one Mathlib module, Lake knows which downstream targets need rebuilding. If I move a dependency revision, Lake knows which traces are stale. I did not want lev guessing about any of that, so it eventually hands the real build back to Lake.

lev coordinates the environment around both

lev reads those same files, checks the lock, prepares an isolated dependency workspace, connects compatible caches, and then calls Lake. Official toolchains can live in lev's verified store; selectors outside that path can still fall back to elan.

The distinction I use is: elan gets me the distribution, Lake understands the project, and lev remembers how I entered the complete environment. On one small checkout that may only save a little setup. It becomes much more useful when I have several checkouts, an old toolchain I need again, or a cluster job that should not rebuild on shared storage.

This dependency on elan and Lake is deliberate. If Lake changes how a target should build, lev should follow Lake rather than inventing a competing answer.

The part I borrowed from uv

The idea clicked while I was moving between Python and Lean work. With uv, I did not think about activating an environment or where a wheel had already been downloaded. I ran uv sync, then uv run, and the project opened in the state described by its files.

I wanted the Lean side of the same terminal session to feel that simple: lev sync, lev run, and no hunt through old shell history. The implementation is different because Lean projects are different.

uv owns a Python dependency solver, Python distributions, virtual environments, and a pip-compatible interface. lev does not need Lean versions of all those pieces. Lake and Reservoir still resolve Lean packages, and Git repositories remain the usual source.

lev.lock therefore sits beside the Lake manifest rather than replacing it. Lake records the dependency graph; lev adds the toolchain, platform, integrity, and alternate-environment information I need when I come back later. I borrowed the workflow from uv, not Python's package model.

A concrete Mathlib walkthrough

I use Mathlib here because most Lean users already know what its repository looks like. There is no lev template hidden in the example and no conversion step; this is the normal project.

git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4

lev sync
lev build
lev run lean --version
lev audit

On a new checkout I usually run lev sync first. I like seeing toolchain and dependency setup finish before a long compilation starts. After that I normally use lev build, which performs the same checks on its way to Lake.

1. 01
   Read the project as it is.

   lev reads lean-toolchain, the Lakefile, and lake-manifest.json. It does not translate them into a private project format.

2. 02
   Select the exact toolchain.

   An official release can come from lev's verified store. Other selectors use elan's existing resolution path.

3. 03
   Check the lock against the project.

   The project path, platform, toolchain, manifest content, and dependency revisions have to agree with the selected environment.

4. 04
   Materialize dependencies.

   Exact Git revisions can come from shared mirrors, but every project receives an ordinary isolated package workspace that Lake can use normally.

5. 05
   Attach compatible artifacts.

   When the selected Lake supports its native artifact cache, lev points it at a toolchain-specific namespace. Lake still decides whether an artifact key is valid.

6. 06
   Run the real build.

   lev invokes Lake and preserves its output and exit status. lev build does not hide another compiler.

Adding a dependency is still a Lake operation

lev can make a declarative dependency edit as a transaction, then ask Lake to resolve it. It has no package-name special case or hardcoded Mathlib release:

lev add PACKAGE --scope OWNER
lev add PACKAGE --git https://github.com/owner/repository --rev "$REVISION"
lev add sibling --path ../sibling

Without an explicit revision, Lake and Reservoir choose a compatible package version and write the exact result to lake-manifest.json. With --rev, I choose the Git revision. If resolution fails, lev restores the Lakefile, manifest, and lev lock together.

What the second checkout reuses

This is where lev first felt useful to me. I cloned Mathlib again for a review and wanted an independent working tree, but I did not want the machine to forget that it had already seen the same compiler and many of the same dependency commits.

git clone https://github.com/leanprover-community/mathlib4.git mathlib-review
cd mathlib-review
lev build

lev reuses three kinds of data:

• Toolchain reuse: the same verified Lean distribution is installed once in the content-addressed store.
• Dependency reuse: the same locked Git commit can be fetched from a common mirror while each checkout gets a normal package tree.
• Artifact reuse: Lake may restore compiled outputs when its artifact key matches, inside the namespace for the selected toolchain.

A changed source file, build option, dependency revision, platform, or toolchain can invalidate an artifact. Lake still decides whether the artifact matches.

The disk-space problem is real too

Speed was only half of it. After enough experiments, I would look at a laptop or cluster directory and find several large .lake trees attached to repositories whose source code was comparatively small. Toolchains, package workspaces, .olean files, native objects, traces, and executables add up quickly.

My usual mix is a current Mathlib checkout, a review worktree, a frozen benchmark, and something temporary. I need those source trees to remain separate. I do not need each one to store another copy of every immutable object it shares with the others.

Pointing every checkout at the same mutable .lake/packages and .lake/build directories is unsafe. One lake update, branch switch, or compiler change could alter another project's state. lev shares immutable Git objects and compatible Lake artifacts, but keeps active source, package, and build workspaces separate.

lev is not a disk compressor. A different compiler needs its own toolchain, and another dependency graph may need another workspace. A cold build creates real outputs. Exact Git objects and valid Lake artifacts can be stored once, and old lev-managed state has one cleanup interface.

lev cache status
lev cache verify --full

# Preview entries older than two weeks.
lev cache gc --max-age-days 14

# Apply only after reading the plan.
lev cache gc --max-age-days 14 --apply

I made garbage collection a dry run by default because a cleanup command should be boring. It reports Git mirrors, local workspaces, toolchain-specific Lake caches, file counts, and total bytes before deleting anything. I can keep an old environment I still use and remove one from a dead experiment.

Shared filesystems and cluster scratch

I noticed this more clearly on a cluster. My repository lived on EFS so every node could see it, which was convenient for source and checkpoints. It was much less pleasant for a Lean build creating and statting thousands of small files. I ended up copying projects to scratch by hand, building there, and trying to remember which directories were safe to reuse.

The same issue applies to NFS and other shared filesystems: source belongs there, but a busy .lake tree can spend a surprising amount of time on remote metadata.

lev --local build mirrors tracked source into a persistent workspace under LEV_CACHE_DIR, keyed by the project, toolchain, and locked environment. Package and build writes stay in that local copy. The next run reuses unchanged source files from the same cache.

For a scheduler job, the command can be as small as this:

LOCAL_SCRATCH="${SLURM_TMPDIR:-/scratch/$USER/${SLURM_JOB_ID:-manual}}"
mkdir -p "$LOCAL_SCRATCH"

LEV_CACHE_DIR="$LOCAL_SCRATCH/lev-cache" \
  lev --local --verbose build

On Slurm, SLURM_TMPDIR may already point at the job's local disk. Other schedulers expose different scratch paths. LEV_CACHE_DIR only needs to sit outside the shared source checkout on storage suited to many temporary writes.

LEV_DATA_DIR is separate and holds content-addressed toolchain objects. A cluster can keep those objects in shared persistent storage while putting workspaces and Lake caches on node scratch. Putting both on local disk gives one job faster I/O, but ephemeral scratch has to be populated again.

Local mode also refuses project layouts it cannot reproduce safely, such as external path dependencies that sit outside the mirrored source tree. I prefer that refusal over a cluster build that silently uses a different sibling directory from the login node.

Changing toolchains without flattening the last environment

I originally wanted this for old experiments. A benchmark might need the Lean and Mathlib versions from a paper, while the project I am actively editing has already moved forward. Installing both compilers is easy enough; keeping both complete environments ready to revisit is the part I kept handling with scripts.

lev has no hardcoded version list. A selector can be an official release, an RC, a nightly, a channel, or another complete identifier supported by its source.

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

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

The third command reopens the first environment instead of flattening it into the second one. Artifacts are not shared blindly across Lean versions; each environment keeps its own cache namespace. Different Lean versions can still require real proof edits. lev only preserves the old environment while I try another one.

What lev matrix is for

lev build --lean ... selects one environment. lev matrix preflights several environments, creates isolated workspaces, and runs the same command in each one.

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

Each matrix lane receives its own lock, workspace, and toolchain-specific cache namespace. The command reports what builds; it does not rewrite a proof, dependency, or Lakefile to make an incompatible version pass.

ML benchmarking across Lean environments

This was the use case that pushed me to build Lev. With more people testing LLMs and theorem-proving systems across Lean benchmarks, the package environment becomes part of the experiment. While testing models on datasets such as miniF2F, I kept encountering code from different papers that expected different Lean releases, Mathlib snapshots, and REPL protocols. I could run the same model and dataset twice but still change the result by changing what parsed or elaborated underneath them.

The model checkpoint is not enough to reproduce a run. I also need the Lean toolchain, project revision, manifest, server or REPL revision, and runner configuration. lev does not manage model weights or datasets; it records and enters the Lean side.

For example, I can keep one Mathlib-based benchmark project at the revision used for a model run and another on current development:

cd benchmarks/mathlib-paper
lev sync --frozen
lev run python evaluate.py

cd ../mathlib-current
lev sync --frozen
lev run python evaluate.py

The surrounding ML environment still provides Python. lev run gives the runner the selected Lean and Lake environment. Two projects can reuse an exact dependency revision or compatible artifact; otherwise their caches stay separate.

An evaluation server or CI farm can prepare each supported project branch once, keep the lev data directory between jobs, and run each request inside its lock. A failed build then identifies a source-and-environment pair, not a worker with the wrong global Lean installation.

Where the speed comes from

I do not want to pretend lev makes Lean itself compile faster. A cold build still has to compile everything missing from a compatible cache. The win comes when I open another checkout or return to an environment and the work is not actually new.

I timed one small Lean REPL case because I wanted to know whether lev added noticeable overhead. One checkout had already populated the artifact cache; the measured checkout was otherwise fresh:

Measured July 19, 2026 on a 96-vCPU Linux host. Clone time and toolchain installation were excluded. The source and toolchain were identical, and the two warm rows reused outputs from an earlier build. This is one cache-reuse check, not a universal performance claim.

Manual Lake took 0.25 seconds and lev took 0.26 seconds. Lake is the artifact-cache engine. lev gives it a consistent cache path and toolchain namespace, then ties that cache to locks, shared Git data, offline execution, verification, and cleanup.

A few other commands and where I use them

The commands below came from smaller annoyances I met after the main build workflow was working. They all use the same lock, workspace, toolchain, and cache model as lev build.

lev still does not own every tool involved. Python manages the Python environment. Package-specific caches stay with their packages. Lake targets stay Lake targets.

Here are some current weaknesses :)

lev 1.0.0 has rough edges. These are the ones I would keep in mind:

• Lake is still required for Lake-backed builds. lev coordinates the environment but does not have a second implementation of the project build graph.
• Lean migrations still require source changes. Separate environments make comparison cleaner, but lev cannot repair tactics, proofs, imports, or APIs after an incompatible upgrade.
• Offline mode needs a prepared cache. If a required toolchain, dependency revision, or artifact is absent, the command stops instead of quietly contacting the network.
• Cold builds are still cold. lev can find valid previous work, but new source, options, dependencies, platforms, or toolchains can require real compilation.
• The test suite cannot cover every machine. It runs on Linux, macOS, and Windows, but I expect new filesystem, shell, proxy, and toolchain cases as more people use it.
• One project may not need lev. If elan and Lake already make the workflow painless, keep using them. lev is for repeated work across projects, versions, worktrees, CI jobs, or machines.

If one of these limits affects your workflow, open an issue or send a fix. I would rather see a concrete example than pretend the first release covers every Lean setup.

Trying lev

Try it first on an existing Lake project:

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

lev doctor
cd my-lean-project
lev sync
lev build

There is nothing to activate. lev run executes a command inside the selected environment, and I can still use ordinary Lake whenever that is enough. lev has saved me time while moving among Lean projects, worktrees, toolchains, and benchmark environments.