Skip to content

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

Closed
ChrisHughes24 wants to merge 3 commits intomasterfrom
polyPerfCH
Closed

[Merged by Bors] - perf: improve some instances in Polynomial#7434
ChrisHughes24 wants to merge 3 commits intomasterfrom
polyPerfCH

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Sep 29, 2023


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
Copy Markdown
Member Author

!bench

@leanprover-bot
Copy link
Copy Markdown
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 added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) 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
Copy Markdown
Member

kbuzzard commented Sep 30, 2023

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

@@ -291,18 +291,27 @@ instance natCast : NatCast R[X] :=
#align polynomial.has_nat_cast Polynomial.natCast

instance semiring : Semiring R[X] :=
Copy link
Copy Markdown
Contributor

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
Copy Markdown
Contributor

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
Copy Markdown
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
Copy Markdown
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
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Sounds good to me.

@ChrisHughes24 ChrisHughes24 added awaiting-review and removed WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Oct 4, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 4, 2023
@ChrisHughes24 ChrisHughes24 removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 4, 2023
@mattrobball
Copy link
Copy Markdown
Contributor

bors d+

@bors
Copy link
Copy Markdown

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.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Oct 4, 2023
@ChrisHughes24
Copy link
Copy Markdown
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
@bors
Copy link
Copy Markdown

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants