feat(Tactic/Linter/Header): suggest formatting imports according to the style convention

Mathlib/Algebra/Lie/Solvable.lean

@@ -6,8 +6,8 @@ Authors: Oliver Nash
 module
 
 public import Mathlib.Algebra.Lie.BaseChange
-public import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
 public import Mathlib.Algebra.Lie.Quotient
+public import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
 
 /-!
 # Solvable Lie algebras

Mathlib/Analysis/LocallyConvex/Asymptotics.lean

@@ -5,8 +5,8 @@ Authors: Anatole Dedecker, Moritz Doll
 -/
 module
 
-public import Mathlib.Analysis.Asymptotics.TVS
 public import Mathlib.Analysis.Asymptotics.Basic
+public import Mathlib.Analysis.Asymptotics.TVS
 public import Mathlib.Analysis.LocallyConvex.WithSeminorms
 
 /-!

Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean

@@ -5,8 +5,8 @@ Authors: Jireh Loreaux
 -/
 module
 
-public import Mathlib.Analysis.Normed.Algebra.GelfandRadius
 public import Mathlib.Analysis.Calculus.Deriv.Basic
+public import Mathlib.Analysis.Normed.Algebra.GelfandRadius
 public import Mathlib.Analysis.Normed.Algebra.Spectrum
 public import Mathlib.Analysis.Normed.Operator.Mul
 

Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean

@@ -5,8 +5,8 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition
 public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift
+public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition
 
 /-!
 # Compatibility with shifts of the comparison morphism for the composition of right derived functors

Mathlib/CategoryTheory/Linear/Yoneda.lean

@@ -5,8 +5,8 @@ Authors: Kim Morrison
 -/
 module
 
-public import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
 public import Mathlib.CategoryTheory.Linear.LinearFunctor
+public import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
 
 /-!
 # The Yoneda embedding for `R`-linear categories

Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean

@@ -10,7 +10,6 @@ public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
 
 import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Combinatorics.SimpleGraph.Bipartite
-
 import Mathlib.Tactic.LinearCombination
 
 /-!

Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean

@@ -5,10 +5,10 @@ Authors: Sébastien Gouëzel
 -/
 module
 
+public import Mathlib.Geometry.Manifold.Notation
 public import Mathlib.Geometry.Manifold.VectorBundle.Hom
-public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
 public import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
-public import Mathlib.Geometry.Manifold.Notation
+public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
 
 /-! # The bundle of alternating maps between `C^n` vector bundles over the same base space is `C^n`
 

Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean

@@ -10,9 +10,9 @@ public import Mathlib.LinearAlgebra.PiTensorProduct.Basic
 public import Mathlib.LinearAlgebra.TensorProduct.Map
 
 import Mathlib.Data.Set.Card
+import Mathlib.LinearAlgebra.Finsupp.LinearCombination
 import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.SetTheory.Cardinal.Finite
-import Mathlib.LinearAlgebra.Finsupp.LinearCombination
 
 /-!
 # Generators of multiple tensor products

Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean

@@ -5,9 +5,9 @@ Authors: Rémy Degenne
 -/
 module
 
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
 public import Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
 public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs
-public import Mathlib.MeasureTheory.Integral.Bochner.Basic
 
 import Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
 import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Mathlib/NumberTheory/NumberField/AdeleRing.lean

@@ -5,8 +5,8 @@ Authors: Salvatore Mercuri, María Inés de Frutos-Fernández
 -/
 module
 
-public import Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
 public import Mathlib.NumberTheory.NumberField.FiniteAdeleRing
+public import Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
 
 /-!
 # The adele ring of a number field

Mathlib/Tactic/Common.lean

@@ -124,6 +124,9 @@ public import Mathlib.Util.WhatsNew
 public meta import Lean.Elab.Tactic.Try
 public meta import Lean.Meta.Tactic.Try.Collect
 
+-- Preserve custom import ordering:
+set_option linter.style.header.imports false
+
 /-!
 # Common tactics, linters, and utilities
 

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 meta 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,16 @@ 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 module system import blocks according to the style convention when \
+    `linter.style.header` is `true`."
+}
 
 /-- Returns the `module` token from header syntax, if there is one. -/
 def headerToModuleTk? (header : TSyntax ``Parser.Module.header) : Option Syntax :=
@@ -283,6 +265,8 @@ 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.ImportFormatOff,
   `MathlibTest.Linter.Header.Verso,
   `MathlibTest.DirectoryDependencyLinter.Test]
 
@@ -334,6 +318,32 @@ 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.
+
+Note that this assumes the check for `linter.style.header` has already been performed.
+-/
+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
+  let note := .note m!"This linter can be disabled by writing \
+    `set_option {linter.style.header.imports.name} false` just after the import block."
+  if errs.isEmpty then
+    -- Note: when `errs.isEmpty`, `Import.mkImportSuggestionMessage` gives us a clickable widget
+    -- that uses `diffGranularity := .word`. This effectively gives us a newline before `{msg}`,
+    -- meaning we don't need one after `reformatted:` here.
+    logWarningAt lastImportRef.stx m!"Imports can be reformatted:{msg}{note}"
+  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}{note}"
+
 section HeaderParser
 
 open Lean.ParseImports
@@ -376,6 +386,9 @@ partial def allowedHeaderParser : Parser :=
     keyword "doc.verso.module",
     -- check last, otherwise it prevents hitting the ones it is a prefix of
     keyword "doc.verso",
+    keyword "linter.style.header.license",
+    keyword "linter.style.header.imports",
+    -- check last, otherwise it prevents hitting the ones it is a prefix of
     keyword "linter.style.header" -- for testing and downstream
   ] >> boolLit)
 
@@ -424,7 +437,11 @@ 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
+  -- TODO: Enable this more broadly (Archive, etc., and downstream)
+  if mainModule.getRoot == `Mathlib || headerTestFiles.contains mainModule then
+    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,31 @@
+/-
+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 M̵a̵t̵h̵l̵i̵b̵.̵I̵n̵i̵t̵
+  ̵i̵m̵p̵o̵r̵t̵ ̵Lean.Elab.Command
+  ̲i̲m̲p̲o̲r̲t̲ ̲M̲a̲t̲h̲l̲i̲b̲.̲I̲n̲i̲t̲
+
+Note: This linter can be disabled by writing `set_option linter.style.header.imports false` just after the import block.
+-/
+#guard_msgs in
+set_option linter.style.header true in
+/-! -/

MathlibTest/Linter/Header/ImportFormatOff.lean

@@ -0,0 +1,21 @@
+/-
+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
+
+set_option linter.style.header.imports false
+
+#guard_msgs in
+set_option linter.style.header true in
+/-! -/