feat(Linter): check import formatting in modified files

[kim-em]

Check that public imports precede private imports, with a blank line between the groups. The text-based linter reports violations and supports automatic fixes through lake exe lint-style --imports --fix --only <modules>.

The formatter groups solely by public/private visibility, preserving meta and all modifiers and the order within each group. It reuses ImportGraph's import parsing, whitespace handling, and source-edit API behind #norm_imports, without removing redundant imports. Unsafe edits, such as splitting a multiline trailing comment, are reported without an automatic fix.

There are 2,076 violations in the scanned Mathlib tree. CI checks only Mathlib files changed relative to the default branch. The separate source-only cleanup is #44512.

New CLI flags:

• --imports enables the import-formatting rule.
• --only checks the named modules without their transitive imports.
• --fix applies safe automatic edits.

Validation: targeted linter tests and executable build, full-tree violation count, exact changed-file workflow simulation, workflow YAML parsing, and git diff --check.

---

• depends on: feat: expose import block source edits import-graph#172

[github-actions]

PR summary 7316203f16

Import changes exceeding 2%

%	File
+2.06%	Mathlib.Tactic.Linter.TextBased

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.TextBased	97	99	+2 (+2.06%)

Import changes for all files

Files	Import difference
Mathlib.Tactic.Linter.TextBased Mathlib.Tactic	2

---

Declarations diff (regex)

+ formatImports

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 7316203).

• +1 new declarations
• −0 removed declarations

+Mathlib.Linter.TextBased.linter.importFormatting

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 7316203f16
Reference commit 7d6757bc18

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

• .github/workflows/build_template.yml

[kim-em]

This now depends on leanprover-community/import-graph#172, which exposes the shared source-edit API used by this linter and #norm_imports. Please merge that prerequisite first; this PR remains targeted at master.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: expose import block source edits import-graph#172
  By Dependent Issues (🤖). Happy coding!

[kim-em]

Closing in favour of #44507.