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.

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 is better suited, for instance, to split files.

Another important difference is that the minImports linter starts counting imports from where the option is set to true downwards, whereas the #min_imports command looks at the imports needed from the command upwards.

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

The linter.minImports.increases regulates whether the minImports linter reports the change in number of imports, when it reports import changes. Setting this option to false helps with test stability.

def Mathlib.Linter.MinImports.«command#import_bumps» : Lean.ParserDescr

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 is better suited, for instance, to split files.

Another important difference is that the minImports linter starts counting imports from where the option is set to true downwards, whereas the #min_imports command looks at the imports needed from the command upwards.

Equations

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