diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index 202d32297ca82..c057808b885da 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/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 diff --git a/test/MinImports.lean b/test/MinImports.lean index abf1594c8f565..49f838a69d1af 100644 --- a/test/MinImports.lean +++ b/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