Skip to content

chore: changes for leanprover/lean4#2478#9007

Closed
mattrobball wants to merge 2063 commits intonightly-testingfrom
lean-pr-testing-2478
Closed

chore: changes for leanprover/lean4#2478#9007
mattrobball wants to merge 2063 commits intonightly-testingfrom
lean-pr-testing-2478

Conversation

@mattrobball
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball commented Dec 12, 2023 •
edited
Loading

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

Open in Gitpod

@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 Dec 12, 2023
@mattrobball mattrobball mentioned this pull request Dec 12, 2023
Merged
@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Dec 12, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 12, 2023

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

mattrobball commented Dec 13, 2023 •
edited
Loading

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.

@ghost ghost added blocked-by-other-PR This PR depends on another PR (this label is automatically 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 Dec 14, 2023
@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Dec 14, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 14, 2023

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

mattrobball commented Dec 14, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 14, 2023

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

mattrobball commented Dec 14, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 14, 2023

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

mattrobball commented Dec 14, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 14, 2023

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

mattrobball commented Dec 14, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 14, 2023

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

mattrobball commented Dec 14, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 14, 2023

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

mattrobball commented Dec 14, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Dec 14, 2023

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%

@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 14, 2023
@ghost
Copy link
Copy Markdown

ghost commented Dec 14, 2023

This PR/issue depends on:

@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 Dec 22, 2023
leanprover-community-mathlib4-bot and others added 2 commits January 10, 2024 09:31
kim-em and others added 20 commits January 30, 2024 13:39
@kim-em
merge master
5848873
@kim-em
update per PR
0c932db
@kim-em
Merge branch 'nightly-testing' of github.com:leanprover-community/mat…
ff7cb13 
…hlib4 into nightly-testing
Merge master into nightly-testing
1672e1c
Merge master into nightly-testing
6482fe9
chore: bump to nightly-2024-01-30
ed24a46
Merge master into nightly-testing
a330570
Merge master into nightly-testing
2035ac1
Merge master into nightly-testing
6ea9050
Merge master into nightly-testing
b2b320d
Merge master into nightly-testing
2d9d9e5
Merge master into nightly-testing
ad2d572
Merge master into nightly-testing
0d6b65a
chore: bump to nightly-2024-01-31
f5635a6
Merge master into nightly-testing
cff5fc4
Merge master into nightly-testing
7c23494
Merge master into nightly-testing
f906b94
Merge master into nightly-testing
b9729c6
Merge master into nightly-testing
ee6bba4
@mattrobball
Merge branch 'nightly-testing' into mrb/left_right
37f3a0e
@kim-em kim-em force-pushed the lean-pr-testing-2478 branch from 7cc0fc5 to 37f3a0e Compare February 1, 2024 01:50
@mergify
Copy link
Copy Markdown

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. ⚠️

@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 Feb 1, 2024
@mergify
Copy link
Copy Markdown

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. ⚠️

@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 Feb 2, 2024
@mergify
Copy link
Copy Markdown

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
@YaelDillies YaelDillies deleted the lean-pr-testing-2478 branch August 12, 2025 05:40
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. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@mattrobball @leanprover-bot @kim-em @mhuisi @fgdorais @nomeata @kmill