[Merged by Bors] - feat: make the `dupNamespace` linter catch any duplicate namespace(s) by grunweg · Pull Request #39793 · leanprover-community/mathlib4

grunweg · 2026-05-24T21:29:18Z

Before this PR, the dupNamespace linter would only flag a namespace as duplicate if it was repeated in two consecutive positions: Foo.Foo.bar would be linted, but neither Foo.Bar.Foo.Bar.baz nor Foo.Bar.Foo.Baz.baz would be (even though they are very likely unintentional).

Strengthen the linter check, to error if any namespace component is duplicated.
This has few false positives (which we manually annotate), but catches many pre-existing
cases where the duplication was clearly unintentional and undesirable.

Most of the mathlib adaptation was done in #39794.

depends on: [Merged by Bors] - fix: decls with a non-consecutive duplicate namespace #39794

github-actions · 2026-05-24T21:30:39Z

PR summary 2e7d27597d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.Lint	5	4	-1 (-20.00%)

Import changes for all files

Files	Import difference
`Mathlib.Tactic.Linter.Lint`	-1

Declarations diff (regex)

+ Bar.Foo.Foo
+ Foo.Bar.Baz.Hoge.Foo.Bar.Baz.az
+ Foo.Bar.Baz.Hoge.Foo.Bar.baz
+ Foo.Bar.Baz.Hoge.Foo.Baz.baz
+ Foo.Bar.Foo.Bar.baz
+ Foo.Bar.Foo.baz
+ Foo.Bar.Foo.baz'
+ Foo.Bar.baz'
+ Foo.Foo
+ Foo.Foo.Bar
+ Foo.Foo.Bar.Baz.hoge
+ Foo.Foos.Bar.Baz
+ Subgroup.AddSubgroup.foo
+ pullback.desc'
- CategoryTheory.Limits.pullback.desc'
- Distribution.IsVanishingOn.smulLeftCLM
- Distribution.dsupport_smulLeftCLM_subset

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

+3 new declarations
−3 removed declarations

-CategoryTheory.Limits.CategoryTheory.Limits.pullback.desc'
+CategoryTheory.Limits.pullback.desc'
+Distribution.IsVanishingOn.smulLeftCLM
-Distribution.TemperedDistribution.Distribution.dsupport_smulLeftCLM_subset
-Distribution.TemperedDistribution.IsVanishingOn.Distribution.IsVanishingOn.smulLeftCLM
+Distribution.dsupport_smulLeftCLM_subset

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 2e7d27597d
Reference commit b4b33fa6e8

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

One thing outside the diff: the module docstring at L67–70 and the option docstring at L74–77 both still say "at least twice consecutively" and use Nat.One.Nat as the negative example, but after this PR Nat.One.Nat does warn. Both need updating.

kim-em · 2026-05-25T15:13:37Z

-        | continue
-      Linter.logLint linter.dupNamespace id
-        m!"The namespace '{dup}' is duplicated in the declaration '{declName}'"
+      if !nm.Nodup then


Redundant if you match on the computed list directly: | [] => continue | [ns] => … | dups => …. Avoids the extra O(n²) Nodup pass and reads more directly.

I actually think the previous logic was more readable. Now, the error message and emitting the linter warning is spread across two similar cases. I'm also not sure if the performance difference matters.
I've changed it anyway (as I don't feel strongly either).

mathlib-dependent-issues · 2026-05-25T16:55:23Z

This PR/issue depends on:

~~[Merged by Bors] - fix: decls with a non-consecutive duplicate namespace #39794~~
By Dependent Issues (🤖). Happy coding!

SnirBroshi · 2026-05-25T17:47:41Z

Now that the dependency was merged, we need to turn off the linter (set_option linter.dupNamespace false in) in 50 places:

These 45 deprecated aliases

Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective
Algebra.FormallyEtale.Algebra.FormallyEtale.of_restrictScalars
Algebra.TensorProduct.Algebra.TensorProduct.commRight_symm_tmul
Bundle.Trivialization.Bundle.Trivialization.mdifferentiable
CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup
CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup_apply
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.classifier
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.hasTerminal
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.homEquiv_eq
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_hom_left_comp
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_comp
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.iso_inv_left_π
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.isoΩ₀
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.isPullback
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.isTerminalΩ₀
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.uniq
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.π
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.χ
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.χ₀
CategoryTheory.SubobjectRepresentableBy._root.CategoryTheory.Classifier.SubobjectRepresentableBy.Ω₀
Equiv.Set.Equiv.strictMono_setCongr
Filter.Germ.Filter.Tendsto.congr_germ
LinearMap.IsSymmetric.LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute
Module.Finite.Module.finite_shrink
Module.Free.Module.free_shrink
NumberField.HeightOneSpectrum.NumberField.instNormedFieldValuedAdicCompletion
NumberField.HeightOneSpectrum.NumberField.instRankOneAdicCompletion
NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal
NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv
NumberField.InfinitePlace.NumberField.InfinitePlace.fintype
Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial
Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial
Set.FiniteExhaustion.Set.nonempty_finiteExhaustion_iff
Submonoid.IsUnit.Submonoid.coe_inv

and CategoryTheory.Bicategory.Adj.Bicategory.{associator/leftUnitor/rightUnitor/whiskerLeft/whiskerRight}.

(btw Joël said these shouldn't be used directly so we could try inlining them into the Bicategory instance below them)

grunweg · 2026-05-25T21:21:39Z

Thanks for the helpful review. (Indeed, I had not made a careful pass over this code yet.) I have acted on most comments, and also fixed a pre-existing outdated line in the doc-string.

I just wonder: did you just use an LLM to review my PR? Some comments read a bit like that.

grunweg · 2026-05-25T21:32:08Z

@SnirBroshi Good point. If you'd like to do this, be my guest (to e.g. make a PR into this branch)! Otherwise, I'll probably do so tomorrow.

SnirBroshi · 2026-05-26T02:19:06Z

If you'd like to do this, be my guest (to e.g. make a PR into this branch)

grunweg#7
I had to merge master first so it shows a bunch of commits, but they should disappear from the diff if you merge master yourself. The commit is grunweg@bfa755e.

grunweg · 2026-05-27T13:06:15Z

@SnirBroshi I just merged master... do you mind rebasing your PR on top of this one? Then I'll be happy to merge it!

SnirBroshi · 2026-05-27T20:42:21Z

@grunweg Done!

joneugster

Thanks, this is a good addition to the linter!

- update documentation (including an outdated comment about auto-generated names; there is now a test which verifies this is false), - print multiple namespaces more nicely, - inline duplicate checking: List.Nodup is currently quadratic; let's avoid an additional pass over the full list. It is slightly less readable, but perhaps the performance difference is worth it...

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>

thorimur · 2026-06-17T15:18:38Z

This looks good to me, thanks! :) I've also checked that every set_option is followed by an in. :)

maintainer merge

github-actions · 2026-06-17T15:19:21Z

🚀 Pull request has been placed on the maintainer queue by thorimur.

grunweg · 2026-06-17T15:42:19Z

I've also checked that every set_option is followed by an in. :)

We do have some linting for that, right? (I haven't checked if it would have caught this one. Perhaps it should?)

…nprover-community#40213) The Scheme.Modules namespace was duplicated in the declaration. Found by the strengthening the `dupNamespace` linter in leanprover-community#39793.

…0390) The old deprecation did not do what it was supposed to, because it duplicate the `NumberField.Units` namespace. This is an oversight from leanprover-community#40239. Found by the linter in leanprover-community#39793. Since that PR is just two days old, I am fixing the deprecation instead of adding an additional one.

adomani · 2026-07-01T22:09:09Z

Thanks!

There are a couple of extra exceptions, I think.

bors d+

mathlib-bors · 2026-07-01T22:09:12Z

✌️ grunweg can now approve this pull request until 2026-07-15 22:09 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/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.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.

The PR added deprecated aliases, but in a wrong namespace: this meant the original declarations did not actually get deprecated (and had in fact duplicated namespaces in their name). Fix the deprecation. As these landed just 24 hours ago, we don't deprecate the deprecations. Also update the deprecation date to when the PR was actually merged.

…tion The deprecation accidentally duplicated declaration namespaces, meaning it was never effective. This is confirmed by the declarations diff on the PR back then. Fix it.

grunweg · 2026-07-01T22:53:23Z

Thanks! The latest linter run caught two broken deprecations, so this is great! The Lean-based declaration diff in the summary comment is extremely helpful here, by the way.

mathlib-auto-merge · 2026-07-01T23:47:00Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

…#39793) Before this PR, the `dupNamespace` linter would only flag a namespace as duplicate if it was repeated in two consecutive positions: `Foo.Foo.bar` would be linted, but neither `Foo.Bar.Foo.Bar.baz` nor `Foo.Bar.Foo.Baz.baz` would be (even though they are very likely unintentional). Strengthen the linter check, to error if any namespace component is duplicated. This has few false positives (which we manually annotate), but catches many pre-existing cases where the duplication was clearly unintentional and undesirable. Most of the mathlib adaptation was done in #39794. Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

mathlib-bors · 2026-07-02T00:40:02Z

Pull request successfully merged into master.

Build succeeded:

…amespace` linter (leanprover#14249) This PR extends `dupNamespace` linter to allow users to opt-in via `linter.extra.dupNamespace.consecutiveOnly` option to check non-consecutive repeated usages of namespace components. By default, only consecutive ones are checked. Opting in for non-consecutive checks matches the behaviour introduced in [mathlib4#39793](leanprover-community/mathlib4#39793).

…leanprover-community#39793) Before this PR, the `dupNamespace` linter would only flag a namespace as duplicate if it was repeated in two consecutive positions: `Foo.Foo.bar` would be linted, but neither `Foo.Bar.Foo.Bar.baz` nor `Foo.Bar.Foo.Baz.baz` would be (even though they are very likely unintentional). Strengthen the linter check, to error if any namespace component is duplicated. This has few false positives (which we manually annotate), but catches many pre-existing cases where the duplication was clearly unintentional and undesirable. Most of the mathlib adaptation was done in leanprover-community#39794. Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

…amespace` linter (leanprover#14249) This PR extends `dupNamespace` linter to allow users to opt-in via `linter.extra.dupNamespace.consecutiveOnly` option to check non-consecutive repeated usages of namespace components. By default, only consecutive ones are checked. Opting in for non-consecutive checks matches the behaviour introduced in [mathlib4#39793](leanprover-community/mathlib4#39793).

…leanprover-community#39793) Before this PR, the `dupNamespace` linter would only flag a namespace as duplicate if it was repeated in two consecutive positions: `Foo.Foo.bar` would be linted, but neither `Foo.Bar.Foo.Bar.baz` nor `Foo.Bar.Foo.Baz.baz` would be (even though they are very likely unintentional). Strengthen the linter check, to error if any namespace component is duplicated. This has few false positives (which we manually annotate), but catches many pre-existing cases where the duplication was clearly unintentional and undesirable. Most of the mathlib adaptation was done in leanprover-community#39794. Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

grunweg added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-linter Linter labels May 24, 2026

SnirBroshi reviewed May 24, 2026

View reviewed changes

Comment thread Mathlib/Tactic/Linter/Lint.lean Outdated

SnirBroshi mentioned this pull request May 24, 2026

[Merged by Bors] - fix: decls with a non-consecutive duplicate namespace #39794

Closed

SnirBroshi reviewed May 24, 2026

View reviewed changes

Comment thread Mathlib/Tactic/Linter/Lint.lean Outdated

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 25, 2026

kim-em reviewed May 25, 2026

View reviewed changes

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 25, 2026

grunweg changed the title ~~feat: check for larger overlap windows in the dupNamespace linter~~ feat: make the dupNamespace linter catch any duplicate namespace(s) May 25, 2026

grunweg removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 27, 2026

mathlib-triage Bot assigned thorimur May 29, 2026

joneugster reviewed May 29, 2026

View reviewed changes

Comment thread Mathlib/Tactic/Linter/Lint.lean Outdated

Comment thread Mathlib/Tactic/Linter/Lint.lean Outdated

Comment thread Mathlib/Tactic/Linter/Lint.lean Outdated

Comment thread Mathlib/Tactic/Linter/Lint.lean Outdated

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label May 29, 2026

joneugster self-assigned this May 29, 2026

grunweg and others added 8 commits May 29, 2026 19:43

feat: check for larger overlap windows in the dupNamespace linter

66e1af5

chore: better error messages; update tests to include backticks

3b807aa

End-to-end-test for the new cases, including some by Snir

46afed1

Re-bless test

dcd8d37

set_option linter.dupNamespace false in (#7)

f062e83

Update Mathlib/Tactic/Linter/Lint.lean

5aab660

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Second comment; mirror change

9703215

thorimur reviewed Jun 17, 2026

View reviewed changes

Comment thread Mathlib/Tactic/Linter/Lint.lean Outdated

Apply suggestions from code review

72444dd

Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 17, 2026

Merge branch 'master' into dupnamespace-stronger

2aacaac

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

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 1, 2026

grunweg added 2 commits July 2, 2026 00:50

chore(CategoryTheory/Limits/Shapes/Pullback/HasPullback): fix depreca…

2e7d275

…tion The deprecation accidentally duplicated declaration namespaces, meaning it was never effective. This is confirmed by the declarations diff on the PR back then. Fix it.

grunweg added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Jul 1, 2026

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

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

mathlib-bors Bot changed the title ~~feat: make the dupNamespace linter catch any duplicate namespace(s)~~ [Merged by Bors] - feat: make the dupNamespace linter catch any duplicate namespace(s) Jul 2, 2026

mathlib-bors Bot closed this Jul 2, 2026

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

wkrozowski mentioned this pull request Jul 2, 2026

feat: add linter.extra.dupNamespace.consecutiveOnly option to dupNamespace linter leanprover/lean4#14249

Merged

Uh oh!

Conversation

grunweg commented May 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 2e7d27597d

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

Uh oh!

kim-em left a comment

Choose a reason for hiding this comment

Uh oh!

kim-em May 25, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg May 25, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-dependent-issues Bot commented May 25, 2026

Uh oh!

SnirBroshi commented May 25, 2026

Uh oh!

grunweg commented May 25, 2026

Uh oh!

grunweg commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SnirBroshi commented May 26, 2026

Uh oh!

grunweg commented May 27, 2026

Uh oh!

SnirBroshi commented May 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thorimur commented Jun 17, 2026

Uh oh!

github-actions Bot commented Jun 17, 2026

Uh oh!

grunweg commented Jun 17, 2026

Uh oh!

adomani commented Jul 1, 2026

Uh oh!

mathlib-bors Bot commented Jul 1, 2026

Uh oh!

grunweg commented Jul 1, 2026

Uh oh!

mathlib-auto-merge Bot commented Jul 1, 2026

Uh oh!

mathlib-bors Bot commented Jul 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

grunweg commented May 24, 2026 •

edited

Loading

github-actions Bot commented May 24, 2026 •

edited

Loading

grunweg commented May 25, 2026 •

edited

Loading

SnirBroshi commented May 27, 2026 •

edited

Loading