lev docs

Core guide

Import minimization

Yes: if a file says import Mathlib, lev can often infer a narrower import set from the exact pinned revision. It keeps compiler evidence separate from library policy and accepts only edits that survive a rebuild.

Import inference

lev shake can infer a smaller import set from compiler-derived dependency evidence in the exact Mathlib revision pinned by the project. You do not need to guess module paths by hand.

Source text alone misses declarations introduced through re-exports, notation, generated imports, or a long module chain. lev reads what Lean and Lake recorded for the elaborated file.

Preview one file
lev shake MyProject.Proof --explain
Preview output
remove #[import Mathlib]
add #[import Mathlib.Data.Nat.Prime.Basic]

The exact replacement depends on the pinned Mathlib revision. lev reports the edit before it writes anything.

TaskCommand
Preview one module with explanationslev shake MyProject.Proof --explain
Check the project and report analyzer coveragelev shake --check --coverage
Preserve existing public and implied importslev shake --check --keep-public --keep-implied
Apply verified edits and isolate failureslev shake --fix --isolate --keep-public --keep-implied

What lev adds beyond plain Lake

lev shake adds repository policy, rollback, whole-project reporting, and rebuild-backed edits to Lake's dependency evidence.

The manual or plain-Lake path

  • Read broad imports by eye and guess smaller modules.
  • Or run analysis and then hand-apply edits across files.
  • Rebuild afterward and hope the batch did not leave the repo in a half-broken state.

The lev path

  • Ask the selected pinned environment for compiler-derived evidence.
  • Apply repository policy such as public-import preservation separately from the evidence itself.
  • Keep an edit only after the requested rebuild succeeds; otherwise restore the original file, or keep only isolated successes.

This is also why lev keeps both visible spellings: lev shake for the everyday workflow and lev inspect imports for the grouped inspection family. The hidden compatibility spelling lev imports remains available for older scripts, but the direct and grouped visible commands are the ones the docs center.

How lev shake works

The apply path is transactional. lev snapshots the source, validates the rewrite, and restores the original when validation fails.

Compiler evidence comes first. Source edits come later, behind validation.
01
discover targets

Resolve explicit modules or the package defaults

You can target one file, a set of files, or the default project surface. Coverage mode later reports what was actually analyzed.

02
read dependency evidence

Ask the selected toolchain what the elaborated file used

The result is revision-sensitive because lev reads the pinned build environment rather than a generic Mathlib catalog.

03
apply policy

Preserve public intent where the compiler cannot see it

--keep-public, --keep-implied, explicit keep annotations, and Mathlib-style replacement flags decide what should remain visible even when the shortest import list is smaller.

04
rebuild and keep or restore

Never treat a proposed import edit as accepted until it builds

With --fix, lev snapshots the original file, applies the rewrite, rebuilds, and restores the source on failure. --isolate can keep independently verified edits from a larger batch.

Compiler evidence and repository policy

The shortest import set is not automatically the right one. A library may need a broader public API than the compiler can infer from one theorem body.

Compiler-derived facts

  • Which declarations the elaborated file reached.
  • Which import set is sufficient for the checked source under this pinned revision.
  • Which rewrite passes or fails the validation build.

Repository policy

  • Whether current public imports should be preserved.
  • Whether implied imports should remain for readability or namespace reasons.
  • Whether a project follows a conservative keep policy or a Mathlib-style replacement policy.
Before
import Mathlib

example (n : Nat) : n ∣ n := by
  exact dvd_refl n
Possible result
import Mathlib.Algebra.Divisibility.Basic

example (n : Nat) : n ∣ n := by
  exact dvd_refl n

The result depends on the pinned Mathlib revision. Public-library policy can still choose to keep a broader import than the compiler minimum.

Import documentation

PageContents
Import workflowsPreview, check, apply, rollback, isolation, JSON, and SARIF.
Import policy and coveragePublic imports, implied imports, keep annotations, and analyzer coverage.
Import graphs and case studyGraphviz output, review artifacts, and the complete FLT project run.
Command referenceOptions, command families, JSON contracts, and common recipes.