Skip to content

refactor(Algebra/Order/Monoid/Unbundled/Defs): upgrade *ReflectLE from abbrevs to classes#37393

Open
SnirBroshi wants to merge 11 commits intoleanprover-community:masterfrom
SnirBroshi:refactor/algebra/reflect-le-abbrevs-to-classes
Open

refactor(Algebra/Order/Monoid/Unbundled/Defs): upgrade *ReflectLE from abbrevs to classes#37393
SnirBroshi wants to merge 11 commits intoleanprover-community:masterfrom
SnirBroshi:refactor/algebra/reflect-le-abbrevs-to-classes

Conversation

@SnirBroshi
Copy link
Copy Markdown
Collaborator

@SnirBroshi SnirBroshi commented Mar 30, 2026 •
edited
Loading

... to mitigate performance regression caused by #36629.
Currently these classes are an abbrev for ContravariantClass so when TC-search tries to synthesize them it ends up looking through all the ContravariantClass instances and not just the relevant ones.

Zulip

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 30, 2026 •
edited
Loading

PR summary 6ef8cc2731

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance (priority := 900) IsOrderedCancelMonoid.toMulLeftReflectLT : MulLeftReflectLT α
+ rel_iff_cov'
- instance (priority := 900) IsOrderedCancelMonoid.toMulLeftReflectLT :

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Mar 30, 2026
@SnirBroshi
Copy link
Copy Markdown
Collaborator Author

SnirBroshi commented Mar 31, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 31, 2026 •
edited
Loading

Benchmark results for 4b8b731 against b301d25 are in. Significant changes detected! @SnirBroshi

  • ✅ build//instructions: -167.0G (-0.09%)

Medium changes (2✅)

  • ✅ build/module/Mathlib.RingTheory.Finiteness.NilpotentKer//instructions: -2.3G (-10.53%)
  • ✅ build/profile/grind typeclass inference//wall-clock: -12s (-6.86%)

Small changes (27✅, 2🟥)

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

vihdzp
vihdzp reviewed Mar 31, 2026
View reviewed changes
@SnirBroshi SnirBroshi requested a review from JovanGerb April 2, 2026 16:45
@JovanGerb
Copy link
Copy Markdown
Contributor

JovanGerb commented Apr 2, 2026

I would also say it would be nicer to not use this CovariantClass field. Instead, we can simply have a field directly specifying the property we want.

@SnirBroshi SnirBroshi requested review from JovanGerb and removed request for JovanGerb April 3, 2026 14:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@JovanGerb JovanGerb Awaiting requested review from JovanGerb

1 more reviewer

@vihdzp vihdzp vihdzp left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@SnirBroshi @leanprover-radar @JovanGerb @vihdzp