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.

structure Mathlib.Linter.ImportState : Type

ImportState is the structure keeping track of the data that the minImports linter uses.

• transClosure is the import graph of the current file.
• minImports is the NameSet of minimal imports to build the file up to the current command.
• importSize is the number of transitive imports to build the file up to the current command.

• transClosure : Option (Lean.NameMap Lean.NameSet)

  The transitive closure of the import graph of the current file. The value is none only at initialization time, as the linter immediately sets it to its value for the current file.

• minImports : Lean.NameSet

  The minimal imports needed to build the file up to the current command.

• importSize : Nat

  The number of transitive imports needed to build the file up to the current command.

instance Mathlib.Linter.instInhabitedImportState : Inhabited ImportState

Equations

• Mathlib.Linter.instInhabitedImportState = { default := { transClosure := default, minImports := default, importSize := default } }

opaque Mathlib.Linter.minImportsRef : IO.Ref ImportState

minImportsRef keeps track of cumulative imports across multiple commands, using ImportState.

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.importsBelow (tc : Lean.NameMap Lean.NameSet) (ms : Lean.NameSet) : Lean.NameSet

importsBelow tc ms takes as input a NameMap NameSet tc, representing the transitiveClosure of the imports of the current module, and a NameSet of module names ms. It returns the modules that are transitively imported by ms, using the data in tc.

Equations

• Mathlib.Linter.MinImports.importsBelow tc ms = Lean.RBTree.fold (fun (x1 : Lean.NameSet) (x2 : Lean.Name) => x1.append (Lean.RBMap.findD tc x2 default)) ms ms

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")

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 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

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