From 885ddec71c2be93441a8f0ef05601de074d9c6d6 Mon Sep 17 00:00:00 2001 From: adomani Date: Sun, 27 Oct 2024 22:17:00 +0000 Subject: [PATCH 1/7] feat: add by how many modules imports grew --- Mathlib/Tactic/Linter/MinImports.lean | 44 +++++++++++++++++++-------- 1 file changed, 31 insertions(+), 13 deletions(-) diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index 202d32297ca82..bca762ac9ecf9 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -28,11 +28,16 @@ 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 {} +/-- `minImportsRef` keeps track of cumulative imports across multiple commands. +* The first component stores the `NameSet` of minimal modules required for the file to + build up to the current linting position. +* The second component stores the number of modules that transitively imported by the `NameSet` + stored in the first component. +-/ +initialize minImportsRef : IO.Ref (NameSet × Nat) ← IO.mkRef ({}, 0) /-- `#reset_min_imports` sets to empty the current list of cumulative imports. -/ -elab "#reset_min_imports" : command => minImportsRef.set {} +elab "#reset_min_imports" : command => minImportsRef.set ({}, 0) /-- The `minImports` linter incrementally computes the minimal imports needed for each file to build. @@ -41,9 +46,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 +58,25 @@ namespace MinImports open Mathlib.Command.MinImports +/-- `impsBelow env ms` takes as input an `Environment` `env` and a `NameSet` of module names `ms`. +It returns the modules that are transitively imported by `ms`. +-/ +def importsBelow (env : Environment) (ms : NameSet) : NameSet := + (env.importGraph.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 + let (importsSoFar, oldCumulImps) ← minImportsRef.get -- 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 +97,21 @@ 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 := (importsBelow env tot).size + minImportsRef.set (currImports, 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\ + Now redundant: {redundant}\n\n\ + New imports: {new}\n" initialize addLinter minImportsLinter From 3ccb8e59dfa303cbed9febb4e1ea7f48db89d088 Mon Sep 17 00:00:00 2001 From: adomani Date: Sun, 27 Oct 2024 23:18:31 +0000 Subject: [PATCH 2/7] fix test messages --- test/MinImports.lean | 28 ++++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/test/MinImports.lean b/test/MinImports.lean index abf1594c8f565..d64cbdb35ae42 100644 --- a/test/MinImports.lean +++ b/test/MinImports.lean @@ -75,8 +75,13 @@ 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] + +Now redundant: [] + +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 +97,13 @@ 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] + +Now redundant: [] + +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 +117,26 @@ 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] + +Now redundant: [] + +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] + +Now redundant: [Mathlib.Tactic.Linter.MinImports] + +New imports: [Mathlib.Tactic.FunProp.Attr, Mathlib.Tactic.NormNum.Basic] + note: this linter can be disabled with `set_option linter.minImports false` -/ #guard_msgs in From f34c08f34b8ce0666aec25ef0d13ac145dfa7394 Mon Sep 17 00:00:00 2001 From: adomani Date: Sun, 27 Oct 2024 23:34:47 +0000 Subject: [PATCH 3/7] store all the import graph --- Mathlib/Tactic/Linter/MinImports.lean | 37 ++++++++++++++++++--------- 1 file changed, 25 insertions(+), 12 deletions(-) diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index bca762ac9ecf9..f174dc483e368 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -28,16 +28,25 @@ The "minImports" linter tracks information about minimal imports over several co namespace Mathlib.Linter -/-- `minImportsRef` keeps track of cumulative imports across multiple commands. -* The first component stores the `NameSet` of minimal modules required for the file to - build up to the current linting position. -* The second component stores the number of modules that transitively imported by the `NameSet` - stored in the first component. +/-- +`ImportState` is the structure keeping track of the data that the `minImports` linter uses. +* `ig` is the import graph of the current file. +* `minImps` is the `NameSet` of minimal imports for the file up to the current command to build. +* `impsSize` is the number of transitive imports for the file up to the current command to build. +-/ +structure ImportState where + ig : Option (NameMap (Array Name)) := none + minImps : NameSet := {} + impsSize : Nat := 0 + deriving Inhabited + +/-- +`minImportsRef` keeps track of cumulative imports across multiple commands, using `ImportState`. -/ -initialize minImportsRef : IO.Ref (NameSet × Nat) ← IO.mkRef ({}, 0) +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 ({}, 0) +elab "#reset_min_imports" : command => minImportsRef.set {} /-- The `minImports` linter incrementally computes the minimal imports needed for each file to build. @@ -61,8 +70,8 @@ open Mathlib.Command.MinImports /-- `impsBelow env ms` takes as input an `Environment` `env` and a `NameSet` of module names `ms`. It returns the modules that are transitively imported by `ms`. -/ -def importsBelow (env : Environment) (ms : NameSet) : NameSet := - (env.importGraph.upstreamOf ms).fold (σ := NameSet) (fun _ ↦ ·.insert ·) {} +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 @@ -72,7 +81,11 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do return if stx == (← `(command| set_option $(mkIdent `linter.minImports) true)) then return let env ← getEnv - let (importsSoFar, oldCumulImps) ← minImportsRef.get + -- 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).ig.isNone then minImportsRef.modify ({· with ig := env.importGraph}) + let impState ← minImportsRef.get + let (importsSoFar, oldCumulImps) := (impState.minImps, impState.impsSize) -- 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 := @@ -104,8 +117,8 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do let currImpArray := currImports.toArray.qsort Name.lt if currImpArray != #[] && currImpArray ≠ importsSoFar.toArray.qsort Name.lt then - let newCumulImps := (importsBelow env tot).size - minImportsRef.set (currImports, newCumulImps) + let newCumulImps := (importsBelow env.importGraph tot).size + minImportsRef.set {minImps := currImports, impsSize := newCumulImps} let new := currImpArray.filter (!importsSoFar.contains ·) let redundant := importsSoFar.toArray.filter (!currImports.contains ·) Linter.logLint linter.minImports stx From 6944589bba1a635159af6eeaa6df09a454d1de2e Mon Sep 17 00:00:00 2001 From: adomani Date: Sun, 27 Oct 2024 23:46:51 +0000 Subject: [PATCH 4/7] fix doc-strings --- Mathlib/Tactic/Linter/MinImports.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index f174dc483e368..a1594cf709214 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -31,8 +31,8 @@ namespace Mathlib.Linter /-- `ImportState` is the structure keeping track of the data that the `minImports` linter uses. * `ig` is the import graph of the current file. -* `minImps` is the `NameSet` of minimal imports for the file up to the current command to build. -* `impsSize` is the number of transitive imports for the file up to the current command to build. +* `minImps` is the `NameSet` of minimal imports to build the file up to the current command. +* `impsSize` is the number of transitive imports to build the file up to the current command. -/ structure ImportState where ig : Option (NameMap (Array Name)) := none @@ -67,8 +67,8 @@ namespace MinImports open Mathlib.Command.MinImports -/-- `impsBelow env ms` takes as input an `Environment` `env` and a `NameSet` of module names `ms`. -It returns the modules that are transitively imported by `ms`. +/-- `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 ·) {} From 29ea27e09d55434be5610b070b13a3b393aa7d93 Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 28 Oct 2024 00:10:33 +0000 Subject: [PATCH 5/7] Kim's comments --- Mathlib/Tactic/Linter/MinImports.lean | 27 ++++++++++++++------------- test/MinImports.lean | 10 ++-------- 2 files changed, 16 insertions(+), 21 deletions(-) diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index a1594cf709214..e57ce2df10481 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -30,14 +30,14 @@ namespace Mathlib.Linter /-- `ImportState` is the structure keeping track of the data that the `minImports` linter uses. -* `ig` is the import graph of the current file. -* `minImps` is the `NameSet` of minimal imports to build the file up to the current command. -* `impsSize` is the number of transitive imports to build the file up to the current command. +* `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 - ig : Option (NameMap (Array Name)) := none - minImps : NameSet := {} - impsSize : Nat := 0 + importGraph : Option (NameMap (Array Name)) := none + minImports : NameSet := {} + importSize : Nat := 0 deriving Inhabited /-- @@ -83,9 +83,10 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do 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).ig.isNone then minImportsRef.modify ({· with ig := env.importGraph}) + if (← minImportsRef.get).importGraph.isNone then + minImportsRef.modify ({· with importGraph := env.importGraph}) let impState ← minImportsRef.get - let (importsSoFar, oldCumulImps) := (impState.minImps, impState.impsSize) + 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 := @@ -117,14 +118,14 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do let currImpArray := currImports.toArray.qsort Name.lt if currImpArray != #[] && currImpArray ≠ importsSoFar.toArray.qsort Name.lt then - let newCumulImps := (importsBelow env.importGraph tot).size - minImportsRef.set {minImps := currImports, impsSize := newCumulImps} + 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 + Linter.logLint linter.minImports stx <| m!"Imports increased by {newCumulImps - oldCumulImps} to\n{currImpArray}\n\n\ - Now redundant: {redundant}\n\n\ - New imports: {new}\n" + New imports: {new}\n" ++ + if redundant.isEmpty then m!"" else m!"\nNow redundant: {redundant}\n" initialize addLinter minImportsLinter diff --git a/test/MinImports.lean b/test/MinImports.lean index d64cbdb35ae42..49f838a69d1af 100644 --- a/test/MinImports.lean +++ b/test/MinImports.lean @@ -78,8 +78,6 @@ lemma hi (n : ℕ) : n = n := by extract_goal; rfl warning: Imports increased by 398 to [Init.Guard, Mathlib.Data.Int.Notation] -Now redundant: [] - New imports: [Init.Guard, Mathlib.Data.Int.Notation] note: this linter can be disabled with `set_option linter.minImports false` @@ -100,8 +98,6 @@ set_option linter.minImports false in warning: Imports increased by 398 to [Init.Guard, Mathlib.Data.Int.Notation] -Now redundant: [] - New imports: [Init.Guard, Mathlib.Data.Int.Notation] note: this linter can be disabled with `set_option linter.minImports false` @@ -120,8 +116,6 @@ set_option linter.minImports true warning: Imports increased by 967 to [Mathlib.Tactic.Linter.MinImports] -Now redundant: [] - New imports: [Mathlib.Tactic.Linter.MinImports] note: this linter can be disabled with `set_option linter.minImports false` @@ -133,10 +127,10 @@ note: this linter can be disabled with `set_option linter.minImports false` warning: Imports increased by 424 to [Mathlib.Tactic.FunProp.Attr, Mathlib.Tactic.NormNum.Basic] -Now redundant: [Mathlib.Tactic.Linter.MinImports] - 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 From 7211477462d49aad0b30368412f09b70beee1d22 Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 28 Oct 2024 07:34:14 +0000 Subject: [PATCH 6/7] use transitive closure --- Mathlib/Tactic/Linter/MinImports.lean | 28 ++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index e57ce2df10481..af02d8d4a9d83 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -30,14 +30,14 @@ namespace Mathlib.Linter /-- `ImportState` is the structure keeping track of the data that the `minImports` linter uses. -* `importGraph` is the import graph of the current file. +* `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 - importGraph : Option (NameMap (Array Name)) := none - minImports : NameSet := {} - importSize : Nat := 0 + transClosure : Option (NameMap NameSet) := none + minImports : NameSet := {} + importSize : Nat := 0 deriving Inhabited /-- @@ -67,11 +67,12 @@ namespace MinImports 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`. +/-- `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 (ig : NameMap (Array Name)) (ms : NameSet) : NameSet := - (ig.upstreamOf ms).fold (σ := NameSet) (fun _ ↦ ·.insert ·) {} +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 @@ -81,10 +82,10 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do return if stx == (← `(command| set_option $(mkIdent `linter.minImports) true)) then return 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}) + -- 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 @@ -118,7 +119,8 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do let currImpArray := currImports.toArray.qsort Name.lt if currImpArray != #[] && currImpArray ≠ importsSoFar.toArray.qsort Name.lt then - let newCumulImps := (importsBelow (impState.importGraph.getD env.importGraph) tot).size + 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 ·) From 894f7a8ec92bed2e2fc3799a841ecccbddea9352 Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 28 Oct 2024 08:53:53 +0000 Subject: [PATCH 7/7] docs --- Mathlib/Tactic/Linter/MinImports.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index af02d8d4a9d83..c057808b885da 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -35,8 +35,12 @@ namespace Mathlib.Linter * `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