Skip to content

[Merged by Bors] - perf: shortcut instances for Semiring#39719

Closed
JovanGerb wants to merge 5 commits into
leanprover-community:masterfrom
JovanGerb:Jovan-Semiring-instances
Closed

[Merged by Bors] - perf: shortcut instances for Semiring#39719
JovanGerb wants to merge 5 commits into
leanprover-community:masterfrom
JovanGerb:Jovan-Semiring-instances

Conversation

@JovanGerb

@JovanGerb JovanGerb commented May 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR adds shortcut instances that make sure synthesis using Semiring doesn't go through the other ring-like classes. This matches the new definition of Semiring.

Open in Gitpod

@github-actions github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label May 22, 2026
@JovanGerb JovanGerb added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 22, 2026
@github-actions

github-actions Bot commented May 22, 2026 •
edited
Loading

Copy link
Copy Markdown

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

@JovanGerb

JovanGerb commented May 22, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@github-actions

github-actions Bot commented May 22, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 4fb7e69768

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance [Semiring α] : Distrib α := inferInstance
+ instance [Semiring α] : MulZeroClass α := inferInstance
+ instance [Semiring α] : MulZeroOneClass α := inferInstance

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.

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

@leanprover-radar

leanprover-radar commented May 22, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 4fb7e69 against 5032702 are in. There are significant results. @JovanGerb

  • ✅ build//instructions: -893.0G (-0.52%)

Medium changes (14✅, 1🟥)

  • ✅ build/module/Mathlib.Algebra.Order.Ring.Unbundled.Basic//instructions: -4.7G (-11.41%)
  • 🟥 build/module/Mathlib.Algebra.Ring.Subsemiring.MulOpposite//instructions: +2.0G (+21.75%)
  • ✅ build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula//instructions: -5.2G (-5.56%)
  • ✅ build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula//instructions: -14.2G (-7.58%)
  • ✅ build/module/Mathlib.Analysis.InnerProductSpace.Reproducing//instructions: -4.9G (-5.80%)
  • ✅ build/module/Mathlib.Analysis.Normed.Field.Basic//instructions: -1.8G (-6.32%)
  • ✅ build/module/Mathlib.CategoryTheory.Preadditive.SingleObj//instructions: -4.1G (-33.18%)
  • ✅ build/module/Mathlib.FieldTheory.SeparableClosure//instructions: -6.4G (-6.39%)
  • ✅ build/module/Mathlib.RepresentationTheory.FiniteIndex//instructions: -5.8G (-7.62%)
  • ✅ build/module/Mathlib.RingTheory.Invariant.Profinite//instructions: -5.1G (-4.11%)
  • ✅ build/module/Mathlib.RingTheory.Kaehler.JacobiZariski//instructions: -17.7G (-11.90%)
  • ✅ build/module/Mathlib.RingTheory.QuasiFinite.Weakly//instructions: -5.2G (-6.72%)
  • ✅ build/module/Mathlib.RingTheory.Unramified.LocalStructure//instructions: -7.3G (-4.15%)
  • ✅ build/module/Mathlib.Tactic.Algebra.Basic//instructions: -3.9G (-11.82%)
  • ✅ build/module/Mathlib.Topology.Algebra.Field//instructions: -4.0G (-19.48%)

Small changes (111✅, 11🟥)

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

@plp127 plp127 changed the title pref: shortcut instances for Semiring perf: shortcut instances for Semiring May 22, 2026
@github-actions github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 24, 2026
JovanGerb
JovanGerb commented May 24, 2026
View reviewed changes
Comment thread Mathlib/RingTheory/EuclideanDomain.lean
gcd_dvd_right := gcd_dvd_right
dvd_gcd := dvd_gcd
gcd_mul_lcm a b := by rw [EuclideanDomain.gcd_mul_lcm]
gcd_mul_lcm a b := by rw [EuclideanDomain.gcd_mul_lcm]; rfl

@JovanGerb JovanGerb May 24, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is now needed due to a bug in with_reducible rfl: it doesn't bump the transparency when unifying instance arguments, so it fails, and we need to add rfl.

JovanGerb
JovanGerb commented May 24, 2026
View reviewed changes
Comment thread Mathlib/Tactic/Ring/Basic.lean

omit [CommSemiring R] in
theorem Int.smul_eq_mul {n n' : ℤ} {r : R} [CommRing R] (hr : n = r) (hn : n' = n) (a : R) :
theorem Int.smul_eq_mul {R} {n n' : ℤ} {r : R} [CommRing R] (hr : n = r) (hn : n' = n) (a : R) :

@JovanGerb JovanGerb May 24, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

omitting instance arguments is very flaky, and now stopped working due to the slightly different synthesis order.

JovanGerb
JovanGerb commented May 24, 2026
View reviewed changes
Comment thread MathlibTest/hintAll.lean
Comment on lines -206 to -208
[apply] ring_nf
Remaining subgoals:
⊢ a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁

@JovanGerb JovanGerb May 24, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This ring_nf suggestion by hint was silly, as it clearly doesn't do anything. So it going away is arguably a good thing.

@sgouezel

sgouezel commented May 24, 2026

Copy link
Copy Markdown
Contributor

bors r+
Thanks!

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 24, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 24, 2026
@JovanGerb
perf: shortcut instances for Semiring (#39719)
f50b40f 
This PR adds shortcut instances that make sure synthesis using `Semiring` doesn't go through the other ring-like classes. This matches the new definition of `Semiring`.
@mathlib-bors

mathlib-bors Bot commented May 24, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title perf: shortcut instances for Semiring [Merged by Bors] - perf: shortcut instances for Semiring May 24, 2026
@mathlib-bors mathlib-bors Bot closed this May 24, 2026
@JovanGerb JovanGerb mentioned this pull request Jun 2, 2026
Closed
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@JovanGerb @b-mehta
perf: shortcut instances for Semiring (leanprover-community#39719)
af27b81 
This PR adds shortcut instances that make sure synthesis using `Semiring` doesn't go through the other ring-like classes. This matches the new definition of `Semiring`.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@JovanGerb @Bergschaf
perf: shortcut instances for Semiring (leanprover-community#39719)
698a853 
This PR adds shortcut instances that make sure synthesis using `Semiring` doesn't go through the other ring-like classes. This matches the new definition of `Semiring`.
mathlib-bors Bot pushed a commit that referenced this pull request Jun 4, 2026
@JovanGerb
perf: another shortcut instance for Semiring (#40153)
f5bbbdf 
This PR adds another shortcut instance for Semiring that I had missed in #39719, because I assumed that it had already been tagged as an instance automatically.
ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@JovanGerb @ReemMelamed
perf: another shortcut instance for Semiring (leanprover-community#…
35b3519 
…40153)

This PR adds another shortcut instance for Semiring that I had missed in leanprover-community#39719, because I assumed that it had already been tagged as an instance automatically.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@JovanGerb @leanprover-radar @sgouezel