Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - perf: improve some instances in Polynomial #7434

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - perf: improve some instances in Polynomial #7434

wants to merge 3 commits into from

Conversation

ChrisHughes24
Copy link
Member

@ChrisHughes24 ChrisHughes24 commented Sep 29, 2023 •
edited
Loading

Open in Gitpod

@ChrisHughes24 ChrisHughes24 added WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes labels Sep 29, 2023
@ChrisHughes24
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit c5bca0a.
There were significant changes against commit 042888f:

  Benchmark                                                   Metric         Change
  =================================================================================
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point              instructions   -40.6%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass        instructions   -19.5%
- ~Mathlib.Data.Polynomial.Basic                              instructions    20.3%
+ ~Mathlib.Data.Polynomial.Div                                instructions    -8.7%
+ ~Mathlib.Data.Polynomial.Lifts                              instructions    -7.6%
+ ~Mathlib.FieldTheory.Finite.GaloisField                     instructions   -15.9%
+ ~Mathlib.FieldTheory.IsAlgClosed.Spectrum                   instructions    -8.2%
+ ~Mathlib.FieldTheory.IsSepClosed                            instructions    -7.4%
+ ~Mathlib.FieldTheory.Normal                                 instructions    -6.3%
+ ~Mathlib.FieldTheory.Perfect                                instructions    -5.8%
+ ~Mathlib.FieldTheory.PrimitiveElement                       instructions    -7.5%
+ ~Mathlib.FieldTheory.SplittingField.Construction            instructions   -11.6%
+ ~Mathlib.FieldTheory.SplittingField.IsSplittingField        instructions    -8.7%
+ ~Mathlib.LinearAlgebra.AnnihilatingPolynomial               instructions   -26.1%
+ ~Mathlib.LinearAlgebra.FreeModule.Norm                      instructions   -61.0%
+ ~Mathlib.LinearAlgebra.Lagrange                             instructions    -5.8%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Basic                instructions    -9.7%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff                instructions    -7.6%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField          instructions   -24.9%
+ ~Mathlib.NumberTheory.BernoulliPolynomials                  instructions    -6.7%
+ ~Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree   instructions    -6.3%
+ ~Mathlib.NumberTheory.ClassNumber.FunctionField             instructions   -20.5%
+ ~Mathlib.NumberTheory.KummerDedekind                        instructions    -7.0%
+ ~Mathlib.RingTheory.AdjoinRoot                              instructions   -49.9%
+ ~Mathlib.RingTheory.AlgebraicIndependent                    instructions    -5.1%
+ ~Mathlib.RingTheory.Jacobson                                instructions   -33.6%
+ ~Mathlib.RingTheory.JacobsonIdeal                           instructions    -8.9%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev                    instructions    -5.3%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma                   instructions    -6.7%
+ ~Mathlib.RingTheory.Polynomial.Nilpotent                    instructions    -8.9%
+ ~Mathlib.RingTheory.Polynomial.Quotient                     instructions   -28.4%
+ ~Mathlib.RingTheory.RootsOfUnity.Minpoly                    instructions    -7.9%

@ChrisHughes24 ChrisHughes24 mentioned this pull request Sep 29, 2023
Open
@ChrisHughes24 ChrisHughes24 added blocked-by-other-PR This PR depends on another PR to Mathlib WIP Work in progress and removed WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes labels Sep 30, 2023
@kbuzzard
Copy link
Member

kbuzzard commented Sep 30, 2023 •
edited
Loading

Note also that build instructions (a measurement of total build time) goes down 0.92%. 🎉

mattrobball
mattrobball reviewed Oct 2, 2023
View reviewed changes
Mathlib/Data/Polynomial/Basic.lean
@@ -291,18 +291,27 @@ instance natCast : NatCast R[X] :=
#align polynomial.has_nat_cast Polynomial.natCast

instance semiring : Semiring R[X] :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

Would building up through the hierarchy to Semiring R[X] yield even better performance? Or would it be middling?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Same with other ones below.

Copy link
Member Author

Choose a reason for hiding this comment

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

Possibly. I don't see why it would but it is certainly possible that it could because I don't fully understand this stuff

Copy link
Member Author

Choose a reason for hiding this comment

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

How about merging this and I experiment with further improvements in another PR?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Sounds good to me.

Mathlib/Data/Polynomial/Basic.lean Outdated Show resolved Hide resolved
@ChrisHughes24 ChrisHughes24 added awaiting-review and removed WIP Work in progress blocked-by-other-PR This PR depends on another PR to Mathlib labels Oct 4, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Oct 4, 2023
@ChrisHughes24 ChrisHughes24 removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Oct 4, 2023
@mattrobball
Copy link
Collaborator

bors d+

@bors
Copy link

bors bot commented Oct 4, 2023

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

@ChrisHughes24
Copy link
Member Author

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 5, 2023
bors bot pushed a commit that referenced this pull request Oct 5, 2023
@ChrisHughes24
perf: improve some instances in Polynomial (#7434)
4b53c17
@bors
Copy link

bors bot commented Oct 5, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title perf: improve some instances in Polynomial [Merged by Bors] - perf: improve some instances in Polynomial Oct 5, 2023
@bors bors bot closed this Oct 5, 2023
@bors bors bot deleted the polyPerfCH branch October 5, 2023 11:48
ChrisHughes24 added a commit that referenced this pull request Oct 5, 2023
@ChrisHughes24
perf(Polynomial): fix CommSemiring instance missed in #7434
061b503
bors bot pushed a commit that referenced this pull request Oct 5, 2023
@ChrisHughes24
perf(Polynomial): fix CommSemiring instance missed in #7434 (#7518)
d7f380a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mattrobball mattrobball mattrobball left review comments

Assignees
No one assigned
Labels
delegated ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@ChrisHughes24 @leanprover-bot @kbuzzard @mattrobball @leanprover-community-mathlib4-bot