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 Mathlib.Linter.ImportState

Equations

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

opaque Mathlib.Linter.minImportsRef : IO.Ref Mathlib.Linter.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.

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

Equations

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