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

chore: changes for leanprover/lean4#2478 #9007

Closed
wants to merge 2,063 commits into from
Closed

chore: changes for leanprover/lean4#2478 #9007

wants to merge 2,063 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Dec 12, 2023 •
edited

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

Open in Gitpod

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 12, 2023
@mattrobball mattrobball mentioned this pull request Dec 12, 2023
Merged
@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 3549a26.
There were significant changes against commit de48aea:

  Benchmark                                                          Metric          Change
  =========================================================================================
+ build                                                              type checking   -11.0%
- open Mathlib                                                       wall-clock        5.4%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions    -14.4%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions     -5.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions    -17.5%
+ ~Mathlib.Algebra.DirectLimit                                       instructions     -5.3%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions    -13.4%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions    -22.1%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions     -4.4%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions    -20.8%
+ ~Mathlib.Algebra.Lie.Killing                                       instructions    -11.3%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions    -34.6%
+ ~Mathlib.Algebra.Module.PID                                        instructions    -14.8%
+ ~Mathlib.Algebra.Quaternion                                        instructions     -5.3%
+ ~Mathlib.Algebra.RingQuot                                          instructions    -18.1%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                     instructions     -4.5%
+ ~Mathlib.AlgebraicGeometry.Properties                              instructions    -23.2%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                          instructions     -5.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                         instructions    -22.1%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                           instructions     -5.9%
+ ~Mathlib.Analysis.Convolution                                      instructions     -2.9%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions     -9.5%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions     -6.6%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                          instructions     -2.8%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions     -8.2%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions     14.4%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions    -14.3%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions    -15.1%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions     -9.3%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions    -40.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                    instructions     -3.9%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                    instructions    -13.0%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions     -2.0%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions    -10.6%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions    -20.3%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions     -5.7%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions    -11.7%
+ ~Mathlib.Analysis.Seminorm                                         instructions     -7.3%
+ ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions     -3.1%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                instructions    -10.0%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions     -3.8%
+ ~Mathlib.Data.Matrix.Rank                                          instructions    -13.8%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions     -5.7%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions     12.2%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions     -8.4%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions    -14.9%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions    -24.2%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions     -3.0%
+ ~Mathlib.FieldTheory.Subfield                                      instructions     -9.9%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions     -8.7%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions    -40.8%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions    -29.1%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions     -5.6%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions    -13.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions    -12.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions    -24.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions    -20.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions    -43.9%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions    -37.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions    -16.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions    -24.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions    -25.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions    -18.7%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions     -7.3%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions    -33.5%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions    -26.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions    -25.2%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions     -4.4%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions     -3.0%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions    -24.0%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions     -5.4%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions     -4.1%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions    -22.8%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions     -9.9%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions    -17.1%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions     -9.3%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions     -5.0%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions     -7.8%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions    -32.9%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions    -11.2%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions    -19.8%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions    -13.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions     -8.4%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions     -8.9%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions    -10.4%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions     -3.6%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions    -10.1%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions    -15.0%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions    -13.6%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions    -23.0%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions    -25.5%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions     -5.5%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions    -15.2%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions     -5.8%
+ ~Mathlib.RingTheory.Kaehler                                        instructions     -3.5%
+ ~Mathlib.RingTheory.Norm                                           instructions    -11.3%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions    -29.6%
+ ~Mathlib.RingTheory.Perfection                                     instructions     -4.8%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions    -26.5%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions     -5.0%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions    -11.6%
+ ~Mathlib.RingTheory.Valuation.Basic                                instructions     -5.2%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions    -14.1%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField              instructions    -19.3%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions    -14.7%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                      instructions    -12.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions    -11.8%

@mattrobball
Copy link
Collaborator Author

mattrobball commented Dec 13, 2023 •
edited

Failures of simp only [Pi.smul_apply] diagnosed here. Work around pending.

Using simp [Pi.smul_apply _] to make binderInfo explicit and relax transparency strictures used in simp for unification.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Dec 14, 2023
@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 889810f.
There were significant changes against commit 3465d1a:

  Benchmark                                                          Metric          Change
  =========================================================================================
+ build                                                              type checking    -9.3%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions    -14.2%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions     -5.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions    -16.8%
+ ~Mathlib.Algebra.DirectLimit                                       instructions     -5.2%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions    -13.4%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions    -21.6%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions    -20.6%
+ ~Mathlib.Algebra.Lie.Killing                                       instructions    -11.2%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions    -33.6%
+ ~Mathlib.Algebra.Module.PID                                        instructions    -13.7%
+ ~Mathlib.Algebra.RingQuot                                          instructions    -15.7%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                     instructions     -3.9%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions     17.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                          instructions     -5.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                         instructions    -22.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                           instructions     -5.9%
+ ~Mathlib.Analysis.Convolution                                      instructions     -2.9%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions     -9.3%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions     -6.4%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions     -7.6%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions     14.7%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions    -14.3%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions    -14.5%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions     -9.2%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions    -40.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                    instructions     -3.1%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                    instructions    -12.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions     -2.1%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions    -11.2%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions    -19.9%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions     -5.6%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions    -11.7%
+ ~Mathlib.Analysis.Seminorm                                         instructions     -7.3%
+ ~Mathlib.CategoryTheory.Abelian.ProjectiveResolution               instructions     -2.7%
+ ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions     -3.1%
+ ~Mathlib.CategoryTheory.Monoidal.Mon_                              instructions     -3.6%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                instructions     -9.5%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions     -3.2%
+ ~Mathlib.Data.Matrix.Rank                                          instructions    -13.3%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions     -4.5%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions     11.5%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions     -9.2%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions    -14.6%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions    -23.9%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions     -3.5%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions     -8.5%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions    -40.7%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions    -29.1%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions     -5.5%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions    -13.4%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions    -12.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions    -24.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions    -20.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions    -43.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions    -36.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions    -15.9%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions    -24.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions    -25.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions    -18.6%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions     -7.1%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions    -32.7%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions    -26.3%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions    -24.8%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions     -9.0%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions     -2.7%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions    -23.9%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions     -4.9%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions     -3.5%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions    -23.1%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions     -9.6%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions    -17.1%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions     -9.0%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions     -5.3%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions     -7.8%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions    -33.3%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions    -12.6%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure                        instructions    -16.6%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions    -19.9%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions    -13.4%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions     -6.1%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions     -8.5%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions    -11.4%
+ ~Mathlib.RepresentationTheory.Action.Basic                         instructions     -2.6%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions     -9.4%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions    -14.8%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions    -12.7%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions    -22.6%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions    -25.4%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions     -5.2%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions    -14.3%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions     -5.2%
+ ~Mathlib.RingTheory.Kaehler                                        instructions     -2.9%
+ ~Mathlib.RingTheory.Norm                                           instructions     -9.7%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions    -29.2%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions    -25.1%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions     -4.1%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions    -11.4%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions    -13.8%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField              instructions    -18.9%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions    -14.4%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                      instructions    -11.9%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions    -11.7%

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 889810f.
There were significant changes against commit 3465d1a:

  Benchmark                                                          Metric          Change
  =========================================================================================
+ build                                                              type checking    -9.3%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions    -14.2%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions     -5.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions    -16.8%
+ ~Mathlib.Algebra.DirectLimit                                       instructions     -5.2%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions    -13.4%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions    -21.6%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions    -20.6%
+ ~Mathlib.Algebra.Lie.Killing                                       instructions    -11.2%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions    -33.6%
+ ~Mathlib.Algebra.Module.PID                                        instructions    -13.7%
+ ~Mathlib.Algebra.RingQuot                                          instructions    -15.7%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                     instructions     -3.9%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions     17.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                          instructions     -5.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                         instructions    -22.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                           instructions     -5.9%
+ ~Mathlib.Analysis.Convolution                                      instructions     -2.9%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions     -9.3%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions     -6.4%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions     -7.6%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions     14.7%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions    -14.3%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions    -14.5%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions     -9.2%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions    -40.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                    instructions     -3.1%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                    instructions    -12.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions     -2.1%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions    -11.2%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions    -19.9%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions     -5.6%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions    -11.7%
+ ~Mathlib.Analysis.Seminorm                                         instructions     -7.3%
+ ~Mathlib.CategoryTheory.Abelian.ProjectiveResolution               instructions     -2.7%
+ ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions     -3.1%
+ ~Mathlib.CategoryTheory.Monoidal.Mon_                              instructions     -3.6%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                instructions     -9.5%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions     -3.2%
+ ~Mathlib.Data.Matrix.Rank                                          instructions    -13.3%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions     -4.5%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions     11.5%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions     -9.2%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions    -14.6%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions    -23.9%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions     -3.5%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions     -8.5%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions    -40.7%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions    -29.1%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions     -5.5%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions    -13.4%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions    -12.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions    -24.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions    -20.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions    -43.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions    -36.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions    -15.9%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions    -24.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions    -25.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions    -18.6%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions     -7.1%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions    -32.7%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions    -26.3%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions    -24.8%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions     -9.0%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions     -2.7%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions    -23.9%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions     -4.9%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions     -3.5%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions    -23.1%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions     -9.6%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions    -17.1%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions     -9.0%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions     -5.3%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions     -7.8%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions    -33.3%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions    -12.6%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure                        instructions    -16.6%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions    -19.9%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions    -13.4%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions     -6.1%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions     -8.5%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions    -11.4%
+ ~Mathlib.RepresentationTheory.Action.Basic                         instructions     -2.6%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions     -9.4%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions    -14.8%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions    -12.7%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions    -22.6%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions    -25.4%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions     -5.2%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions    -14.3%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions     -5.2%
+ ~Mathlib.RingTheory.Kaehler                                        instructions     -2.9%
+ ~Mathlib.RingTheory.Norm                                           instructions     -9.7%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions    -29.2%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions    -25.1%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions     -4.1%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions    -11.4%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions    -13.8%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField              instructions    -18.9%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions    -14.4%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                      instructions    -11.9%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions    -11.7%

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit f861b00.
There were significant changes against commit 3465d1a:

  Benchmark                                                          Metric          Change
  =========================================================================================
- build                                                              linting           5.2%
+ build                                                              type checking    -9.5%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions    -14.2%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions     -5.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions    -16.8%
+ ~Mathlib.Algebra.DirectLimit                                       instructions     -5.2%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions    -13.4%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions    -21.6%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions    -20.6%
+ ~Mathlib.Algebra.Lie.Killing                                       instructions    -11.2%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions    -33.6%
+ ~Mathlib.Algebra.Module.PID                                        instructions    -13.6%
+ ~Mathlib.Algebra.RingQuot                                          instructions    -15.7%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                     instructions     -3.8%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions     17.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                          instructions     -5.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                         instructions    -22.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                           instructions     -5.8%
+ ~Mathlib.Analysis.Convolution                                      instructions     -2.9%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions     -9.3%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions     -6.3%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions     -7.6%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions     14.7%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions    -14.3%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions    -14.5%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions     -9.2%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions    -40.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                    instructions     -3.5%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                    instructions    -12.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions     -2.0%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions    -11.2%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions    -19.9%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions     -5.6%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions    -11.7%
+ ~Mathlib.Analysis.Seminorm                                         instructions     -7.3%
+ ~Mathlib.CategoryTheory.Abelian.ProjectiveResolution               instructions     -2.7%
+ ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions     -3.0%
+ ~Mathlib.CategoryTheory.Monoidal.Mon_                              instructions     -3.6%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                instructions     -9.5%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions     -3.2%
+ ~Mathlib.Data.Matrix.Rank                                          instructions    -13.3%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions     -4.5%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions     11.4%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions    -10.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions    -14.6%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions    -23.9%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions     -3.5%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions     -8.5%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions    -40.7%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions    -29.1%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions     -5.5%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions    -13.4%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions    -12.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions    -24.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions    -20.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions    -43.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions    -36.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions    -15.9%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions    -24.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions    -25.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions    -18.5%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions     -7.1%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions    -32.7%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions    -26.3%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions    -24.8%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions     -9.0%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions     -2.7%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions    -24.0%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions     -4.9%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions     -3.5%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions    -23.1%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions     -9.6%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions    -17.1%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions     -9.0%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions     -5.3%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions     -7.8%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions    -33.3%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions    -12.6%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure                        instructions    -16.6%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions    -19.9%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions    -13.4%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions     -6.1%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions     -8.5%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions    -11.4%
+ ~Mathlib.RepresentationTheory.Action.Basic                         instructions     -2.6%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions     -9.3%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions    -14.7%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions    -12.7%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions    -22.6%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions    -25.3%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions     -5.2%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions    -14.4%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions     -5.3%
+ ~Mathlib.RingTheory.Kaehler                                        instructions     -2.9%
+ ~Mathlib.RingTheory.Norm                                           instructions     -9.7%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions    -29.2%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions    -25.1%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions     -4.1%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions    -11.4%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions    -13.8%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField              instructions    -18.9%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions    -14.4%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                      instructions    -11.9%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions    -11.7%

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 382e567.
There were significant changes against commit 3465d1a:

  Benchmark                                                          Metric          Change
  =========================================================================================
+ build                                                              type checking    -9.4%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions    -14.3%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions     -5.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions    -17.3%
+ ~Mathlib.Algebra.DirectLimit                                       instructions     -5.6%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions    -13.3%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions    -21.7%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions     -4.2%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions    -20.7%
+ ~Mathlib.Algebra.Lie.Killing                                       instructions    -11.1%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions    -33.6%
+ ~Mathlib.Algebra.Module.PID                                        instructions    -11.7%
+ ~Mathlib.Algebra.Quaternion                                        instructions     -5.0%
+ ~Mathlib.Algebra.RingQuot                                          instructions    -16.0%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                     instructions     -4.5%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions     17.6%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                          instructions     -5.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                         instructions    -22.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                           instructions     -5.8%
+ ~Mathlib.Analysis.Convolution                                      instructions     -2.8%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions     -9.4%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions     -6.5%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                          instructions     -2.5%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions     -7.9%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions     14.7%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions    -14.2%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions    -14.7%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions     -9.2%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions    -40.1%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                    instructions     -4.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                    instructions    -12.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions     -2.0%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions    -11.3%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions    -20.0%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions     -5.3%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions    -11.6%
+ ~Mathlib.Analysis.Seminorm                                         instructions     -7.2%
- ~Mathlib.CategoryTheory.Abelian.ProjectiveResolution               instructions      5.9%
+ ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions     -3.0%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                instructions     -9.8%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions     -3.7%
+ ~Mathlib.Data.Matrix.Rank                                          instructions    -13.7%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions     -5.0%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions     10.4%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions     -9.8%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions    -14.8%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions    -23.9%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions     -4.7%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions     -8.6%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions    -40.8%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions    -29.1%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions     -5.5%
- ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing               instructions      2.2%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions    -13.2%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions    -12.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions    -24.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions    -20.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions    -43.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions    -36.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions    -15.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions    -24.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions    -25.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions    -18.7%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions     -7.2%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions    -32.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions    -25.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions    -24.8%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions     -4.3%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions     -2.9%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions    -24.0%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions     -5.2%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions     -4.0%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions    -22.7%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions     -9.7%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions    -17.0%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions     -9.0%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions     -4.8%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions     -7.6%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions    -32.8%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions    -11.1%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions    -19.7%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions    -13.6%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions     -6.1%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions     -8.8%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions    -11.0%
+ ~Mathlib.RepresentationTheory.Rep                                  instructions     -4.9%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions     -3.3%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions     -9.7%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions    -13.4%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions    -13.1%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions    -22.5%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions    -25.4%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions     -5.3%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions    -14.3%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions     -5.7%
+ ~Mathlib.RingTheory.Kaehler                                        instructions     -2.9%
+ ~Mathlib.RingTheory.Norm                                           instructions     -9.9%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions    -29.4%
+ ~Mathlib.RingTheory.Perfection                                     instructions     -4.7%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions    -25.3%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions     -4.5%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions    -11.4%
+ ~Mathlib.RingTheory.Valuation.Basic                                instructions     -5.0%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions    -14.0%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField              instructions    -19.1%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions    -14.4%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                      instructions    -11.9%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions    -11.7%

@mattrobball mattrobball force-pushed the lean-pr-testing-2478 branch 2 times, most recently from cddbd4c to fe82dd9 Compare December 14, 2023 19:02
@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit a0a58ad.
There were significant changes against commit 0b290c7:

  Benchmark                                                          Metric          Change
  =========================================================================================
+ build                                                              type checking   -12.1%
+ lint                                                               wall-clock       -5.6%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions    -14.3%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions     -5.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions    -17.3%
+ ~Mathlib.Algebra.DirectLimit                                       instructions     -5.5%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions    -13.3%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions    -21.7%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions     -4.2%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions    -20.7%
+ ~Mathlib.Algebra.Lie.Killing                                       instructions    -11.1%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions    -33.6%
+ ~Mathlib.Algebra.Module.PID                                        instructions    -11.7%
+ ~Mathlib.Algebra.Quaternion                                        instructions     -5.0%
+ ~Mathlib.Algebra.RingQuot                                          instructions    -16.0%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                     instructions     -4.5%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions     17.6%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                          instructions     -5.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                         instructions    -22.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                           instructions     -5.8%
+ ~Mathlib.Analysis.Convolution                                      instructions     -2.8%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions     -9.4%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions     -6.5%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                          instructions     -2.5%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions     -7.9%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions     14.7%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions    -14.2%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions    -14.7%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions     -9.2%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions    -40.1%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                    instructions     -5.0%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                    instructions    -12.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions     -2.0%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions    -11.3%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions    -20.0%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions     -5.3%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions    -11.6%
+ ~Mathlib.Analysis.Seminorm                                         instructions     -7.2%
- ~Mathlib.CategoryTheory.Abelian.ProjectiveResolution               instructions      5.9%
+ ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions     -3.1%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                instructions     -9.8%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions     -3.7%
+ ~Mathlib.Data.Matrix.Rank                                          instructions    -13.7%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions     -5.0%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions     10.4%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions     -9.4%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions    -14.8%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions    -23.9%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions     -4.7%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions     -8.6%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions    -40.8%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions    -29.1%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions     -5.5%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions    -13.2%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions    -12.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions    -24.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions    -20.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions    -43.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions    -36.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions    -15.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions    -24.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions    -25.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions    -18.7%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions     -7.2%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions    -32.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions    -25.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions    -24.8%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions     -4.3%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions     -2.9%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions    -23.8%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions     -5.3%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions     -4.0%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions    -22.7%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions     -9.7%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions    -17.0%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions     -9.0%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions     -4.9%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions     -7.6%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions    -32.8%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions    -11.1%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions    -19.7%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions    -13.6%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions     -6.1%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions     -8.8%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions    -11.0%
+ ~Mathlib.RepresentationTheory.Rep                                  instructions     -4.9%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions     -3.4%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions     -9.7%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions    -13.4%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions    -13.1%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions    -22.5%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions    -25.3%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions     -5.3%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions    -14.3%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions     -5.7%
+ ~Mathlib.RingTheory.Kaehler                                        instructions     -2.9%
+ ~Mathlib.RingTheory.Norm                                           instructions     -9.9%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions    -29.4%
+ ~Mathlib.RingTheory.Perfection                                     instructions     -4.7%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions    -25.4%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions     -4.6%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions    -11.4%
+ ~Mathlib.RingTheory.Valuation.Basic                                instructions     -5.0%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions    -14.0%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField              instructions    -19.1%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions    -14.4%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                      instructions    -11.9%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions    -11.7%

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 68460b8.
There were significant changes against commit 0b290c7:

  Benchmark                                                          Metric          Change
  =========================================================================================
+ build                                                              type checking   -12.1%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions    -14.3%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions     -5.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions    -17.4%
+ ~Mathlib.Algebra.DirectLimit                                       instructions     -5.5%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions    -13.3%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions    -21.7%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions     -4.2%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions    -20.7%
+ ~Mathlib.Algebra.Lie.Killing                                       instructions    -11.2%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions    -33.6%
+ ~Mathlib.Algebra.Module.PID                                        instructions    -13.2%
+ ~Mathlib.Algebra.Quaternion                                        instructions     -5.0%
+ ~Mathlib.Algebra.RingQuot                                          instructions    -16.0%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                     instructions     -4.5%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties             instructions     -3.1%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions     17.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                          instructions     -5.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                         instructions    -22.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                           instructions     -5.7%
+ ~Mathlib.Analysis.Convolution                                      instructions     -2.8%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions     -9.4%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions     -6.5%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                          instructions     -2.5%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions     -7.9%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions     14.7%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions    -14.2%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions    -14.7%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions     -9.2%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions    -40.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                    instructions     -3.6%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                    instructions    -12.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions     -2.0%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions    -11.0%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions    -19.9%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions     -5.3%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions    -11.6%
+ ~Mathlib.Analysis.Seminorm                                         instructions     -7.2%
+ ~Mathlib.CategoryTheory.Abelian.ProjectiveResolution               instructions     -2.9%
+ ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions     -3.1%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                instructions     -9.7%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions     -3.7%
+ ~Mathlib.Data.Matrix.Rank                                          instructions    -13.7%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions     -5.0%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions     13.5%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions     -8.6%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions    -14.8%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions    -24.0%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions     -3.5%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions     -8.6%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions    -40.8%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions    -29.1%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions     -5.5%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions    -13.2%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions    -12.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions    -24.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions    -20.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions    -43.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions    -36.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions    -15.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions    -24.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions    -25.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions    -18.7%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions     -7.2%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions    -32.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions    -25.7%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions    -24.8%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions     -4.3%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions     -2.9%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions    -23.5%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions     -5.3%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions     -4.0%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions    -22.7%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions     -9.7%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions    -17.0%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions     -9.0%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions     -4.9%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions     -7.6%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions    -32.8%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions    -11.1%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions    -19.7%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions    -13.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions     -6.1%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions     -8.7%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions    -10.6%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution           instructions     -2.5%
+ ~Mathlib.RepresentationTheory.Rep                                  instructions     -4.9%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions     -3.2%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions     -9.8%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions    -13.5%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions    -13.1%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions    -22.5%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions    -25.4%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions     -5.4%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions    -14.3%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions     -5.7%
+ ~Mathlib.RingTheory.Kaehler                                        instructions     -3.1%
+ ~Mathlib.RingTheory.Norm                                           instructions     -9.9%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions    -29.5%
+ ~Mathlib.RingTheory.Perfection                                     instructions     -4.8%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions    -25.3%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions     -4.6%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions    -11.4%
+ ~Mathlib.RingTheory.Valuation.Basic                                instructions     -5.0%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions    -14.0%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField              instructions    -19.2%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions    -14.5%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                      instructions    -11.9%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions    -11.7%

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 291977a.
There were significant changes against commit 0b290c7:

  Benchmark                                                          Metric             Change
  ============================================================================================
+ build                                                              tactic execution    -5.5%
+ build                                                              type checking      -12.3%
+ lint                                                               wall-clock          -5.3%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization                    instructions       -14.3%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions        -5.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions       -17.4%
+ ~Mathlib.Algebra.DirectLimit                                       instructions        -5.5%
+ ~Mathlib.Algebra.DirectSum.Ring                                    instructions       -13.3%
+ ~Mathlib.Algebra.DualQuaternion                                    instructions       -21.7%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions        -4.2%
+ ~Mathlib.Algebra.Lie.DirectSum                                     instructions       -20.7%
+ ~Mathlib.Algebra.Lie.Killing                                       instructions       -11.2%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions       -33.6%
+ ~Mathlib.Algebra.Module.PID                                        instructions       -13.1%
+ ~Mathlib.Algebra.Quaternion                                        instructions        -5.0%
+ ~Mathlib.Algebra.RingQuot                                          instructions       -16.0%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group                     instructions        -4.5%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties             instructions        -3.2%
- ~Mathlib.AlgebraicGeometry.Properties                              instructions        17.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic                          instructions        -5.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds                         instructions       -22.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs                           instructions        -5.8%
+ ~Mathlib.Analysis.Convolution                                      instructions        -2.8%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions        -9.4%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions        -6.5%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                          instructions        -2.5%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions        -7.9%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions        14.7%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms                      instructions       -14.2%
+ ~Mathlib.Analysis.Normed.Field.Basic                               instructions       -14.7%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension                      instructions        -9.2%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential                    instructions       -40.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                    instructions        -5.0%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                    instructions       -12.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions        -2.0%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions       -11.0%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions       -19.9%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions        -5.3%
+ ~Mathlib.Analysis.NormedSpace.lpSpace                              instructions       -11.6%
+ ~Mathlib.Analysis.Seminorm                                         instructions        -7.2%
+ ~Mathlib.CategoryTheory.Abelian.ProjectiveResolution               instructions        -2.9%
+ ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions        -3.1%
+ ~Mathlib.CategoryTheory.Sites.Sheaf                                instructions        -9.9%
+ ~Mathlib.Data.IsROrC.Basic                                         instructions        -3.7%
+ ~Mathlib.Data.Matrix.Rank                                          instructions       -13.7%
+ ~Mathlib.Data.MvPolynomial.Basic                                   instructions        -5.0%
- ~Mathlib.FieldTheory.AbelRuffini                                   instructions        13.5%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions        -9.2%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions       -14.9%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions       -24.0%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions        -3.6%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions        -8.6%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions       -40.8%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions       -29.1%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions        -5.5%
+ ~Mathlib.LinearAlgebra.AdicCompletion                              instructions       -13.2%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination                     instructions       -12.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions       -24.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions       -20.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions       -43.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions       -36.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs                      instructions       -15.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions       -24.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions       -25.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions       -18.7%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions        -7.2%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic                       instructions       -32.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions       -25.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions       -24.8%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions        -4.3%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm                     instructions        -2.9%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum                             instructions       -23.5%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin                                instructions        -5.3%
+ ~Mathlib.MeasureTheory.Constructions.Pi                            instructions        -4.0%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions       -22.7%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions        -9.7%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions       -17.0%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp                  instructions        -9.0%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions        -4.8%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions        -7.6%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure                       instructions       -32.8%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions       -11.1%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions       -19.7%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions       -13.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions        -6.1%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions        -8.7%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions       -10.6%
+ ~Mathlib.RepresentationTheory.Rep                                  instructions        -4.9%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions        -3.2%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions        -9.8%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions       -13.5%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions       -13.0%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions       -22.5%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal                 instructions       -25.3%
+ ~Mathlib.RingTheory.HahnSeries                                     instructions        -5.4%
+ ~Mathlib.RingTheory.Ideal.Quotient                                 instructions       -14.3%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations                       instructions        -5.7%
+ ~Mathlib.RingTheory.Kaehler                                        instructions        -3.1%
+ ~Mathlib.RingTheory.Norm                                           instructions        -9.9%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions       -29.5%
+ ~Mathlib.RingTheory.Perfection                                     instructions        -4.8%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions       -25.3%
+ ~Mathlib.RingTheory.PowerSeries.Basic                              instructions        -4.6%
+ ~Mathlib.RingTheory.Subring.Basic                                  instructions       -11.4%
+ ~Mathlib.RingTheory.Valuation.Basic                                instructions        -5.0%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions       -13.9%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField              instructions       -19.2%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                          instructions       -14.5%
+ ~Mathlib.Topology.Category.Profinite.Nobeling                      instructions       -11.9%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions       -11.7%

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Dec 14, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 22, 2023
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
0073d72
@semorrison
merge master
5848873
@semorrison
update per PR
0c932db
@semorrison
Merge branch 'nightly-testing' of github.com:leanprover-community/mat…
ff7cb13 
…hlib4 into nightly-testing
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
1672e1c
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
6482fe9
@leanprover-community-mathlib4-bot
chore: bump to nightly-2024-01-30
ed24a46
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
a330570
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
2035ac1
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
6ea9050
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
b2b320d
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
2d9d9e5
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
ad2d572
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
0d6b65a
@leanprover-community-mathlib4-bot
chore: bump to nightly-2024-01-31
f5635a6
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
cff5fc4
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
7c23494
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
f906b94
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
b9729c6
@leanprover-community-mathlib4-bot
Merge master into nightly-testing
ee6bba4
@mattrobball
Merge branch 'nightly-testing' into mrb/left_right
37f3a0e
@mergify Mergify
Copy link

mergify bot commented Feb 1, 2024

⚠️ The sha of the head commit of this PR conflicts with #9843. Mergify cannot evaluate rules on this PR. ⚠️

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 1, 2024
@mergify Mergify
Copy link

mergify bot commented Feb 1, 2024

⚠️ The sha of the head commit of this PR conflicts with #9843. Mergify cannot evaluate rules on this PR. ⚠️

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 2, 2024
@mergify Mergify
Copy link

mergify bot commented Feb 8, 2024

⚠️ The sha of the head commit of this PR conflicts with #9843. Mergify cannot evaluate rules on this PR. ⚠️

@mattrobball mattrobball closed this Feb 8, 2024
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
merge-conflict The PR has a merge conflict with master, and needs manual merging.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
9 participants
@mattrobball @leanprover-bot @leanprover-community-mathlib4-bot @semorrison @mhuisi @fgdorais @nomeata @kmill @joehendrix