Environments and cache

Environment identity

An environment includes more than the Lean version. lev combines the selected toolchain, platform, project configuration, Lake manifest, and exact dependency revisions. Two projects may use the same compiler while resolving different dependency trees; those are different environments even if some cached objects can be shared.

lev.lock complements lake-manifest.json; it does not replace it. Lake's manifest describes resolved package dependencies. lev's lock records the broader environment and integrity information needed to reproduce and audit that resolution.

The responsibilities stay separate. Lake resolves and builds the project; lev records enough of the surrounding environment to reproduce that build next week, on another machine, or in a benchmark checkout.

lev doctor
lev doctor --json -o environment.json

# Same report under the inspection family
lev inspect environment

lev doctor checks the selected Lean and Lake runtime, Git and optional elan installation, project files, cache locations, artifact state, and workspace configuration. It does not synchronize dependencies or create missing project state.

The miniF2F problem

I ran into this while testing an LLM on miniF2F. A result in a paper was tied to more than a theorem set: it depended on a particular Lean release, Mathlib revision, project snapshot, and REPL. Moving between baselines meant reconstructing that combination again, then waiting while another checkout rebuilt dependencies I already had.

That experience shaped lev's environment model. A benchmark checkout keeps the versions it expects, and its lock identifies the exact combination. Another checkout can reuse Git objects or build artifacts when their keys match, but it does not inherit the first checkout's manifest or toolchain by accident.

cd paper-baseline
lev sync --frozen
lev run python evaluate.py

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

If the papers use different source snapshots, keep separate checkouts. If one checkout supports several Lean releases, record those environments together and select a run with --lean. In either case, the result stays attached to an environment you can name and inspect.

Select and retain toolchains

lev toolchain list
lev toolchain install leanprover/lean4:v4.19.0
lev project pin leanprover/lean4:v4.19.0

# Run without changing the project's default
lev build --lean leanprover/lean4:v4.18.0

# Make a resolved alternate environment the default
lev project use leanprover/lean4:v4.19.0

An explicit --lean selection creates or reuses a separate environment. It does not flatten the current checkout into whichever version happened to run last. This is useful while testing a release candidate or keeping a paper's original environment available beside current development.

Lock modes

“Locked,” “frozen,” and “offline” constrain different things. --locked requires an existing manifest; --frozen verifies lev.lock, the manifest, and project configuration without refreshing the lock; --offline forbids network access. A valid lock can still name an object that is absent locally, so frozen and offline answer separate questions.

Recovering from lock drift

When lev sync --frozen reports lock drift, the message names what disagrees: the toolchain selector, the Lakefile, or the manifest. What you do next depends on whether that change was deliberate.

• The change was intentional. You edited the Lakefile, pinned a new toolchain, or updated a dependency. Run lev lock to record the new environment, review the lev.lock diff, and commit it with the change that caused it.
• The change was not intentional. Restore the drifted file from version control and re-run lev sync. Do not regenerate the lock to silence a drift you cannot explain; the drift is the finding.

lev lock --check answers the drift question without materializing anything, which makes it the cheapest first gate in CI.

How cache reuse works

lev shares expensive work without turning every checkout into the same mutable directory. Git data, toolchains, dependency environments, and build artifacts use separate stores because they have different identity and cleanup rules.

Git objects

Content-addressed dependency history

Toolchains

Persistent verified compiler objects

Lake artifacts

Toolchain-specific, compatibility-keyed builds

Lake decides whether a build artifact matches the trace keys for the current target. lev makes that reuse practical across projects and toolchain variants without collapsing them into one mutable workspace.

A cache hit may skip work, but it does not weaken the lock. Cache misses fall back to the normal Lake build path.

The cache decision, step by step

1. lev selects the exact project environment and toolchain.
2. It assigns Lake a toolchain-specific LAKE_CACHE_DIR and enables Lake's artifact-cache protocol with LAKE_ARTIFACT_CACHE.
3. Lake computes trace keys from the build inputs it owns. A matching mapping can attach an existing artifact; a missing mapping schedules ordinary compilation.
4. lev coordinates shared locks, checks that mapped local outputs exist, and records cache state for inspection and garbage collection.
5. The project lock remains the source of environment identity. Reused build output is only an optimization beneath that boundary.

The local artifact cache is not a signed package registry. Its safety comes from Lake's trace identity, toolchain separation, file structure, and local verification commands. Remote snapshots add a different property: an Ed25519 signature authenticates the producer before lev installs the snapshot.

Where lev stores state

lev separates fast, reconstructible state from persistent verified objects. Both locations are plain directories that can be inspected, relocated, or deleted.

lev cache dir prints the resolved cache location. Bare lev inspect reports both stores alongside the discovered project, selected runtime and toolchain, lock state, and available build metadata. Use --data-dir or LEV_DATA_DIR when you need to make the persistent toolchain store explicit. Deleting either store never changes project files; the lock still describes what to rebuild.

Inspect and maintain cache state

lev cache dir
lev cache status
lev cache verify
lev cache artifacts status
lev cache artifacts verify

# Garbage collection only reports candidates until --apply is present
lev cache gc --max-age-days 30
lev cache gc --max-age-days 30 --apply

# Show orchestration and reuse decisions during a build
lev -v build

lev: already synchronized 0 Git dependencies: 0 created, 0 reused, 0 updated; 0 mirrors created, 0 fetched
Build completed successfully.

A dependency-free project reports zeros. A project with Git dependencies prints how many checkouts were created, reused, updated, mirrored, and fetched before Lake prints its own build result.

Move artifacts between machines

Remote snapshots let one verified build seed another machine without passing around an unsigned archive. Generate a signing key once, keep the private half on the producer, and distribute the public half to consumers through a trusted channel.

lev cache remote keygen \
  --private-key ~/.config/lev/cache-signing.key \
  --public-key cache-signing.pub

# Producer: sign and upload the current locked snapshot
lev cache remote push https://cache.example.org/lean-artifacts \
  --namespace acme/algebra \
  --signing-key ~/.config/lev/cache-signing.key

# Consumer: authenticate, verify, and install that snapshot
lev cache remote pull https://cache.example.org/lean-artifacts \
  --namespace acme/algebra \
  --public-key cache-signing.pub

The snapshot revision defaults to the current project lock digest. The toolchain and native platform default to the active environment, so a pull cannot silently install an artifact set under an unrelated key. Use --revision, --toolchain, or --platform only when selecting a known snapshot deliberately.

lev project publish v1.2.0 --dry-run
lev project publish v1.2.0

Test several Lean versions

lev matrix \
  --lean leanprover/lean4:v4.18.0 \
  --lean leanprover/lean4:v4.19.0 \
  -- lake build

Before each run, lev prints lev: matrix environment TOOLCHAIN, selects that environment, and streams the delegated command's output unchanged. Without --keep-going, the first failed environment stops the matrix. With it, later environments still run and the command returns the first nonzero status.

lev matrix checks the same command against several toolchains while keeping selection, cache behavior, and exit handling explicit. It does not add a timing summary; lev inspect performance covers experiments where elapsed time matters. Shared objects are reused only when their keys permit it, so testing a candidate compiler does not silently rewrite the default project's dependency state.