The minImports linter

The minImports linter incrementally computes the minimal imports needed for each file to build. Whenever it detects that a new command requires an increase in the (transitive) imports that it computed so far, it emits a warning mentioning the bigger minimal imports.

Unlike the related #min_imports command, the linter takes into account notation and tactic information. It also works incrementally, accumulating increasing import information. This is better suited, for instance, to split files.

The "minImports" linter

The "minImports" linter tracks information about minimal imports over several commands.

opaque Mathlib.Linter.minImportsRef : IO.Ref Lean.NameSet

minImportsRef keeps track of cumulative imports across multiple commands.

def Mathlib.Linter.«command#reset_min_imports» : Lean.ParserDescr

#reset_min_imports sets to empty the current list of cumulative imports.

Equations

• Mathlib.Linter.«command#reset_min_imports» = Lean.ParserDescr.node `Mathlib.Linter.command#reset_min_imports 1024 (Lean.ParserDescr.symbol "#reset_min_imports")

opaque Mathlib.Linter.linter.minImports : Lean.Option Bool

The minImports linter incrementally computes the minimal imports needed for each file to build. Whenever it detects that a new command requires an increase in the (transitive) imports that it computed so far, it emits a warning mentioning the bigger minimal imports.

Unlike the related #min_imports command, the linter takes into account notation and tactic information. It also works incrementally, providing information that it better suited, for instance, to split files.

def Mathlib.Linter.MinImports.minImportsLinter : Lean.Linter

The minImports linter incrementally computes the minimal imports needed for each file to build. Whenever it detects that a new command requires an increase in the (transitive) imports that it computed so far, it emits a warning mentioning the bigger minimal imports.

Unlike the related #min_imports command, the linter takes into account notation and tactic information. It also works incrementally, providing information that it better suited, for instance, to split files.

Equations

• One or more equations did not get rendered due to their size.