Skip to content

chore: changes for leanprover/lean4#2478#7257

Closed
mattrobball wants to merge 1000 commits intomasterfrom
lean-pr-testing-2478
Closed

chore: changes for leanprover/lean4#2478#7257
mattrobball wants to merge 1000 commits intomasterfrom
lean-pr-testing-2478

Conversation

@mattrobball
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball commented Sep 19, 2023 •
edited
Loading

These are adaptions to adjust for the changes to structure instance elaboration in leanprover/lean4#2478.

Open in Gitpod

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Sep 20, 2023

The benchmarking seems to say:

  • this results in a speed up for many files in Mathlib
  • but a significant slow-down in the worst files
  • overall a 4.5% decrease in instructions
  • overall a 2.5% wall-clock slow-down

I'm not entirely sure what to do with that.

The optimist in me says: the worst files (particularly AlgebraicGeometry.*) have something fundamentally wrong in them (but what?), and when we sort them out they will, like everything else, get a speed up too.

The pessimist says: this is an overall slow-down.

@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Sep 20, 2023 •
edited
Loading

Since there are existing fixes for RingTheory.Kaehler and Analysis.NormedSpace.Operator, let's eliminate them from consideration.

The significant regressions (double digits) in large files are then all concentrated in AlgebraicGeometry.

Parts of AG are unusable at the moment.

Everyone is affected by it since one file and the path to it completely control the build time for all of Mathlib. This is why total build time is a poor measure of performance improvement. It only measures the effect on RingHomProperties.

The terms exposed are simply too large. I'd wager that it leads all folders in use of erw when appropriately measured, for example.

The change here creates more tightly packed terms which is great when your design is disciplined but terrible when it's not. In particular, when you rely on exposing giant terms in unification, you are going to need more cycles to succeed and pay the price.

There needs to be a refactor enforcing API boundaries in AG. Should we postpone the benefits for everyone else until this is done?

@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Sep 20, 2023

but a significant slow-down in the worst files

Excluding Kaehler and OperatorNorm, there is a good net drop in instructions for the ten largest (by instructions) files.

It only gets better when you go to top 20 or 30.

Areas of concern like GroupCohomology (number 3 and 5) get noticeably better.

kim-em
kim-em reviewed Sep 21, 2023
View reviewed changes
kim-em
kim-em reviewed Sep 21, 2023
View reviewed changes
kim-em
kim-em reviewed Sep 21, 2023
View reviewed changes
kim-em
kim-em reviewed Sep 21, 2023
View reviewed changes
kim-em
kim-em reviewed Sep 21, 2023
View reviewed changes
kim-em
kim-em reviewed Sep 21, 2023
View reviewed changes
kim-em
kim-em reviewed Sep 21, 2023
View reviewed changes
@kim-em kim-em mentioned this pull request Sep 21, 2023
Merged
@mattrobball mattrobball mentioned this pull request Sep 21, 2023
Closed
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 21, 2023
@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 22, 2023
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 22, 2023
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Oct 16, 2023
@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Oct 16, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 16, 2023

Here are the benchmark results for commit 2c655ab.
There were significant changes against commit e3644b2:

  Benchmark                                                          Metric             Change
  ============================================================================================
+ build                                                              compilation         -5.2%
+ build                                                              elaboration         -6.0%
+ build                                                              tactic execution    -6.8%
+ build                                                              type checking      -12.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions       -14.5%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions        -6.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions       -22.4%
+ ~Mathlib.Algebra.DirectLimit                                       instructions       -36.0%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions       -13.7%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions       -21.9%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions        -4.0%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions       -20.9%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions       -33.3%
+ ~Mathlib.Algebra.Module.PID                                        instructions       -14.9%
+ ~Mathlib.Algebra.RingQuot                                          instructions       -15.4%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra                          instructions        -3.0%
- ~Mathlib.AlgebraicGeometry.AffineScheme                            instructions         7.9%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point                     instructions        -2.8%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass               instructions        -3.0%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions        19.1%
+ ~Mathlib.Analysis.Calculus.ContDiff                                instructions        -9.0%
+ ~Mathlib.Analysis.Calculus.ContDiffDef                             instructions        -5.3%
+ ~Mathlib.Analysis.Convolution                                      instructions        -2.6%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions        -9.1%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions        -3.6%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions        -8.0%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions        16.9%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions       -13.7%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions       -14.7%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions        -8.9%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions       -38.9%
+ ~Mathlib.Analysis.NormedSpace.Multilinear                          instructions        -6.1%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions       -22.2%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions        -4.7%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions       -11.7%
+ ~Mathlib.Analysis.Seminorm                                         instructions        -7.2%
+ ~Mathlib.CategoryTheory.Abelian.InjectiveResolution                instructions        -6.9%
+ ~Mathlib.CategoryTheory.Abelian.Projective                         instructions        -1.3%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory          instructions        -4.4%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions        -3.6%
+ ~Mathlib.Data.Matrix.Rank                                          instructions       -13.6%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions        -5.4%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions        12.5%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions        -3.8%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions       -15.1%
+ ~Mathlib.FieldTheory.IsAlgClosed.Basic                             instructions        -6.4%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions        -3.2%
+ ~Mathlib.FieldTheory.Subfield                                      instructions       -10.0%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions        -8.3%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions       -40.3%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions       -29.7%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions        -5.6%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions       -13.0%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions       -12.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions       -22.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions       -20.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions       -43.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions       -36.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions       -14.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions       -13.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions       -25.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions       -19.1%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions        -7.3%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions       -33.5%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions       -24.7%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions       -25.0%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions         6.4%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions        -2.6%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions       -24.7%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions        -5.6%
+ ~Mathlib.LinearAlgebra.QuotientPi                                  instructions       -14.6%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions        -4.5%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions       -10.6%
+ ~Mathlib.MeasureTheory.Function.LpSeminorm                         instructions        -4.0%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions       -17.0%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions        -8.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions        -4.8%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions        -7.4%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions       -31.1%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions        -6.9%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions       -20.9%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions       -11.0%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions        -8.0%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions        -7.6%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions       -10.4%
+ ~Mathlib.RepresentationTheory.Character                            instructions       -11.6%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution           instructions        -1.3%
+ ~Mathlib.RepresentationTheory.Rep                                  instructions        -4.9%
+ ~Mathlib.RingTheory.Adjoin.Field                                   instructions       -17.7%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions        -3.5%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions        -8.9%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions       -12.5%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions       -13.5%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions       -22.5%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions       -24.3%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions        -5.3%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions       -14.1%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions        -5.8%
+ ~Mathlib.RingTheory.Norm                                           instructions        -9.5%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions       -29.5%
+ ~Mathlib.RingTheory.Perfection                                     instructions        -4.5%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions       -26.0%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions        -3.9%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions       -11.6%
+ ~Mathlib.RingTheory.Valuation.Basic                                instructions        -4.9%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions       -13.1%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions       -15.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions       -10.8%

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Oct 17, 2023

That benchmark is great news!

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 18, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 19, 2023
@mattrobball mattrobball changed the title Lean pr testing 2478 chore: changes for leanprover/lean4#2478 Nov 6, 2023
@mattrobball mattrobball marked this pull request as ready for review November 6, 2023 00:37
@mattrobball mattrobball added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 6, 2023
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Nov 8, 2023
@mattrobball mattrobball closed this Nov 9, 2023
@sgouezel sgouezel added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

Assignees

No one assigned

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) 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.

8 participants

@mattrobball @kim-em @leanprover-bot @sgouezel @eric-wieser @collares @PatrickMassot @dwrensha