chore: use import graph 171 for header linter suggestions

Mathlib/Tactic/Linter/Header.lean

@@ -5,11 +5,11 @@ Authors: Michael Rothgang, Damiano Testa, Thomas R. Murrills
 -/
 module
 
-public meta import Lean.Elab.Command
+public meta import ImportGraph.Imports.Pretty
+public meta import Lean.Linter.Basic
 public meta import Std.Sync.Mutex
 public import Lean.Parser.Module
 public import Mathlib.Tactic.Linter.DirectoryDependency
-public meta import Lean.Linter.Basic
 public import Std.Sync.Mutex
 
 /-!
@@ -47,7 +47,7 @@ a module doc-string (unless the command is exempted for some reason).
 
 meta section
 
-open Lean Elab Command Linter
+open ImportGraph Lean Elab Command Linter
 
 namespace Mathlib.Linter
 
@@ -233,34 +233,15 @@ public register_option linter.style.header.license : String := {
   descr := "The text required as the second line of the copyright header."
 }
 
-/-- Extends `Import` with ``stx : TSyntax `Lean.Parser.Module.import`` to allow reporting at the
-given import. -/
-structure ImportRef extends Import where
-  stx : TSyntax ``Parser.Module.import
-
-/-- Returns the module `Ident` (following `(public)? (meta)? import (all)?` of a given
-`ImportRef`. -/
-def ImportRef.getIdent (i : ImportRef) : Ident :=
-  match i.stx with
-  | `(Parser.Module.import|
-      $[public]? $[meta]? import $[all]? $n:ident) => n
-  | _ => ⟨.missing⟩
-
-/-- Destructures header syntax (`(module)? (prelude)? $imports*`) into an array of `ImportRef`s. -/
-def headerToImportRefs (header : TSyntax ``Parser.Module.header) : Array ImportRef :=
-  match header with
-  | `(Parser.Module.header| $[module%$moduleTk]? $[prelude]? $imports*) =>
-    imports.filterMap fun
-      | stx@`(Parser.Module.import|
-          $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n:ident) =>
-        some {
-          module := n.getId
-          importAll := allTk.isSome
-          isExported := publicTk.isSome || moduleTk.isNone
-          isMeta := metaTk.isSome
-          stx := ⟨stx⟩ }
-      | _ => none
-  | _ => #[]
+/--
+Whether to reformat import blocks in the module system according to the style convention. Note that
+this only has an effect if `linter.style.header` is `true` and the header is participating in the
+module system. This does not remove redundant imports.
+-/
+public register_option linter.style.header.imports : Bool := {
+  defValue := true
+  descr := "Whether to reformat import blocks according to the style convention."
+}
 
 /-- Returns the `module` token from header syntax, if there is one. -/
 def headerToModuleTk? (header : TSyntax ``Parser.Module.header) : Option Syntax :=
@@ -283,6 +264,7 @@ because they are files that test the linter.
 def headerTestFiles : NameSet := .ofList [
   `MathlibTest.Linter.Header.Basic,
   `MathlibTest.Linter.Header.Fail,
+  `MathlibTest.Linter.Header.ImportFormat,
   `MathlibTest.Linter.Header.Verso,
   `MathlibTest.DirectoryDependencyLinter.Test]
 
@@ -334,6 +316,28 @@ def duplicateImportsCheck (imports : Array ImportRef) : CommandElabM Unit := do
     else
       importsSoFar := importsSoFar.insert imp.toImport
 
+/--
+If we are in the module system and `linter.style.header.imports` is `true`, reformat imports.
+-/
+def formatImports (imports : Array (ImportRef × Import.Whitespace)) : CommandElabM Unit := do
+  unless
+    (← getEnv).header.isModule && getLinterValue linter.style.header.imports (← getLinterOptions)
+  do
+    return
+  let some (lastImportRef, _) := imports.back? | return
+  let impsRef := mkNullNode <| imports.map (·.1.stx)
+  let some (msg, errs) ← liftCoreM <|
+      Import.mkImportSuggestionMessage impsRef (imports.map (·.1.toImport)) imports
+    | return
+  -- Note: potentially, we should just bail if there are errors.
+  if errs.isEmpty then
+    -- Note: the widget nature of `diffGranularity := .word` effectively gives us a newline
+    -- before `{msg}`, meaning we don't need one here.
+    logWarningAt lastImportRef.stx m!"Imports can be reformatted:{msg}"
+  else
+    logWarningAt lastImportRef.stx m!"Imports can be reformatted, but some comments could not be \
+      carried over. Please review the comment that will be inserted after the imports.\n{msg}"
+
 @[inherit_doc Mathlib.Linter.linter.style.header]
 def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
   unless getLinterValue linter.style.header (← getLinterOptions) do
@@ -376,7 +380,9 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
   -- Re-parse the header slowly, to get the leading whitespace and nice source locations for imports
   let (headerStx, s, log) ← Parser.parseHeader (Parser.mkInputContext map.source (← getFileName))
   if log.hasErrors then return
-  let importRefs := headerToImportRefs headerStx
+  let importRefsWithWhitespace := headerToImportRefsWithWhitespace headerStx
+  formatImports importRefsWithWhitespace
+  let importRefs := importRefsWithWhitespace.map (·.1)
   -- Report on broad or duplicate imports.
   broadImportsCheck importRefs mainModule
   duplicateImportsCheck importRefs

MathlibTest/Linter/Header/ImportFormat.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
+module
+
+import Mathlib.Init
+meta import Mathlib.Init
+
+
+   public meta   import Mathlib.Init
+
+public import Mathlib.Init
+import Lean.Elab.Command
+
+/--
+warning: Imports can be reformatted:
+  i̵m̵p̵o̵r̵t̵ ̵M̵a̵t̵h̵l̵i̵b̵.̵I̵n̵i̵t̵p̲u̲b̲l̲i̲c̲ meta import Mathlib.Init
+  public i̲m̲p̲o̲r̲t̲ ̲M̲a̲t̲h̲l̲i̲b̲.̲I̲n̲i̲t̲
+  ̲
+  ̲meta  ̵ ̵import Mathlib.Init
+  p̵u̵b̵l̵i̵c̵ ̵import Mathlib.Init
+  import Lean.Elab.Command
+-/
+#guard_msgs in
+set_option linter.style.header true in
+/-! -/

lake-manifest.json

@@ -21,14 +21,14 @@
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/thorimur/import-graph",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "7ad9f2e325aa6cec3dacaa97c2653a98032750eb",
+   "scope": "",
+   "rev": "80ac24ded84c7807ea95eb70a775bc301b79e63b",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "pretty-import-cmp",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",

lakefile.lean

@@ -14,7 +14,7 @@ require "leanprover-community" / "proofwidgets" @ git "main"
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets failed to reuse pre-built JS code. \
     Please report this issue on the Lean Zulip."
-require "leanprover-community" / "importGraph" @ git "main"
+require importGraph from git "https://github.com/thorimur/import-graph" @ "pretty-import-cmp"
 require "leanprover-community" / "LeanSearchClient" @ git "main"
 require "leanprover-community" / "plausible" @ git "main"