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

[thorimur]

This PR enables the header linter to reformat imports to match the style guide. It logs an interactive suggestion in the event that imports are not formatted correctly. (The try-this suggestion preserves comments above and inline with each import.)

This is only active in the module system, and currently only for files in Mathlib (and test files).

This linter is on by default whenever linter.style.header is on, but may be turned off separately from the rest of the header linter by writing set_option linter.style.header.imports false just after the import block. (Note: while we're here, we also allow linter.style.header.license to be set just after the import block for consistency.)

The suggestion does not "normalize" imports as #norm_imports does, i.e. eliminate redundancy among imports. It only makes sure that the imports are ordered and grouped correctly.

This also fixes some unformatted imports that crept in since #44513.

---

• depends on: fix: sort names alphabetically in Imports.Pretty import-graph#171
• depends on: [Merged by Bors] - chore: format imports #44513

[github-actions]

PR summary f70a744f14

Import changes exceeding 2%

%	File
+11.11%	Mathlib.Tactic.Linter.Header

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.Header	9	10	+1 (+11.11%)
Mathlib.Tactic.Common	376	377	+1 (+0.27%)
Mathlib.CategoryTheory.Functor.Derived.RightDerivedCompositionCommShift	662	663	+1 (+0.15%)
Mathlib.CategoryTheory.Linear.Yoneda	1014	1015	+1 (+0.10%)
Mathlib.LinearAlgebra.PiTensorProduct.Generators	1227	1228	+1 (+0.08%)
Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits	1570	1571	+1 (+0.06%)
Mathlib.Algebra.Lie.Solvable	1679	1680	+1 (+0.06%)
Mathlib.Analysis.LocallyConvex.Asymptotics	1770	1771	+1 (+0.06%)
Mathlib.Geometry.Manifold.VectorBundle.ContinuousAlternatingMap	2430	2431	+1 (+0.04%)
Mathlib.Analysis.Normed.Algebra.GelfandFormula	2932	2933	+1 (+0.03%)
Mathlib.MeasureTheory.Measure.TotalVariation.Basic	3010	3011	+1 (+0.03%)
Mathlib.NumberTheory.NumberField.AdeleRing	3408	3409	+1 (+0.03%)

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 8645 files with changed transitive imports taking up over 377244 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

+ formatImports
- ImportRef
- ImportRef.getIdent
- headerToImportRefs

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 -- stale, waiting for the new build)

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

• +1 new declarations
• −0 removed declarations

+Mathlib.Linter.linter.style.header.imports

---

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

Current commit f70a744f14
Reference commit e3e75e8614

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).

[kim-em]

Could we validate the proposed replacement before offering the code action? A multiline block comment starting after an import can be split when whitespace is reassigned, even when errs.isEmpty is true.

For example, formatting this header:

module

import B /- trailing
continued -/
public import A

currently produces:

module

continued -/
public import A

import B /- trailing

I reproduced this against ImportGraph's merged main at d058217, using the same headerToImportRefsWithWhitespace / prettyWithSourceWhitespace path used by mkImportSuggestionMessage. The formatter reports FormatErrors.isEmpty: true: the opening /- trailing stays with import B, while continued -/ moves with public import A. Applying the suggestion therefore corrupts a valid file. Returning early only when errs is nonempty would not catch it.

A defensive check would apply the candidate edit to the source, reparse the header, and require that it contains exactly the expected imports in the intended order, with all modifiers preserved. Checking only the parser's error log is insufficient: in this example parseHeader returns no errors but an empty import list because continued ends the header. If validation fails, we can still warn about formatting, but omit the automatic edit. Ideally the comment handling itself is fixed in ImportGraph too.

Could we add this as a regression test? #44503 already checks the reparsed import list before applying automatic fixes.

[thorimur]

Nice catch! I'll address this when I'm back from PTO, but I wanted to mention that I suspect this also uncovers an issue in core's Lean.Syntax.updateLeading(Aux), on which this formatting/whitespace-splitting relies! 👀

(Or maybe it's just an API gap. It's possible that updateLeading is not even attempting to have well-formed whitespace, and is indeed just looking for that trailing newline.)

[thorimur]

My feeling is that while this is important, it is also the case that as far as this PR goes, it is more important to keep Mathlib from drifting from the import style convention than to wait for the necessary upstream (ImportGraph) changes to fix this, especially given that it's likely quite a rare occurrence. (Nor is it worth the code complexity that would be necessary to address it here.)

I do think this should be fixed in import graph, though; I now have some not-yet-PR'd code that performs the defensive reparsing. Parsing the comment itself is a bit finicky but there are options I'm considering :) In the meantime if you'd like to make an issue on import graph, you could assign me to it! :)

But, all in all, I think the benefit is worth leaving this edge case is unhandled in this PR.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[thorimur]

!bench

[leanprover-radar]

Benchmark results for 60af689 against fad3406 are in. There are significant results. @thorimur

• 🟥 build//instructions: +33.9G (+0.03%)

Small changes (43✅, 104🟥)

• ✅ build/module/Mathlib.Algebra.Divisibility.Finite//instructions: -14.2M (-0.57%)
• 🟥 build/module/Mathlib.Algebra.Expr//instructions: +3.6M (+0.21%)
• 🟥 build/module/Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero//instructions: +3.8M (+0.16%)
• ✅ build/module/Mathlib.Algebra.Homology.ShortComplex.QuasiIso//instructions: -140.8M (-2.17%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Algebra.Homology.ShortComplex.Retract//instructions: -13.6M (-0.42%)
• 🟥 build/module/Mathlib.Algebra.LinearRecurrence//instructions: +198.1M (+2.12%) (reduced significance based on absolute threshold)
• 🟥 build/module/Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset//instructions: +22.0M (+0.60%)
• 🟥 build/module/Mathlib.Algebra.Order.Group.Action.End//instructions: +11.4M (+0.43%)
• 🟥 build/module/Mathlib.Algebra.Order.Ring.Units//instructions: +25.3M (+0.79%) (reduced significance based on absolute threshold)
• 🟥 build/module/Mathlib.Algebra.Ring.BooleanRing//instructions: +75.2M (+0.50%)
• ✅ build/module/Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic//instructions: -27.8M (-0.37%)
• 🟥 build/module/Mathlib.AlgebraicGeometry.Cover.Sigma//instructions: +20.3M (+0.33%)
• ✅ build/module/Mathlib.AlgebraicGeometry.EffectiveEpi//instructions: -46.4M (-0.53%)
• 🟥 build/module/Mathlib.AlgebraicGeometry.Morphisms.LocalIso//instructions: +38.1M (+0.74%)
• ✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale//instructions: -38.0M (-0.61%)
• 🟥 build/module/Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy//instructions: +61.5M (+0.31%)
• 🟥 build/module/Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp//instructions: +10.2M (+0.33%)
• 🟥 build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note//instructions: +3.8M (+0.23%)
• ✅ build/module/Mathlib.Analysis.Calculus.BumpFunction.Normed//instructions: -59.0M (-0.57%)
• ✅ build/module/Mathlib.Analysis.Calculus.LogDerivUniformlyOn//instructions: -192.8M (-3.85%) (reduced significance based on absolute threshold)
• and 127 more

[mathlib-dependent-issues]

This PR/issue depends on:

• fix: sort names alphabetically in Imports.Pretty import-graph#171
• [Merged by Bors] - chore: format imports #44513
  By Dependent Issues (🤖). Happy coding!

[grunweg]

There's one more drifting file. I'll take a first review look (hopefully) tomorrow. Thanks for automating away the bikeshedding!

[thorimur]

This is drifting basically as soon as I fix it, so I think I'm just going to wait for a review instead of keeping iton the queue proper if that's alright :)

[grunweg]

I have a this a more thorough review and have only minor questions. Thanks for doing this!

[thorimur]

Oof, it seems like #43912 has introduced a lot of violations due to unlucky timing.

I think at this point I either ought to (1) make skimmer work as-is with the header linter (the header linter does some shenanigans with the current working directory, and skimmer is run from scripts/, so to get it to work previously I had to add it as a lake dependency), either by refining the header linter's inLibraryRoot logic or changing skimmer or (2) providing the text-based version