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

Mathlib/Tactic/Linter/MinImports.lean

@@ -28,8 +28,22 @@
 
 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.
+* `importGraph` 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
+  importGraph : Option (NameMap (Array Name)) := none
+  minImports : NameSet := {}
+  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 +55,9 @@
 
 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 +67,30 @@
 
 open Mathlib.Command.MinImports
 
+/-- `impsBelow ig ms` takes as input an `importGraph` `ig` and a `NameSet` of module names `ms`.
+It returns the modules that are transitively imported by `ms`, using the data in `ig`.
+-/
+def importsBelow (ig : NameMap (Array Name)) (ms : NameSet) : NameSet :=
+  (ig.upstreamOf ms).fold (σ := NameSet) (fun _ ↦ ·.insert ·) {}
+
 @[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 `ig = none`; in this case, we set it to
+    -- be the `importGraph` for the file.
+    if (← minImportsRef.get).importGraph.isNone then
+      minImportsRef.modify ({· with importGraph := env.importGraph})
+    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 +111,21 @@
         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 := (importsBelow (impState.importGraph.getD env.importGraph) 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