Imports in practice

Inspect the module graph

lev inspect graph reads project source imports without crawling generated build trees. Roots can be module names or Lean file paths and can be repeated. When an import looks surprising, this is usually the fastest way to see whether the surprise is local or structural.

Graph reports

lev inspect graph MyProject.Main
lev inspect graph MyProject.Main MyProject.Tests --external
lev inspect graph MyProject.Main --format json -o imports.json
lev inspect graph MyProject.Main --external --format dot -o imports.dot
dot -Tsvg imports.dot -o imports.svg

Graph output

3 modules, 3 edges, 0 cycles
MyProject.Main  MyProject/Main.lean  direct=2 external=0 transitive=2
  -> MyProject.Algebra
  -> MyProject.Util
MyProject.Algebra  MyProject/Algebra.lean  direct=0 external=1 transitive=0
  -> Mathlib.Algebra.Group.Basic
MyProject.Util  MyProject/Util.lean  direct=0 external=0 transitive=0

--external includes modules outside the project and renders them as dashed boxes in DOT. The Graphviz dot command is separate software. lev inspect graph exits unsuccessfully if it detects a cycle.

Example import graph: solid nodes are project modules; the external Mathlib module sits outside the project boundary.

MyProject.Mainroot module

MyProject.Algebraproject import

Mathlib.Algebra...external import

MyProject.Utilsecond direct import

Case study: the FLT project

A toy file can show the mechanism, but I wanted to know what happened when a real library pushed back. The trial project was Imperial College London's FLT formalization at commit 0996e0c. That checkout contained 269 Lean files; the default FLT target exposed 259 module-system files to Lake's analysis.

Baseline: 8,920 jobs / 196.79 s
First preview: 119 files proposed
Verified result: 34 files / +9 -54

The aggressive pass exposed the files where library policy still mattered. The final counts belong to this checkout; they are not a general shrinkage claim.

Repeat this workflow on another substantial library

lev sync --frozen
lev shake --check
lev shake --check --keep-public
lev shake --check --keep-public --keep-implied
lev shake --fix --keep-public --keep-implied --isolate
lev shake --check --keep-public --keep-implied

Establish the baseline

A complete 8,920-job Lake build passed. That exact target, rather than a small demonstration module, became the validation boundary.

Let the aggressive pass fail

The first preview proposed 119 files. Applying all suggestions broke 10 modules, so lev restored every source from its transaction snapshot.

Preserve library intent

--keep-public reduced the proposal to 76 files but left one failure. Adding --keep-implied reduced it to 34, exposing the difference between implementation dependencies and re-export policy.

Annotate two exceptions

Two namespace-only imports received -- shake: keep. lev rewrote 33 other files, the complete target passed in 228.04 seconds, and a repeated minimization run found no remaining changes.

FLT proposals after progressively conservative policyFile counts from that FLT checkout.

Aggressive

119

Keep public

Public + implied

Each bar counts source files lev proposed to modify under that policy.

The case study changed lev. It exposed a false-positive verification path where Lake's artifact cache could report success without producing a changed .olean. Import validation now bypasses that cache and checks freshness before accepting edits.

End state

$ lev shake --check --keep-public --keep-implied
lev: imports are already minimal

$ git diff --stat
34 files changed, 9 insertions(+), 54 deletions(-)

The timing describes this checkout. The accepted result was a smaller import surface that rebuilt cleanly, restored all files after failed batches, and produced no further changes on the final check.

Put import policy in CI

Once import drift becomes project policy, the result needs to survive code review. JSON is good for scripts and diffs. SARIF is good for annotation UIs. lev check --imports is the blunt whole-project gate when import drift is only one phase in a longer verification run.

Machine-readable checks

lev shake --check --json > shake.json
lev shake --check --sarif lev-shake.sarif
lev check --offline --imports

Need	Command	Why it fits
Post-process drift in a script	`lev shake --check --json`	The envelope is versioned and diffable, so scripts can branch on the schema and inspect the file list directly.
Annotate pull requests	`lev shake --check --sarif`	SARIF gives review systems a standard path for surfacing file-level findings without scraping terminal text.
Fold imports into the full project gate	`lev check --offline --imports`	The import phase runs only after configuration, lock, dependency, audit, toolchain, and build checks have already passed.

GitHub Actions upload

- run: lev shake --check --sarif lev-shake.sarif
- if: always()
  uses: github/codeql-action/upload-sarif@v3
  with:
    sarif_file: lev-shake.sarif

lev check --imports stops at the first broken prerequisite. If the project does not build, report that failure before proposing imports for a file that never elaborated.