Import workflows

Test one file first

Preview what lev would do to one file before applying a project-wide edit. The examples use the direct lev shake spelling, but lev inspect imports accepts the same options and produces the same lev.cli.shake/v1 report.

Preview, check, and apply

lev shake MyProject.Proof --explain
lev shake MyProject.Proof --check
lev shake MyProject.Proof --fix

# The grouped form accepts the same options
lev inspect imports MyProject.Proof --explain

MyProject/Proof.lean:
  remove #[import Mathlib]
  add #[import Mathlib.Data.Nat.Prime.Basic]

The module names come from the project's pinned Lake and dependencies.

Previews and --check both leave source unchanged and return status 1 when drift is found. --check also labels JSON output as check mode for CI. --fix applies and validates; --apply is an equivalent spelling. --isolate turns a failing batch into smaller verification units so accepted edits do not have to be discarded with an unrelated rejected file.

The transaction boundary is the main safety property. A failed verification restores the Lean source files selected for rewriting instead of leaving a partial import edit in the branch.

$ lev inspect imports --fix
Successfully applied 1 suggestions.
lev: verifying rewritten imports
Build completed successfully.

$ lev inspect imports --fix
lev: imports are already minimal

$ lev inspect imports --fix
lev: verifying rewritten imports
error: unknown constant 'Nat.prime_five'
lev: import verification failed; restoring the original Lean sources
$ echo $?
1

Running the command again should produce no new edits. That fixed point is a useful check that the accepted source and the analyzer agree. On failure, lev restores the original bytes before returning, so the working tree is not left halfway through an import rewrite.

When one file rejects the batch

Suppose A.lean can use the smaller imports but B.lean relies on a namespace effect that does not appear as a declaration edge. With --isolate, lev verifies the restored baseline, tests smaller subsets, keeps A.lean, and restores B.lean.

$ lev inspect imports --fix --isolate --json > shake.json
lev: batch verification failed; isolating import edits
lev: verifying the restored baseline
lev: rejected the import rewrite for B.lean
lev: keep the dependency with `import Mathlib -- shake: keep`
$ echo $?
1

{
  "schema": "lev.cli.shake/v1",
  "data": {
    "mode": "isolate",
    "status": "partially_applied",
    "files": [
      {
        "path": "A.lean",
        "disposition": "applied",
        "removed_imports": [],
        "added_imports": []
      },
      {
        "path": "B.lean",
        "disposition": "rejected",
        "removed_imports": [],
        "added_imports": [],
        "keep_annotations": [
          "import Mathlib -- shake: keep"
        ]
      }
    ]
  }
}

Status 1 is intentional here: useful edits were kept, but the requested whole-project minimization did not fully succeed. Review the retained diff, add the suggested keep annotation when it matches project intent, and run the command again. The report names the file that still needs a policy decision.

A rewrite can compile and still expose the wrong public API. The next page covers the separate policy for public imports, implied imports, and prefix preservation.

Requirements and failure behavior

• The selected Lake toolchain must provide its native shake command; older toolchains without it cannot run the analysis.
• Analyzed files must use the Lean module system (a leading module command). Legacy files are reported, not silently skipped.
• Stale .olean files are rebuilt automatically before analysis unless --no-build disables that retry. --force instead asks Lake to analyze stale .olean files without its freshness check.
• Validation builds bypass Lake's artifact cache and end with a freshness check, so a cache hit cannot mask a missing .olean.
• If the whole-batch rewrite fails under --isolate, lev restores and verifies the baseline first. A broken baseline leaves every file unchanged; a partial result exits with status 1 and reports candidate -- shake: keep annotations for the failing files.

Policy, coverage, and project-wide analysis

Once a one-file rewrite succeeds, set the repository policy, check analyzer coverage, and inspect the project-wide graph.