feat: rewrite the duplicateImports linter (#17555)

as part of the header linter. This yields better error spans, is more robust (as it avoids false positives from text-based parsing) and yields results more quickly (providing a better user experience).

Also rewrite the `broadImports` linter to log warnings directly, as opposed to passing them down to the `headerLinter` and logging them there.



Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Co-authored-by: adomani <adomani@gmail.com>

Author: grunweg

Mathlib/Tactic/Linter/Header.lean

@@ -205,36 +205,6 @@ def copyrightHeaderChecks (copyright : String) : Array (Syntax × String) := Id.
     output := output.push (toSyntax copyright "-/", s!"Copyright too short!")
   return output
 
-/-- Check the `Syntax` `imports` for broad imports: either `Mathlib.Tactic` or any import
-starting with `Lake`. -/
-def broadImportsCheck (imports : Array Syntax) (mainModule : Name) : Array (Syntax × String) := Id.run do
-  let mut output := #[]
-  for i in imports do
-    match i.getId with
-    | `Mathlib.Tactic =>
-      output := output.push (i, s!"Files in mathlib cannot import the whole tactic folder.")
-    | `Mathlib.Tactic.Replace =>
-      if mainModule != `Mathlib.Tactic then output := output.push (i,
-      s!"Mathlib.Tactic.Replace defines a deprecated form of the 'replace' tactic; \
-      please do not use it in mathlib.")
-    | `Mathlib.Tactic.Have =>
-      if ![`Mathlib.Tactic, `Mathlib.Tactic.Replace].contains mainModule then
-        output := output.push (i,
-          s!"Mathlib.Tactic.Have defines a deprecated form of the 'have' tactic; \
-          please do not use it in mathlib.")
-    | modName =>
-      if modName.getRoot == `Lake then
-      output := output.push (i,
-        s!"In the past, importing 'Lake' in mathlib has led to dramatic slow-downs of the linter \
-          (see e.g. mathlib4#13779). Please consider carefully if this import is useful and \
-          make sure to benchmark it. If this is fine, feel free to allow this linter.")
-      else if (`Mathlib.Deprecated).isPrefixOf modName &&
-          !(`Mathlib.Deprecated).isPrefixOf mainModule then
-        -- We do not complain about files in the `Deprecated` directory importing one another.
-        output := output.push (i, s!"Files in the `Deprecated` directory are not supposed to be imported.")
-
-  return output
-
 /--
 The "header" style linter checks that a file starts with
 ```
@@ -263,6 +233,47 @@ register_option linter.style.header : Bool := {
 
 namespace Style.header
 
+/-- Check the `Syntax` `imports` for broad imports:
+`Mathlib.Tactic`, any import starting with `Lake`, `Mathlib.Tactic.{Have,Replace}`
+or anything in the `Deprecated` folder. -/
+def broadImportsCheck (imports : Array Syntax) (mainModule : Name) : CommandElabM Unit := do
+  for i in imports do
+    match i.getId with
+    | `Mathlib.Tactic =>
+      Linter.logLint linter.style.header i "Files in mathlib cannot import the whole tactic folder."
+    | `Mathlib.Tactic.Replace =>
+      if mainModule != `Mathlib.Tactic then
+        Linter.logLint linter.style.header i
+          "'Mathlib.Tactic.Replace' defines a deprecated form of the 'replace' tactic; \
+          please do not use it in mathlib."
+    | `Mathlib.Tactic.Have =>
+      if ![`Mathlib.Tactic, `Mathlib.Tactic.Replace].contains mainModule then
+        Linter.logLint linter.style.header i
+          "'Mathlib.Tactic.Have' defines a deprecated form of the 'have' tactic; \
+          please do not use it in mathlib."
+    | modName =>
+      if modName.getRoot == `Lake then
+      Linter.logLint linter.style.header i
+        "In the past, importing 'Lake' in mathlib has led to dramatic slow-downs of the linter \
+        (see e.g. mathlib4#13779). Please consider carefully if this import is useful and \
+        make sure to benchmark it. If this is fine, feel free to silence this linter."
+      else if (`Mathlib.Deprecated).isPrefixOf modName &&
+          !(`Mathlib.Deprecated).isPrefixOf mainModule then
+        -- We do not complain about files in the `Deprecated` directory importing one another.
+        Linter.logLint linter.style.header i
+          "Files in the `Deprecated` directory are not supposed to be imported."
+
+/-- Check the syntax `imports` for syntactically duplicate imports.
+The output is an array of `Syntax` atoms whose ranges are the import statements,
+and the embedded strings are the error message of the linter.
+-/
+def duplicateImportsCheck (imports : Array Syntax)  : CommandElabM Unit := do
+  let mut importsSoFar := #[]
+  for i in imports do
+    if importsSoFar.contains i then
+      Linter.logLint linter.style.header i m!"Duplicate imports: '{i}' already imported"
+    else importsSoFar := importsSoFar.push i
+
 @[inherit_doc Mathlib.Linter.linter.style.header]
 def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
   unless Linter.getLinterValue linter.style.header (← getOptions) do
@@ -290,9 +301,10 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
     let (stx, _) ← Parser.parseHeader { input := fm.source, fileName := fil, fileMap := fm }
     parseUpToHere (stx.getTailPos?.getD default) "\nsection")
   let importIds := getImportIds upToStx
-  -- Report on broad imports.
-  for (imp, msg) in broadImportsCheck importIds mainModule do
-    Linter.logLint linter.style.header imp msg
+  -- Report on broad or duplicate imports.
+  broadImportsCheck importIds mainModule
+  duplicateImportsCheck importIds
+
   let afterImports := firstNonImport? upToStx
   if afterImports.isNone then return
   let copyright := match upToStx.getHeadInfo with

Mathlib/Tactic/Linter/TextBased.lean

@@ -6,7 +6,6 @@ Authors: Michael Rothgang
 
 import Batteries.Data.String.Matcher
 import Mathlib.Data.Nat.Notation
-import Std.Data.HashMap.Basic
 
 /-!
 ## Text-based linters
@@ -57,7 +56,6 @@ inductive StyleError where
   | adaptationNote
   /-- A line ends with windows line endings (\r\n) instead of unix ones (\n). -/
   | windowsLineEnding
-  | duplicateImport (importStatement: String) (alreadyImportedLine: ℕ)
 deriving BEq
 
 /-- How to format style errors -/
@@ -78,16 +76,13 @@ def StyleError.errorMessage (err : StyleError) : String := match err with
     "Found the string \"Adaptation note:\", please use the #adaptation_note command instead"
   | windowsLineEnding => "This line ends with a windows line ending (\r\n): please use Unix line\
     endings (\n) instead"
-  | StyleError.duplicateImport (importStatement) (alreadyImportedLine) =>
-    s!"Duplicate imports: {importStatement} (already imported on line {alreadyImportedLine})"
 
 /-- The error code for a given style error. Keep this in sync with `parse?_errorContext` below! -/
 -- FUTURE: we're matching the old codes in `lint-style.py` for compatibility;
 -- in principle, we could also print something more readable.
 def StyleError.errorCode (err : StyleError) : String := match err with
   | StyleError.adaptationNote => "ERR_ADN"
   | StyleError.windowsLineEnding => "ERR_WIN"
-  | StyleError.duplicateImport _ _ => "ERR_DIMP"
 
 /-- Context for a style error: the actual error, the line number in the file we're reading
 and the path to the file. -/
@@ -122,12 +117,8 @@ def compare (existing new : ErrorContext) : ComparisonResult :=
 
   -- NB: keep the following in sync with `parse?_errorContext` below.
   -- Generally, comparable errors must have equal `StyleError`s.
-  else match (existing.error, new.error) with
-  -- We do *not* care about the kind or line number of a duplicate import.
-  | (StyleError.duplicateImport _ _, StyleError.duplicateImport _ _) =>
-    ComparisonResult.Comparable
-  -- In all other cases, `StyleErrors` must compare equal.
-  | (a, b) => if a == b then ComparisonResult.Comparable else ComparisonResult.Different
+  else
+    if existing.error == new.error then ComparisonResult.Comparable else ComparisonResult.Different
 
 /-- Find the first style exception in `exceptions` (if any) which covers a style exception `e`. -/
 def ErrorContext.find?_comparable (e : ErrorContext) (exceptions : Array ErrorContext) :
@@ -170,7 +161,6 @@ def parse?_errorContext (line : String) : Option ErrorContext := Id.run do
         -- NB: keep this in sync with `compare` above!
         | "ERR_ADN" => some (StyleError.adaptationNote)
         | "ERR_WIN" => some (StyleError.windowsLineEnding)
-        | "ERR_DIMP" => some (StyleError.duplicateImport "" 0)
         | _ => none
       match String.toNat? lineNumber with
       | some n => err.map fun e ↦ (ErrorContext.mk e n path)
@@ -214,26 +204,6 @@ def adaptationNoteLinter : TextbasedLinter := fun lines ↦ Id.run do
     lineNumber := lineNumber + 1
   return (errors, none)
 
-/-- Lint on a collection of input strings if one of the is a duplicate import statement. -/
-def duplicateImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
-  let mut lineNumber := 1
-  let mut errors := Array.mkEmpty 0
-  let mut importStatements : Std.HashMap String ℕ := {}
-  for line in lines do
-    if line.startsWith "import " then
-      let lineWithoutComment := (line.splitOn "--")[0]!
-      let importStatement := lineWithoutComment.trim
-      if importStatements.contains importStatement then
-        let alreadyImportedLine := importStatements[importStatement]!
-        errors := errors.push (
-          (StyleError.duplicateImport importStatement alreadyImportedLine),
-          lineNumber
-        )
-      else
-        importStatements := importStatements.insert importStatement lineNumber
-    lineNumber := lineNumber + 1
-  return (errors, none)
-
 /-- Whether a collection of lines consists *only* of imports, blank lines and single-line comments.
 In practice, this means it's an imports-only file and exempt from almost all linting. -/
 def isImportsOnlyFile (lines : Array String) : Bool :=
@@ -245,7 +215,7 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    adaptationNoteLinter, duplicateImportsLinter
+    adaptationNoteLinter
   ]
 
 

MathlibTest/Header.lean

@@ -6,23 +6,27 @@ Authors: Damiano Testa
 
 import Mathlib.Tactic.Linter.Header
 import Lake
+import Mathlib.Tactic.Linter.Header
 import /- -/ Mathlib.Tactic -- the `TextBased` linter does not flag this `broadImport`
 import Mathlib.Tactic.Have
 import Mathlib.Deprecated.Subfield
 
 /--
-warning: In the past, importing 'Lake' in mathlib has led to dramatic slow-downs of the linter (see e.g. mathlib4#13779). Please consider carefully if this import is useful and make sure to benchmark it. If this is fine, feel free to allow this linter.
+warning: In the past, importing 'Lake' in mathlib has led to dramatic slow-downs of the linter (see e.g. mathlib4#13779). Please consider carefully if this import is useful and make sure to benchmark it. If this is fine, feel free to silence this linter.
 note: this linter can be disabled with `set_option linter.style.header false`
 ---
 warning: Files in mathlib cannot import the whole tactic folder.
 note: this linter can be disabled with `set_option linter.style.header false`
 ---
-warning: Mathlib.Tactic.Have defines a deprecated form of the 'have' tactic; please do not use it in mathlib.
+warning: 'Mathlib.Tactic.Have' defines a deprecated form of the 'have' tactic; please do not use it in mathlib.
 note: this linter can be disabled with `set_option linter.style.header false`
 ---
 warning: Files in the `Deprecated` directory are not supposed to be imported.
 note: this linter can be disabled with `set_option linter.style.header false`
 ---
+warning: Duplicate imports: 'Mathlib.Tactic.Linter.Header' already imported
+note: this linter can be disabled with `set_option linter.style.header false`
+---
 warning: The module doc-string for a file should be the first command after the imports.
 Please, add a module doc-string before `/-!# Tests for the `docModule` linter
 -/

scripts/nolints-style.txt

@@ -15,7 +15,3 @@ Mathlib/Tactic/Linter/TextBased.lean : line 84 : ERR_ADN : Found the string "Ada
 Mathlib/Tactic/Linter/TextBased.lean : line 274 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
 Mathlib/Tactic/Linter/TextBased.lean : line 279 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
 Mathlib/Tactic/Linter/TextBased.lean : line 280 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
-
--- The "duplicate imports" linter fires on this line inside a multi-line module docstring,
--- which says 'import statements': this is a false positive.
-Mathlib/Tactic/Linter/Header.lean : line 228 : ERR_DIMP : Duplicate imports: import statements* (already imported on line 19)