Import policy and coverage

Set policy before applying project-wide edits

After lev shake produces a plausible rewrite, decide how the repository treats public and implied imports. Then check coverage so a clean result cannot hide files that were never analyzed.

Policy	Options	Effect
Preserve the current public surface	`--keep-public --keep-implied`	Keeps deliberate re-exports and implied boundaries unchanged.
Replace broad public imports	`--add-public --keep-implied --keep-prefix`	Keeps replacements public and prefers useful prefix modules.
Measure analyzer coverage	`--coverage`	Reports analyzed modules, files outside the selected roots, and legacy files.
Keep a source-level exception	`-- shake: keep`	Records API or namespace intent that declaration dependencies do not express.

Repository policy recipes

The one-file preview shows compiler-derived import evidence. The repository still has to decide what each module promises downstream. Record that policy before applying the rewrite.

Preserve the current public API

lev inspect imports \
  --keep-public \
  --keep-implied \
  --explain

lev inspect imports \
  --keep-public \
  --keep-implied \
  --fix \
  --isolate

Mathlib-style replacement policy

lev inspect imports \
  --add-public \
  --keep-implied \
  --keep-prefix \
  --explain

lev inspect imports \
  --add-public \
  --keep-implied \
  --keep-prefix \
  --fix \
  --isolate

The first recipe is the conservative one. Every existing public import stays public, even if the current implementation would elaborate with less. That is usually the right starting point for a library with an established downstream surface.

The second recipe follows the approach Mathlib maintainers discussed for broad public imports: allow a public import to be replaced, keep its replacements public, and prefer a useful prefix module over a long list of exact leaves. The policy preserves what a module intends to re-export.

The Mathlib discussion of public import minimization records the tradeoff in detail. Compiler evidence narrows the search; repository policy decides the result.

Policy flag	What it means
`--keep-public`	Preserve public imports as deliberate re-export policy.
`--add-public`	Allow a public import to be replaced, but keep its replacements public.
`--keep-implied`	Preserve imports implied by transitive library boundaries.
`--keep-prefix`	Prefer a broader convenience module over an exact list of leaf imports.

Know what was actually analyzed

A clean check is only as strong as its coverage. --coverage reports which project files Lake's analysis actually saw, so "no drift" cannot silently mean "nothing was inspected."

Coverage report

lev inspect imports --check --coverage
lev inspect imports --check --coverage --json

Coverage summary

$ lev inspect imports --check --coverage
coverage: analyzed 41 module files
coverage: 3 module files outside the selected roots
coverage: 1 legacy file without a leading module command
lev: imports are already minimal

Coverage separates project Lean files into three groups: module files analyzed under the selected roots, module files outside those roots, and legacy files without a leading module command. The JSON envelope (lev.cli.shake/v1) includes each proposed, applied, rejected, or restored file, which makes the report diffable across CI runs.

Compiler evidence is not API intent

A declaration dependency records what the current implementation references. It cannot always explain why an import is present, because elaboration does not encode every API or namespace decision.

Import role	Compiler evidence	Repository response
Declaration used in a proof	Yes, through elaborated dependencies	Safe candidate for inference
Public re-export	Not as downstream API intent	Use `--keep-public` to preserve it, or `--add-public` under a replacement policy
Namespace or scoped notation effect	Not always as a declaration edge	Keep it explicitly when required
Implied or transitive boundary	May look redundant locally	Use `--keep-implied` for libraries that want to preserve that boundary

Explicit project intent

import Mathlib.NumberTheory.NumberField.Basic -- shake: keep

-- The import is part of this module's public surface even when
-- the implementation below has no direct declaration edge to it.

The keep comment documents API intent in the source file when compiler evidence alone cannot explain the import.

Graph and project-wide examples

lev inspect graph renders project and external edges as text, JSON, or Graphviz DOT. The same page includes the FLT case study, where public and implied import policies reduced an aggressive 119-file proposal to a verified 34-file diff, and the CI commands for JSON and SARIF output.