feat: overlapping instances linter

[JovanGerb]

This is a new attempt at the overlapping instances linter, with better performance.

One question is where to put the yellow squiggle of the warning message. It is now at the start of the definition value, i.e. the by token for typical proofs. This is slightly annoying, because the yellow squiggle is overridden by the red squiggle from "unsolved goals".

Another annoyance is the need for withSetBoolOptionIn. This is a private declaration in the unusedInstancesInType linter, with a link to an unsolved issue. I've marked it public, but maybe it should go to a separate file, depending on how fast we think the issue will be resolved.

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

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

Co-authored-by: @thorimur

---

• depends on: chore: adaptations for overlapping instances linter #38151
• depends on: chore(GroupTheory/GroupAction/Hom): improve to_additive use #38150

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 3dec916 against 05475ca are in. No significant results found. @JovanGerb

• 🟥 build//instructions: +655.2G (+0.38%)

Medium changes (2🟥)

• 🟥 build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: +18.6G (+6.70%)
• 🟥 build/profile/interpretation//wall-clock: +8m 9s (+5.06%)

Small changes (3🟥)

• 🟥 build//instructions: +655.2G (+0.38%)
• 🟥 build/module/Mathlib.Analysis.Normed.Ring.Basic//instructions: +767.3M (+1.37%)
• 🟥 build/module/Mathlib.Lean.Meta.Basic//instructions: +143.3M (+3.69%)

and 1 hidden

[mathlib-dependent-issues]

This PR/issue depends on:

• chore: adaptations for overlapping instances linter #38151
• chore(GroupTheory/GroupAction/Hom): improve to_additive use #38150
  By Dependent Issues (🤖). Happy coding!

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for cfd593f against 05475ca are in. There are significant results. @JovanGerb

• 🟥 build//instructions: +1.3T (+0.74%)

Large changes (1🟥)

• 🟥 build/profile/interpretation//wall-clock: +10m 6s (+6.27%)

Medium changes (1🟥)

• 🟥 build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: +19.5G (+7.02%)

Small changes (24🟥)

Too many entries to display here. View the full report on radar instead.

[JovanGerb]

Wow, inlining the InfoTree folding function caused the loop to be run in the interpreter, which causes a big slowdown!

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 88dfef6 against 05475ca are in. No significant results found. @JovanGerb

• 🟥 build//instructions: +587.2G (+0.34%)

Medium changes (1🟥)

• 🟥 build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: +18.6G (+6.70%)

Small changes (3🟥)

• 🟥 build//instructions: +587.2G (+0.34%)
• 🟥 build/module/Mathlib.Lean.Meta.Basic//instructions: +141.3M (+3.64%)
• 🟥 build/profile/interpretation//wall-clock: +5m 59s (+3.71%)

and 1 hidden

[JovanGerb]

I'm pretty happy with the benchmark now. I only don't understand what makes this file UniversalFactorizationRing slow down so much. There aren't even that many instance hypotheses there.

[JovanGerb]

Just to confirm the UniversalFactorizationRing slowdown is not a fluke:

!bench

[leanprover-radar]

Benchmark results for bb07869 against 9470b68 are in. No significant results found. @JovanGerb

• 🟥 build//instructions: +599.5G (+0.35%)

Medium changes (2🟥)

• 🟥 build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: +18.4G (+6.61%)
• 🟥 build/profile/interpretation//wall-clock: +7m 57s (+4.95%)

Small changes (1🟥)

1 hidden