feat(Linter): check import formatting in modified files

.github/workflows/build_template.yml

@@ -1022,6 +1022,42 @@ jobs:
           lint-bib-file: true
           ref: ${{ inputs.pr_branch_ref }}
 
+      # Import grouping has many pre-existing violations, so enforce it only in files changed from
+      # the repository's default branch. A separate cleanup PR can normalize the existing files.
+      - name: Check import formatting in modified Mathlib files
+        env:
+          BASE_BRANCH: ${{ github.event.repository.default_branch }}
+        shell: bash
+        run: |
+          base_ref="refs/remotes/origin/${BASE_BRANCH}"
+          refspec="+refs/heads/${BASE_BRANCH}:${base_ref}"
+          git fetch --no-tags origin "${refspec}"
+          if ! merge_base="$(git merge-base "origin/${BASE_BRANCH}" HEAD)"; then
+            # `lint-style-action` uses a shallow checkout. Usually fetching the base branch gives
+            # `merge-base` enough history; deepen only when the branch point is older.
+            git fetch --no-tags --unshallow origin "${refspec}"
+            merge_base="$(git merge-base "origin/${BASE_BRANCH}" HEAD)"
+          fi
+
+          changed_files="${RUNNER_TEMP}/import-style-changed-files"
+          git diff --name-only -z --diff-filter=ACMR "${merge_base}"...HEAD -- Mathlib \
+            > "${changed_files}"
+
+          modules=()
+          while IFS= read -r -d '' file; do
+            if [[ "${file}" == Mathlib/*.lean ]]; then
+              module="${file%.lean}"
+              modules+=("${module//\//.}")
+            fi
+          done < "${changed_files}"
+
+          if (( ${#modules[@]} > 0 )); then
+            printf 'Fix with: lake exe lint-style --imports --fix --only'
+            printf ' %q' "${modules[@]}"
+            printf '\n'
+            lake exe lint-style --github --imports --only "${modules[@]}"
+          fi
+
   final:
     name: Post-CI job
     # ensure that this runs iff direct dependencies succeeded even if transitive dependencies  were skipped

Mathlib/Tactic/Linter/TextBased.lean

@@ -5,6 +5,8 @@ Authors: Michael Rothgang, Jon Eugster, Adomas Baliuka
 -/
 module
 
+public meta import ImportGraph.Imports.Pretty
+public meta import ImportGraph.Lean.Syntax
 public meta import Lake.Util.Casing
 public import Mathlib.Data.Nat.Notation
 public meta import Mathlib.Tactic.Linter.TextBased.UnicodeLinter
@@ -32,6 +34,7 @@ Currently, this file contains linters checking
   `!`, `.` or spaces.
 - for any code containing unicode characters not on the allowlist
 - for incorrect usage of unicode variant selectors
+- for incorrectly grouped public and private imports
 
 This linter has a file for style exceptions (to avoid false positives in the implementation),
 or for downstream projects to allow a gradual adoption of this linter.
@@ -62,6 +65,8 @@ inductive StyleError where
   * `selector` is the desired selector or `none`
   -/
   | unicodeVariant (s : String) (selector: Option Char)
+  /-- Public and private imports are not grouped as prescribed by the style guide. -/
+  | importFormatting
 deriving BEq, Inhabited
 
 /-- How to format style errors -/
@@ -115,6 +120,8 @@ def StyleError.errorMessage (err : StyleError) : String := match err with
     | _, _ =>
       s!"Unexpected unicode variant selector: \"{s}\" ({oldHex}). \
         Consider deleting it."
+  | importFormatting =>
+    "Public imports must precede private imports, with a blank line between the two groups"
 
 /-- The error code for a given style error. Keep this in sync with `parse?_errorContext` below! -/
 -- The error codes were chosen like this for historic reasons. In principle, we could also print
@@ -126,6 +133,7 @@ def StyleError.errorCode (err : StyleError) : String := match err with
   | StyleError.semicolon => "ERR_SEM"
   | StyleError.unwantedUnicode _ => "ERR_UNICODE"
   | StyleError.unicodeVariant _ _ => "ERR_UNICODE_VARIANT"
+  | StyleError.importFormatting => "ERR_IMPORTS"
 
 
 /-- Context for a style error: the actual error, the line number in the file we're reading
@@ -238,6 +246,7 @@ def parse?_errorContext (line : String) : Option ErrorContext := Id.run do
             let offending := removeQuotations (← errorMessage[4]?)
             StyleError.unicodeVariant offending none
           | _ => none
+        | "ERR_IMPORTS" => some StyleError.importFormatting
         | _ => none
       match String.toNat? lineNumber with
       | some n => err.map fun e ↦ (ErrorContext.mk e n path)
@@ -268,6 +277,41 @@ also return the collection of all lines, changed as needed to fix the linter err
 abbrev TextbasedLinter := LinterOptions → Array String →
   Array (StyleError × ℕ) × (Option (Array String))
 
+/-- Check that public imports precede private imports, with a blank line between the two groups. -/
+public register_option linter.importFormatting : Bool := { defValue := false }
+
+/-- Check whether `public import` and private `import` declarations in a module are grouped in that
+order and separated by one blank line. The `meta` and `all` modifiers are ignored when determining
+the group. If needed, return an automatically formatted source file when it is safe to do so.
+
+The formatter uses the source-editing and parsed import/whitespace machinery behind
+`#norm_imports`, while retaining the order within each group and not removing redundant imports. -/
+def formatImports (source fileName : String) : IO (Option (ℕ × String)) := do
+  let inputCtx := Lean.Parser.mkInputContext source fileName
+  let (header, _, log) ← Lean.Parser.parseHeader inputCtx
+  if log.hasErrors || (ImportGraph.Lean.getModule header).isNone then
+    return none
+  let sourceImports := ImportGraph.headerToImportRefsWithWhitespace header
+  if !sourceImports.any (·.1.isExported) || !sourceImports.any (!·.1.isExported) then
+    return none
+  let imports := sourceImports.map fun imp ↦ (imp.1.toImport, imp.2)
+  let formatted := ImportGraph.Lean.Import.prettyWithWhitespaceGroupedByVisibility imports
+  let some edit := ImportGraph.Lean.Import.mkImportBlockEdit source sourceImports formatted
+    | return none
+  let fixed := edit.apply source
+  let lineNumber := (inputCtx.fileMap.toPosition edit.startPos).line
+  -- Refuse unsafe automatic edits, for example when a multi-line block comment cannot be carried
+  -- with its import by the whitespace representation. Returning the original source still makes
+  -- the linter report the violation.
+  let (fixedHeader, _, fixedLog) ← Lean.Parser.parseHeader <|
+    Lean.Parser.mkInputContext fixed fileName
+  let expectedImports := (sourceImports.filter (·.1.isExported) ++
+    sourceImports.filter (!·.1.isExported)).map (·.1.toImport)
+  let actualImports := (ImportGraph.Lean.headerToImportRefs fixedHeader).map (·.toImport)
+  if fixedLog.hasErrors || actualImports != expectedImports then
+    return some (lineNumber, source)
+  return some (lineNumber, fixed)
+
 /-! Definitions of the actual text-based linters. -/
 section
 
@@ -454,15 +498,15 @@ def lintFile (opts : LinterOptions) (path : FilePath) (exceptions : Array ErrorC
     changes_made := true
     errors := errors.push (ErrorContext.mk StyleError.windowsLineEnding 1 path)
   let lines := (replaced.splitOn "\n").toArray
+  -- A working copy of the lines in this file, modified by applying the auto-fixes.
+  let mut changed := lines
 
   -- We don't need to run any further checks on imports-only files.
-  if isImportsOnlyFile lines then
-    return (errors, if changes_made then some lines else none)
+  if isImportsOnlyFile changed then
+    return (errors, if changes_made then some changed else none)
 
   -- All further style errors raised in this file.
   let mut allOutput := #[]
-  -- A working copy of the lines in this file, modified by applying the auto-fixes.
-  let mut changed := lines
 
   for lint in allLinters do
     let (new_errors, changes) := lint opts changed
@@ -494,6 +538,19 @@ def lintFile (opts : LinterOptions) (path : FilePath) (exceptions : Array ErrorC
   -- Filter exceptions. Note: This list is not sorted. For github, this is fine.
   errors := errors.append
     (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone))
+
+  -- Apply import formatting after the line-based linters. This keeps their reported line numbers
+  -- tied to the source on disk even when regrouping imports adds or removes blank lines.
+  if getLinterValue linter.importFormatting opts then
+    let changedSource := "\n".intercalate changed.toList
+    if let some (lineNumber, fixed) ← formatImports changedSource path.toString then
+      let error := ErrorContext.mk StyleError.importFormatting lineNumber path
+      if error.find?_comparable exceptions |>.isNone then
+        errors := errors.push error
+        let fixedLines := (fixed.splitOn "\n").toArray
+        if fixedLines != changed then
+          changed := fixedLines
+          changes_made := true
   return (errors, if changes_made then some changed else none)
 
 /-- Lint a collection of modules for style violations.
@@ -525,7 +582,7 @@ def lintModules (opts : LinterOptions) (nolints : Array String) (moduleNames : A
   formatErrors allUnexpectedErrors style
   if allUnexpectedErrors.size > 0 then
     IO.eprintln s!"error: found {allUnexpectedErrors.size} new style error(s)! \
-      Try `lake exe lint-style --fix` to apply automatic fixes."
+      Rerun `lake exe lint-style` with `--fix` to apply automatic fixes."
   return numberErrorFiles
 
 /-- Verify that all modules are named in `UpperCamelCase` -/

MathlibTest/Linter/TextBased.lean

@@ -655,9 +655,49 @@ end showLinter
 
 /-! Tests for linters defined in `TextBased.lean`. -/
 section textBased
-section unicodeLinter
 
 open Mathlib.Linter.TextBased
+
+section importFormatting
+
+set_option linter.unusedTactic false in
+example : True := by
+  run_tac do
+    let source := "module\n\nimport B\npublic import C\npublic import A\nimport D\n\n#check Nat\n"
+    let expected :=
+      "module\n\npublic import C\npublic import A\n\nimport B\nimport D\n\n#check Nat\n"
+    let some (lineNumber, actual) ← formatImports source "Test.lean"
+      | throwError "Expected import formatting to change"
+    unless lineNumber == 3 do
+      throwError "Expected the import error on line 3, got line {lineNumber}"
+    unless actual == expected do
+      throwError "Unexpected import formatting output:\n{actual}"
+
+    let source := "module\n\npublic import A\n\nimport B\n\n#check Nat\n"
+    unless (← formatImports source "Test.lean").isNone do
+      throwError "Correctly grouped imports should be left unchanged"
+
+    let source := "module\n\nimport B\npublic meta import C\nimport all D\n" ++
+      "public import A\n\n#check Nat\n"
+    let expected := "module\n\npublic meta import C\npublic import A\n\nimport B\n" ++
+      "import all D\n\n#check Nat\n"
+    let some (_, actual) ← formatImports source "Test.lean"
+      | throwError "Expected meta and all imports to be grouped by visibility"
+    unless actual == expected do
+      throwError "Unexpected formatting with meta and all imports:\n{actual}"
+
+    let source := "module\n\nimport B /- trailing\ncontinued -/\n" ++
+      "public import A\n\n#check Nat\n"
+    let some (_, actual) ← formatImports source "Test.lean"
+      | throwError "Expected unsafe import formatting to still be reported"
+    unless actual == source do
+      throwError "Unsafe import formatting should be reported without an automatic fix"
+  trivial
+
+end importFormatting
+
+section unicodeLinter
+
 open Mathlib.Linter.TextBased.UnicodeLinter
 
 /- A character either does or doesn't have an abbreviation in the VSCode extension. -/
@@ -797,6 +837,10 @@ meta def ErrorContext.isValid_parse?_error_context (ec : ErrorContext) : Bool :=
   error := .semicolon,
   lineNumber := 1234, path := "Mathlib/Tactic/Measurability/Init.lean"}
 
+#guard ErrorContext.isValid_parse?_error_context {
+  error := .importFormatting,
+  lineNumber := 1234, path := "Mathlib/Tactic/Measurability/Init.lean"}
+
 #guard ErrorContext.isValid_parse?_error_context {
   error := .unwantedUnicode '\u1234',
   lineNumber := 1234, path:="./MYFILE.lean"}

docs/workflows.md

@@ -36,7 +36,7 @@ This is an overview of the most important triggers used by Mathlib CI. For a com
 ### The main CI pipelines above all use this reusable workflow for the base logic:
 | File  | Description |
 |---|---|
-| [`build_template.yml`](../.github/workflows/build_template.yml) | Reusable CI workflow (`workflow_call`) that performs Lean setup, build/test/lint steps, cache/artifact handling, and reporting. |
+| [`build_template.yml`](../.github/workflows/build_template.yml) | Reusable CI workflow (`workflow_call`) that performs Lean setup, build/test/lint steps, changed-file import-formatting checks, cache/artifact handling, and reporting. |
 
 ## Pull requests
 

lake-manifest.json

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7ad9f2e325aa6cec3dacaa97c2653a98032750eb",
+   "rev": "7d55631b042cb7d24f67f83a8a4b7c7b588a4e9b",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

scripts/README.md

@@ -227,7 +227,9 @@ to module `Foo.Bar` (no `srcDir` indirection).
 - `mk_all.lean`
   run via `lake exe mk_all`, regenerates the import-only files
   `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean` and `Counterexamples.lean`
-- `lint-style.lean`: style linters written in Lean. Run via `lake exe lint-style`.
+- `lint-style.lean`: style linters written in Lean. Run via `lake exe lint-style`. Pass `--imports`
+  to check public/private import grouping, `--only` to avoid traversing the named modules' imports,
+  and `--fix` to apply available fixes.
 - `check_title_labels.lean` verifies that a (non-WIP, non-draft) PR has a well-formed title.
   In the future, it may also check that a feature PR has a topic label.
 - `lint-bib.sh`

scripts/lint-style.lean

@@ -193,6 +193,10 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
     toOptions := ← getLakefileLeanOptions,
     linterSets := linter_sets%,
   }
+  let opts := if args.hasFlag "imports" then
+    { opts with toOptions := opts.toOptions.setBool `linter.importFormatting true }
+  else
+    opts
 
   let style : ErrorFormat := match args.hasFlag "github" with
     | true => ErrorFormat.github
@@ -250,11 +254,14 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   let pkgs := originModules.map (·.components.head!)
   Lean.initSearchPath (← Lean.findSysroot)
   let searchPath ← Lean.getSrcSearchPath
-  let allModuleNames ← originModules.flatMapM fun mod => do
-    let some file ← searchPath.findWithExt "lean" mod
-      | throw <| IO.userError s!"could not find module with name {mod}"
-    let imports := (← file.parseImports').filterInit.imports.map (·.module)
-    pure <| imports.filter (·.components.head! ∈ pkgs)
+  let allModuleNames ← if args.hasFlag "only" then
+    pure originModules
+  else
+    originModules.flatMapM fun mod => do
+      let some file ← searchPath.findWithExt "lean" mod
+        | throw <| IO.userError s!"could not find module with name {mod}"
+      let imports := (← file.parseImports').filterInit.imports.map (·.module)
+      pure <| imports.filter (·.components.head! ∈ pkgs)
 
   -- Read the `nolints` file, with manual exceptions for the linter.
   -- NB. We pass these lints to `lintModules` explicitly to prevent cache invalidation bugs:
@@ -290,6 +297,8 @@ def lintStyle : Cmd := `[Cli|
     github;     "Print errors in a format suitable for github problem matchers\n\
                  otherwise, produce human-readable output"
     fix;        "Automatically fix the style error, if possible"
+    imports;    "Check the formatting of public and private import groups"
+    only;       "Lint only the named modules, rather than their transitive imports"
 
   ARGS:
     ...modules : String; "Which modules, and their imports, will be linted.\n\