[Merged by Bors] - feat: overlapping instances linter by JovanGerb · Pull Request #38126 · leanprover-community/mathlib4

JovanGerb · 2026-04-16T15:47:17Z

This PR implements the overlapping instances linter, with better performance than the previous attempt.

The overlapping instances linter warns on data-carrying overlaps between instances in the local context of a declaration, as well as on redundant instances of Prop classes (i.e. those which can be synthesized from another instance in the context).

An annoyance is the need for withSetBoolOptionIn. This is a private declaration in the unusedInstancesInType linter, with a link to leanprover/lean4#13133, which has been merged. When that commit lands in mathlib, we should move to withSetOptionIn.

See #35095 and #33677 for previous iterations of this linter.

See #14731 for an old attempt at a weaker form of this linter.

Co-authored-by: @thorimur

… linter

…ive)

…rlaps

mathlib-merge-conflicts · 2026-05-26T03:54:28Z

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

jcommelin · 2026-05-26T09:30:42Z

bors d+

mathlib-bors · 2026-05-26T09:30:45Z

✌️ JovanGerb can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

This PR creates the `unrestricted` array in the unicode linter, which contains characters that have no restrictions on which selector they are followed by, and are not enforced to be followed by any selector at all. We include `'⚠'` in it to allow `⚠️`. We don't want to ban the text version (`⚠`), as this is used in lake output (without the text selector) and so may conceivably be mentioned in a comment. We plan to use `⚠️` in #38126.

mathlib-dependent-issues · 2026-05-26T19:41:56Z

This PR/issue depends on:

~~[Merged by Bors] - chore: adaptations for overlapping instances linter #38151~~
~~[Merged by Bors] - chore(GroupTheory/GroupAction/Hom): improve to_additive use #38150~~
~~[Merged by Bors] - feat: unrestricted character set in unicode linter #39796~~
By Dependent Issues (🤖). Happy coding!

…Instances-2

JovanGerb · 2026-05-26T21:00:27Z

(By the way, I think it would be better not to use force push, because it is easy to mess something up, and there is no way to check this after the fact, appart from reading the whole +777 line diff again)

thorimur · 2026-05-26T21:21:31Z

The force push only affects the last few commits that I overwrote, right? 👀 So presumably only those would need to be checked? (I guess there is a chance you accidentally delete a commit. 🤔)

In this case it was to banish the earlier merge of the #39796 branch, which was giving me a lot of trouble after the new version had been merged into master.

(Ah, I guess you can git revert merge commits, after looking into it...you just need some mysterious flags.)

thorimur · 2026-05-26T21:23:58Z

Anyway, I think this is finally all ready... 😁

JovanGerb · 2026-05-27T09:42:27Z

Ah yes I hadn't noticed that the force push only affected the last few commits. I think that soon we'll be able to remove withSetBoolOptionIn, but we can do that in a follow-up PR. Let's hope this merges without any new warnings:

bors r+

@thorimur

This PR implements the overlapping instances linter, with better performance than the previous attempt. The overlapping instances linter warns on data-carrying overlaps between instances in the local context of a declaration, as well as on redundant instances of `Prop` classes (i.e. those which can be synthesized from another instance in the context). An annoyance is the need for `withSetBoolOptionIn`. This is a private declaration in the `unusedInstancesInType` linter, with a link to leanprover/lean4#13133, which has been merged. When that commit lands in mathlib, we should move to `withSetOptionIn`. See #35095 and #33677 for previous iterations of this linter. See #14731 for an old attempt at a weaker form of this linter. Co-authored-by: @thorimur Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

mathlib-bors · 2026-05-27T11:17:15Z

Pull request successfully merged into master.

Build succeeded:

@thorimur

This PR implements the overlapping instances linter, with better performance than the previous attempt. The overlapping instances linter warns on data-carrying overlaps between instances in the local context of a declaration, as well as on redundant instances of `Prop` classes (i.e. those which can be synthesized from another instance in the context). An annoyance is the need for `withSetBoolOptionIn`. This is a private declaration in the `unusedInstancesInType` linter, with a link to leanprover/lean4#13133, which has been merged. When that commit lands in mathlib, we should move to `withSetOptionIn`. See leanprover-community#35095 and leanprover-community#33677 for previous iterations of this linter. See leanprover-community#14731 for an old attempt at a weaker form of this linter. Co-authored-by: @thorimur Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

…unity#39796) This PR creates the `unrestricted` array in the unicode linter, which contains characters that have no restrictions on which selector they are followed by, and are not enforced to be followed by any selector at all. We include `'⚠'` in it to allow `⚠️`. We don't want to ban the text version (`⚠`), as this is used in lake output (without the text selector) and so may conceivably be mentioned in a comment. We plan to use `⚠️` in leanprover-community#38126.

@thorimur

This PR implements the overlapping instances linter, with better performance than the previous attempt. The overlapping instances linter warns on data-carrying overlaps between instances in the local context of a declaration, as well as on redundant instances of `Prop` classes (i.e. those which can be synthesized from another instance in the context). An annoyance is the need for `withSetBoolOptionIn`. This is a private declaration in the `unusedInstancesInType` linter, with a link to leanprover/lean4#13133, which has been merged. When that commit lands in mathlib, we should move to `withSetOptionIn`. See leanprover-community#35095 and leanprover-community#33677 for previous iterations of this linter. See leanprover-community#14731 for an old attempt at a weaker form of this linter. Co-authored-by: @thorimur Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

…unity#39796) This PR creates the `unrestricted` array in the unicode linter, which contains characters that have no restrictions on which selector they are followed by, and are not enforced to be followed by any selector at all. We include `'⚠'` in it to allow `⚠️`. We don't want to ban the text version (`⚠`), as this is used in lake output (without the text selector) and so may conceivably be mentioned in a comment. We plan to use `⚠️` in leanprover-community#38126.

@thorimur

This PR implements the overlapping instances linter, with better performance than the previous attempt. The overlapping instances linter warns on data-carrying overlaps between instances in the local context of a declaration, as well as on redundant instances of `Prop` classes (i.e. those which can be synthesized from another instance in the context). An annoyance is the need for `withSetBoolOptionIn`. This is a private declaration in the `unusedInstancesInType` linter, with a link to leanprover/lean4#13133, which has been merged. When that commit lands in mathlib, we should move to `withSetOptionIn`. See leanprover-community#35095 and leanprover-community#33677 for previous iterations of this linter. See leanprover-community#14731 for an old attempt at a weaker form of this linter. Co-authored-by: @thorimur Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

JovanGerb and others added 30 commits January 6, 2026 19:35

feat: A linter for instances that overlap on data

d301b1f

chore: Init and import management

cc6b2b1

feat: localInstances argument to ContextInfo.runMetaMWithMessages

b4a8dbb

feat: getDeclBodyInfos

8176967

chore: import changes + header mgmt

8fa638f

refactor: return data from findOverlappingDataInstances, remove env…

a2594a1

… linter

feat: syntax linter overlappingInstances

72cd2cb

test: overlapping instances (first pass; all pass, but not comprehens…

e4cc55e

…ive)

chore: remove prettty printing logic for now

3167b84

chore: simplify and document some internals

664a00d

docs: misc.

d446fbd

test: update tests

73b6a3d

tweak: don't break, just record "dominating" cases

511c942

chore: deriving

f034b5d

refactor: use an ultimately simpler data structure for collecting ove…

b65b2ea

…rlaps

docs: explain choices

b377001

chore: refactor infotree utils slightly

369dd15

clean up else acc chain a bit

04a7e79

chore: remove unused variables

28d7938

chore: readability

691267d

chore: move comment

e9508ae

test: show projections

b60a105

chore: refactor message generation

e761690

chore: continue refactoring

c77a8d3

feat: first pass at deduplicating error messages

f86ae52

chore: tweak code comments

fe0dfa5

chore: update tests to remove redundant messages

6397f9f

chore: improve tests a bit (still needs some fleshing out)

b50ed2c

chore: variable names

490dd49

chore: improve message

0aaa23c

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

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

mathlib-merge-conflicts 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 May 26, 2026

mathlib-triage Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 26, 2026

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 26, 2026

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

thorimur and others added 4 commits May 26, 2026 16:18

chore: ite -> if then else since it no longer saves us a line

17fe8dd

chore: slightly nicer trace message

d7702a0

Merge branch 'master' into Jovan-overlappingInstances-2

4a91eb8

Merge remote-tracking branch 'upstream/master' into Jovan-overlapping…

f0cfcfc

…Instances-2

thorimur force-pushed the Jovan-overlappingInstances-2 branch from 9e4d1bc to f0cfcfc Compare May 26, 2026 20:20

mathlib-bors Bot changed the title ~~feat: overlapping instances linter~~ [Merged by Bors] - feat: overlapping instances linter May 27, 2026

mathlib-bors Bot closed this May 27, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Merged by Bors] - feat: overlapping instances linter#38126

[Merged by Bors] - feat: overlapping instances linter#38126
JovanGerb wants to merge 157 commits into
leanprover-community:masterfrom
JovanGerb:Jovan-overlappingInstances-2

JovanGerb commented Apr 16, 2026 •

edited by thorimur

Loading

Uh oh!

mathlib-merge-conflicts Bot commented May 26, 2026

Uh oh!

jcommelin commented May 26, 2026

Uh oh!

mathlib-bors Bot commented May 26, 2026

Uh oh!

mathlib-dependent-issues Bot commented May 26, 2026

Uh oh!

JovanGerb commented May 26, 2026

Uh oh!

thorimur commented May 26, 2026 •

edited

Loading

Uh oh!

thorimur commented May 26, 2026

Uh oh!

JovanGerb commented May 27, 2026

Uh oh!

mathlib-bors Bot commented May 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Uh oh!

Conversation

JovanGerb commented Apr 16, 2026 • edited by thorimur Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-merge-conflicts Bot commented May 26, 2026

Uh oh!

jcommelin commented May 26, 2026

Uh oh!

mathlib-bors Bot commented May 26, 2026

Uh oh!

mathlib-dependent-issues Bot commented May 26, 2026

Uh oh!

JovanGerb commented May 26, 2026

Uh oh!

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

Uh oh!

Uh oh!

thorimur commented May 26, 2026

Uh oh!

JovanGerb commented May 27, 2026

Uh oh!

mathlib-bors Bot commented May 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

JovanGerb commented Apr 16, 2026 •

edited by thorimur

Loading

thorimur commented May 26, 2026 •

edited

Loading