[Merged by Bors] - feat: add by how many modules imports grew

Mathlib/Tactic/Linter/MinImports.lean

@@ -28,8 +28,26 @@ The "minImports" linter tracks information about minimal imports over several co
 
 namespace Mathlib.Linter
 
-/-- `minImportsRef` keeps track of cumulative imports across multiple commands. -/
-initialize minImportsRef : IO.Ref NameSet ← IO.mkRef {}
+/--
+`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.
+-/
+structure ImportState where
+  /-- 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. -/
+  transClosure : Option (NameMap NameSet) := none
+  /-- The minimal imports needed to build the file up to the current command. -/
+  minImports   : NameSet := {}
+  /-- The number of transitive imports needed to build the file up to the current command. -/
+  importSize   : Nat := 0
+  deriving Inhabited
+
+/--
+`minImportsRef` keeps track of cumulative imports across multiple commands, using `ImportState`.
+-/
+initialize minImportsRef : IO.Ref ImportState ← IO.mkRef {}
 
 /-- `#reset_min_imports` sets to empty the current list of cumulative imports. -/
 elab "#reset_min_imports" : command => minImportsRef.set {}
@@ -41,9 +59,9 @@ 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
+It also works incrementally, providing information that is better suited, for instance, to split
 files.
- -/
+-/
 register_option linter.minImports : Bool := {
   defValue := false
   descr := "enable the minImports linter"
@@ -53,18 +71,31 @@ namespace MinImports
 
 open Mathlib.Command.MinImports
 
+/-- `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`.
+-/
+def importsBelow (tc : NameMap NameSet) (ms : NameSet) : NameSet :=
+  ms.fold (·.append <| tc.findD · default) ms
+
 @[inherit_doc Mathlib.Linter.linter.minImports]
-def minImportsLinter : Linter where run := withSetOptionIn fun stx => do
+def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do
     unless Linter.getLinterValue linter.minImports (← getOptions) do
       return
-    if (← MonadState.get).messages.hasErrors then
+    if (← get).messages.hasErrors then
       return
     if stx == (← `(command| set_option $(mkIdent `linter.minImports) true)) then return
-    let importsSoFar ← minImportsRef.get
+    let env ← getEnv
+    -- the first time `minImportsRef` is read, it has `transClosure = none`;
+    -- in this case, we set it to be the `transClosure` for the file.
+    if (← minImportsRef.get).transClosure.isNone then
+      minImportsRef.modify ({· with transClosure := env.importGraph.transitiveClosure})
+    let impState ← minImportsRef.get
+    let (importsSoFar, oldCumulImps) := (impState.minImports, impState.importSize)
     -- when the linter reaches the end of the file or `#exit`, it gives a report
     if #[``Parser.Command.eoi, ``Lean.Parser.Command.exit].contains stx.getKind then
       let explicitImportsInFile : NameSet :=
-        .fromArray (((← getEnv).imports.map (·.module)).erase `Init) Name.quickCmp
+        .fromArray ((env.imports.map (·.module)).erase `Init) Name.quickCmp
       let newImps := importsSoFar.diff explicitImportsInFile
       let currentlyUnneededImports := explicitImportsInFile.diff importsSoFar
       -- we read the current file, to do a custom parsing of the imports:
@@ -85,15 +116,22 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx => do
         logWarningAt ((impMods.find? (·.isOfKind `import)).getD default)
           m!"-- missing imports\n{"\n".intercalate withImport.toList}"
     let id ← getId stx
-    let newImports := getIrredundantImports (← getEnv) (← getAllImports stx id)
+    let newImports := getIrredundantImports env (← getAllImports stx id)
     let tot := (newImports.append importsSoFar)
-    let redundant := (← getEnv).findRedundantImports tot.toArray
+    let redundant := env.findRedundantImports tot.toArray
     let currImports := tot.diff redundant
     let currImpArray := currImports.toArray.qsort Name.lt
     if currImpArray != #[] &&
        currImpArray ≠ importsSoFar.toArray.qsort Name.lt then
-      minImportsRef.modify fun _ => currImports
-      Linter.logLint linter.minImports stx m!"Imports increased to\n{currImpArray}"
+      let newCumulImps := -- We should always be in the situation where `getD` finds something
+        (importsBelow (impState.transClosure.getD env.importGraph.transitiveClosure) tot).size
+      minImportsRef.modify ({· with minImports := currImports, importSize := newCumulImps})
+      let new := currImpArray.filter (!importsSoFar.contains ·)
+      let redundant := importsSoFar.toArray.filter (!currImports.contains ·)
+      Linter.logLint linter.minImports stx <|
+        m!"Imports increased by {newCumulImps - oldCumulImps} to\n{currImpArray}\n\n\
+          New imports: {new}\n" ++
+            if redundant.isEmpty then m!"" else m!"\nNow redundant: {redundant}\n"
 
 initialize addLinter minImportsLinter
 

test/MinImports.lean

@@ -75,8 +75,11 @@ import Mathlib.Data.Nat.Notation
 lemma hi (n : ℕ) : n = n := by extract_goal; rfl
 
 /--
-warning: Imports increased to
+warning: Imports increased by 398 to
 [Init.Guard, Mathlib.Data.Int.Notation]
+
+New imports: [Init.Guard, Mathlib.Data.Int.Notation]
+
 note: this linter can be disabled with `set_option linter.minImports false`
 -/
 #guard_msgs in
@@ -92,8 +95,11 @@ set_option linter.minImports false in
 #reset_min_imports
 
 /--
-warning: Imports increased to
+warning: Imports increased by 398 to
 [Init.Guard, Mathlib.Data.Int.Notation]
+
+New imports: [Init.Guard, Mathlib.Data.Int.Notation]
+
 note: this linter can be disabled with `set_option linter.minImports false`
 -/
 #guard_msgs in
@@ -107,16 +113,24 @@ set_option linter.minImports true in
 set_option linter.minImports true
 
 /--
-warning: Imports increased to
+warning: Imports increased by 967 to
 [Mathlib.Tactic.Linter.MinImports]
+
+New imports: [Mathlib.Tactic.Linter.MinImports]
+
 note: this linter can be disabled with `set_option linter.minImports false`
 -/
 #guard_msgs in
 #reset_min_imports
 
 /--
-warning: Imports increased to
+warning: Imports increased by 424 to
 [Mathlib.Tactic.FunProp.Attr, Mathlib.Tactic.NormNum.Basic]
+
+New imports: [Mathlib.Tactic.FunProp.Attr, Mathlib.Tactic.NormNum.Basic]
+
+Now redundant: [Mathlib.Tactic.Linter.MinImports]
+
 note: this linter can be disabled with `set_option linter.minImports false`
 -/
 #guard_msgs in