[Merged by Bors] - chore: format imports by thorimur · Pull Request #44513 · leanprover-community/mathlib4

thorimur · 2026-10-05T08:04:50Z

This PR formats imports throughout Mathlib by grouping imports into visibility blocks separated by a newline (public import/import/import all), then sorting within each block by meta/(non-meta), and then sorting alphabetically. This uses scripts/runSkimmer.sh to apply the suggestions generated in #44507. (Files outside of Mathlib/ are not touched.)

This was discussed among reviewers in the mathlib reviewers channel on Zulip in the topic "linting imports", as well as incidentally in the latter part of this topic.

(Note: this does not format Mathlib.Tactic.Common yet, since that file makes deliberate choices about import ordering.)

(Note for regeneration purposes: this technically used a transient skimmer lakefile dependency and lake build Mathlib:applyCurrentTryThis instead of the script per se, due to the header linter's sensitivity to the package directory and implementation details of the runSkimmer script. This may be fixed in the future.)

github-actions · 2026-10-05T08:06:35Z

PR summary 2065829e8a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

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

+0 new declarations
−0 removed declarations

No declaration differences.

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

Current commit 2065829e8a
Reference commit 49fd9dee36

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

thorimur · 2026-10-05T08:13:24Z

!bench

leanprover-radar · 2026-10-05T08:13:42Z

Benchmark results for 6c1305e against be31cde are in. No significant results found. @thorimur

✅ build//instructions: -13.9G (-0.01%)

Medium changes (2✅, 1🟥)

✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -1.2G (-2.61%)
🟥 build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order//instructions: +1.7G (+1.78%)
✅ build/module/Mathlib.Topology.Sets.CompactOpenCovered//instructions: -1.3G (-3.56%)

Small changes (8✅, 2🟥)

✅ build/module/Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso//instructions: -100.5M (-4.80%) (reduced significance based on absolute threshold)
✅ build/module/Mathlib.Algebra.Torsor.Basic//instructions: -274.5M (-1.88%)
🟥 build/module/Mathlib.AlgebraicGeometry.ZariskisMainTheorem//instructions: +902.4M (+1.97%)
✅ build/module/Mathlib.Analysis.Meromorphic.FactorizedRational//instructions: -517.0M (-2.15%)
✅ build/module/Mathlib.Analysis.Meromorphic.Order//instructions: -668.5M (-0.99%)
✅ build/module/Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs//instructions: -583.3M (-1.42%)
🟥 build/module/Mathlib.Topology.Algebra.Valued.ValuedField//instructions: +1.6G (+3.55%)
✅ build/module/Mathlib.Topology.Covering.FundamentalGroupCircle//instructions: -160.4M (-2.49%) (reduced significance based on absolute threshold)
✅ build/module/Mathlib.Topology.Sets.OpenCover//instructions: -275.5M (-4.39%)
✅ build/module/Mathlib.Topology.Sets.Opens//instructions: -660.8M (-3.71%)

kim-em · 2026-10-05T11:52:17Z

bors merge

mathlib-bors · 2026-10-05T11:52:21Z

👎 Rejected by label

kim-em · 2026-10-05T11:52:53Z

bors merge

kim-em · 2026-10-05T12:00:11Z

bors r-

mathlib-bors · 2026-10-05T12:00:14Z

Bors build canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

grunweg · 2026-10-05T12:02:05Z

I think this policy decision should be discussed a little longer:
bors r-

grunweg · 2026-10-05T12:02:44Z

(I do personally think this policy is reasonable, but I don't see the urgency of merging this just now, especially if the PR can be auto-regenerated.)

fpvandoorn · 2026-10-08T09:05:57Z

This has huge support among reviewers, so this LGTM.

bors d+

mathlib-bors · 2026-10-08T09:06:00Z

✌️ thorimur can now approve this pull request until 2026-10-22 09:05 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, Wanted/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean, Wanted.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

thorimur

(Sorry for the force push, it was the easiest way to regenerate :) )

thorimur · 2026-10-09T05:08:34Z

!bench

leanprover-radar · 2026-10-09T05:09:02Z

Benchmark results for 27775b5 against 49fd9de are in. There are significant results. @thorimur

✅ build//instructions: -6.1G (-0.00%)

Medium changes (2✅, 2🟥)

✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -1.2G (-2.73%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order//instructions: +1.7G (+1.82%)
🟥 build/module/Mathlib.Topology.Algebra.Valued.ValuedField//instructions: +1.6G (+3.59%)
✅ build/module/Mathlib.Topology.Sets.CompactOpenCovered//instructions: -1.2G (-3.59%)

Small changes (55✅, 35🟥)

✅ build/module/Mathlib.Algebra.DirectSum.Ring//instructions: -123.5M (-0.44%)
✅ build/module/Mathlib.Algebra.Field.NegOnePow//instructions: -21.5M (-0.66%)
✅ build/module/Mathlib.Algebra.Field.Subfield.Basic//instructions: -129.3M (-0.65%)
✅ build/module/Mathlib.Algebra.Order.Floor.Defs//instructions: -102.9M (-1.06%)
✅ build/module/Mathlib.Algebra.Order.Ring.Abs//instructions: -82.3M (-0.67%)
✅ build/module/Mathlib.Algebra.Order.Ring.Defs//instructions: -43.2M (-0.81%)
🟥 build/module/Mathlib.Algebra.Polynomial.Degree.CardPowDegree//instructions: +170.1M (+3.13%)
✅ build/module/Mathlib.Algebra.Ring.Subring.Pointwise//instructions: -77.4M (-1.16%)
✅ build/module/Mathlib.Algebra.Ring.Subsemiring.Pointwise//instructions: -45.7M (-0.76%)
🟥 build/module/Mathlib.Algebra.Star.Module//instructions: +83.9M (+0.62%)
✅ build/module/Mathlib.Algebra.Torsor.Basic//instructions: -275.8M (-1.98%) (reduced significance based on absolute threshold)
✅ build/module/Mathlib.AlgebraicGeometry.Cover.QuasiCompact//instructions: -130.1M (-0.69%)
✅ build/module/Mathlib.AlgebraicGeometry.Cover.Sigma//instructions: -147.8M (-2.32%) (reduced significance based on absolute threshold)
✅ build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic//instructions: -103.9M (-0.60%)
✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.Constructors//instructions: -188.3M (-0.81%)
✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.LocalClosure//instructions: -146.4M (-1.88%)
✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap//instructions: -388.2M (-3.39%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.AlgebraicGeometry.ZariskisMainTheorem//instructions: +919.9M (+2.05%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic//instructions: +314.8M (+1.62%) (reduced significance based on absolute threshold)
✅ build/module/Mathlib.Analysis.Analytic.IteratedFDeriv//instructions: -92.1M (-0.30%)
and 70 more

thorimur · 2026-10-09T05:14:52Z

What should we do about Mathlib.Tactic.Common? It has comments describing the order of imports. Do we leave the file as-is? Or do we just delete those comments?

I've tentatively reverted the changes to Mathlib.Tactic.Common so that this PR now leaves it unchanged. Given that this is a conservative choice rather than an "active" one, I'm going to bors r+ so that this PR doesn't rot. :)

thorimur · 2026-10-09T05:15:28Z

!bench

leanprover-radar · 2026-10-09T05:15:46Z

Benchmark results for 2065829 against 49fd9de are in. There are significant results. @thorimur

✅ build//instructions: -8.8G (-0.01%)

Medium changes (2✅, 2🟥)

✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -1.2G (-2.74%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order//instructions: +1.7G (+1.82%)
🟥 build/module/Mathlib.Topology.Algebra.Valued.ValuedField//instructions: +1.6G (+3.58%)
✅ build/module/Mathlib.Topology.Sets.CompactOpenCovered//instructions: -1.2G (-3.59%)

Small changes (55✅, 34🟥)

🟥 build/module/Aesop.Stats.Extension//instructions: +4.8M (+0.43%)
✅ build/module/Mathlib.Algebra.DirectSum.Ring//instructions: -124.3M (-0.44%)
✅ build/module/Mathlib.Algebra.Field.NegOnePow//instructions: -17.5M (-0.54%)
✅ build/module/Mathlib.Algebra.Field.Subfield.Basic//instructions: -130.4M (-0.65%)
✅ build/module/Mathlib.Algebra.Order.Floor.Defs//instructions: -104.1M (-1.07%)
✅ build/module/Mathlib.Algebra.Order.Ring.Abs//instructions: -82.0M (-0.67%)
✅ build/module/Mathlib.Algebra.Order.Ring.Defs//instructions: -43.0M (-0.81%)
🟥 build/module/Mathlib.Algebra.Polynomial.Degree.CardPowDegree//instructions: +170.3M (+3.13%)
✅ build/module/Mathlib.Algebra.Ring.Subring.Pointwise//instructions: -78.0M (-1.17%)
✅ build/module/Mathlib.Algebra.Ring.Subsemiring.Pointwise//instructions: -46.8M (-0.78%)
🟥 build/module/Mathlib.Algebra.Star.Module//instructions: +84.0M (+0.62%)
✅ build/module/Mathlib.Algebra.Torsor.Basic//instructions: -273.7M (-1.96%) (reduced significance based on absolute threshold)
✅ build/module/Mathlib.AlgebraicGeometry.Artinian//instructions: -49.2M (-0.57%)
✅ build/module/Mathlib.AlgebraicGeometry.Cover.QuasiCompact//instructions: -135.5M (-0.71%)
✅ build/module/Mathlib.AlgebraicGeometry.Cover.Sigma//instructions: -153.0M (-2.40%) (reduced significance based on absolute threshold)
✅ build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic//instructions: -99.8M (-0.57%)
✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.Constructors//instructions: -196.1M (-0.85%)
✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.LocalClosure//instructions: -152.6M (-1.96%)
✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap//instructions: -392.6M (-3.43%) (reduced significance based on absolute threshold)
🟥 build/module/Mathlib.AlgebraicGeometry.ZariskisMainTheorem//instructions: +921.7M (+2.05%) (reduced significance based on absolute threshold)
and 69 more

thorimur · 2026-10-09T06:00:12Z

Given that this PR will easily rot and is a tad inconvenient to generate, I'm going to make the choice to not format Mathlib.Tactic.Common given its comments about import ordering, with the rationale that an unreviewed non-change is much more acceptable in these circumstances than an unreviewed change. :)

bors r+

This PR formats imports throughout Mathlib by grouping imports into visibility blocks separated by a newline (`public import`/`import`/`import all`), then sorting within each block by `meta`/(non-meta), and then sorting alphabetically. This uses `scripts/runSkimmer.sh` to apply the suggestions generated in #44507. (Files outside of `Mathlib/` are not touched.) This was discussed among reviewers in the mathlib reviewers channel on Zulip in the topic "linting imports", as well as incidentally in the latter part of [this topic](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/chore.3A.20demote.20public.20imports.20.2343918/with/625621866). (Note: this does not format Mathlib.Tactic.Common yet, since that file makes deliberate choices about import ordering.) (Note for regeneration purposes: this technically used a transient skimmer lakefile dependency and `lake build Mathlib:applyCurrentTryThis` instead of the script per se, due to the header linter's sensitivity to the package directory and implementation details of the `runSkimmer` script. This may be fixed in the future.) Co-authored-by: Kim Morrison <kim@tqft.net>

mathlib-bors · 2026-10-09T07:21:22Z

Pull request successfully merged into master.

Build succeeded:

Most conflicts come from master's regrouping of public and private imports (#44512, #44513): resolved by taking master's import layout and reapplying this PR's meta/removal changes line by line. - Mathlib/Init.lean: keep master's new `Batteries.Tactic.Alias` import and `Linter.DeclType` (which bundles the instance linters, #44436), the latter as a `public meta import`. - Mathlib/Data/Ineq.lean: drop the duplicate `ToFormat` instance as master did (#44383); the parsing functions stay moved to `Mathlib.Tactic.Ineq`. - Control/Monad/{Basic,Cont}, Lean/Expr/Basic, FieldSimp, Linarith/Lemmas, LinearCombination/Lemmas: re-add this PR's new imports (`Batteries.Data.Except`, `Lean.ProjFns`, `Lean.Structure`, `Mathlib.Tactic.Ineq`) in master's public import group. - Mathlib/Tactic/Push.lean: drop the `public import Lean.Elab.ConfigEval` that git's auto-merge reintroduced. - Mathlib/Tactic/Echelon/Core.lean: master added `public import Qq` to this `public meta section` file; make it `public meta import Qq`. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

github-actions Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 5, 2026

kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 5, 2026

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Oct 5, 2026

mathlib-bors Bot removed the ready-to-merge This PR has been sent to bors. label Oct 5, 2026

grunweg added the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Oct 5, 2026

mathlib-bors Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 8, 2026

chore: skimmer

a412387

thorimur force-pushed the format-imports branch from a949cff to a412387 Compare October 9, 2026 04:43

thorimur commented Oct 9, 2026

View reviewed changes

test: update hint suggestions after import reordering

27775b5

chore: do not format

2065829

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Oct 9, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Oct 9, 2026

mathlib-bors Bot changed the title ~~chore: format imports~~ [Merged by Bors] - chore: format imports Oct 9, 2026

mathlib-bors Bot closed this Oct 9, 2026

mathlib-bors Bot removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 9, 2026

thorimur mentioned this pull request Oct 12, 2026

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

Open

2 tasks done

Conversation

thorimur commented Oct 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Oct 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2065829e8a

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

thorimur commented Oct 5, 2026

Uh oh!

leanprover-radar commented Oct 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kim-em commented Oct 5, 2026

Uh oh!

mathlib-bors Bot commented Oct 5, 2026

Uh oh!

kim-em commented Oct 5, 2026

Uh oh!

kim-em commented Oct 5, 2026

Uh oh!

mathlib-bors Bot commented Oct 5, 2026

Uh oh!

grunweg commented Oct 5, 2026

Uh oh!

grunweg commented Oct 5, 2026

Uh oh!

fpvandoorn commented Oct 8, 2026

Uh oh!

mathlib-bors Bot commented Oct 8, 2026

Uh oh!

thorimur left a comment

Choose a reason for hiding this comment

Uh oh!

thorimur commented Oct 9, 2026

Uh oh!

leanprover-radar commented Oct 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thorimur commented Oct 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thorimur commented Oct 9, 2026

Uh oh!

leanprover-radar commented Oct 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thorimur commented Oct 9, 2026

Uh oh!

mathlib-bors Bot commented Oct 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

thorimur commented Oct 5, 2026 •

edited

Loading

github-actions Bot commented Oct 5, 2026 •

edited

Loading

leanprover-radar commented Oct 5, 2026 •

edited

Loading

leanprover-radar commented Oct 9, 2026 •

edited

Loading

thorimur commented Oct 9, 2026 •

edited

Loading

leanprover-radar commented Oct 9, 2026 •

edited

Loading