mathlib4
mathlib4 copied to clipboard
Published
20 hours ago •
leanprover-community
leanprover-community
Lean pr testing 4272
Here are the benchmark results for commit ee8fec761e6eaec871f5adc5f32fbf24bb5aa177. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
========================================================================================================
+ build linting -6.0%
+ build task-clock -6.0%
+ build typeclass inference -17.2%
+ build wall-clock -6.8%
+ lint wall-clock -5.2%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -14.1%
+ ~Mathlib.Algebra.Algebra.Quasispectrum instructions -16.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -17.1%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -24.7%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -29.5%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -12.0%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -14.5%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -12.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -11.7%
+ ~Mathlib.Algebra.Order.Module.Defs instructions -17.0%
+ ~Mathlib.Algebra.Order.ToIntervalMod instructions -18.7%
+ ~Mathlib.Algebra.Polynomial.Module.Basic instructions -9.1%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -14.7%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -20.8%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -26.7%
+ ~Mathlib.Analysis.Analytic.Basic instructions -10.0%
+ ~Mathlib.Analysis.Analytic.CPolynomial instructions -11.9%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -9.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -10.4%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds instructions -7.1%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -10.4%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -14.0%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -9.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions -10.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Measurable instructions -12.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -10.3%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -11.8%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -24.2%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -14.7%
+ ~Mathlib.Analysis.Calculus.LineDeriv.Basic instructions -16.1%
+ ~Mathlib.Analysis.Calculus.Rademacher instructions -16.8%
+ ~Mathlib.Analysis.Convex.Function instructions -31.7%
+ ~Mathlib.Analysis.Convex.Gauge instructions -15.4%
+ ~Mathlib.Analysis.Convex.Jensen instructions -19.7%
+ ~Mathlib.Analysis.Convex.Mul instructions -15.0%
+ ~Mathlib.Analysis.Convex.Segment instructions -20.0%
+ ~Mathlib.Analysis.Convolution instructions -10.8%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -8.0%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -10.0%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -8.3%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -21.6%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -9.9%
+ ~Mathlib.Analysis.NormedSpace.BallAction instructions -21.9%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -13.6%
+ ~Mathlib.Analysis.NormedSpace.MStructure instructions -30.1%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -13.4%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -12.6%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -17.9%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -18.2%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Prod instructions -14.6%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions -5.2%
+ ~Mathlib.Analysis.NormedSpace.SphereNormEquiv instructions -41.6%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances instructions -9.3%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -12.0%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -20.5%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -6.9%
+ ~Mathlib.Analysis.Seminorm instructions -15.3%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -9.1%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -20.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.3%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.9%
+ ~Mathlib.Data.Finset.Pointwise instructions -9.0%
+ ~Mathlib.Data.Matrix.Basic instructions -14.2%
+ ~Mathlib.Data.Num.Lemmas instructions -15.7%
+ ~Mathlib.Data.Set.Pointwise.Interval instructions -15.4%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -10.4%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -14.9%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -6.7%
+ ~Mathlib.GroupTheory.HNNExtension instructions -8.9%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -12.0%
+ ~Mathlib.GroupTheory.PushoutI instructions -17.5%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -16.2%
+ ~Mathlib.LinearAlgebra.Dual instructions -4.6%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -10.0%
+ ~Mathlib.LinearAlgebra.LinearPMap instructions -8.9%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -26.6%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -21.0%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions -9.0%
+ ~Mathlib.LinearAlgebra.Ray instructions -17.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -8.1%
+ ~Mathlib.LinearAlgebra.TensorProduct.Graded.External instructions -3.4%
+ ~Mathlib.LinearAlgebra.TensorProduct.RightExactness instructions -7.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -20.4%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -10.2%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -8.2%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -10.1%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -18.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -9.2%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -9.5%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -7.8%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -17.9%
+ ~Mathlib.MeasureTheory.Measure.Haar.Unique instructions -16.3%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -16.7%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -9.7%
+ ~Mathlib.RepresentationTheory.GroupCohomology.LowDegree instructions -8.3%
+ ~Mathlib.RingTheory.Derivation.Basic instructions -15.4%
+ ~Mathlib.RingTheory.IntegralRestrict instructions -6.5%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -15.8%
+ ~Mathlib.RingTheory.Kaehler instructions -8.7%
+ ~Mathlib.RingTheory.Localization.Basic instructions -11.4%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -7.6%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -16.0%
+ ~Mathlib.Topology.Algebra.Group.Basic instructions -15.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -8.5%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -12.1%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -10.2%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -9.3%
+ ~Mathlib.Topology.Homotopy.Path instructions -15.3%
!bench
Wow, that last run was really fast 🏎️ Hopefully this one is even faster
Here are the benchmark results for commit c6b57e963c89481d25175c5d633025b9fbaf1375. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
========================================================================================================
+ build task-clock -5.3%
+ build typeclass inference -16.8%
+ lint wall-clock -5.1%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -14.0%
+ ~Mathlib.Algebra.Algebra.Quasispectrum instructions -16.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -17.1%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -25.2%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -29.4%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -12.2%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -14.4%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -12.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -11.7%
+ ~Mathlib.Algebra.Order.Module.Defs instructions -17.0%
+ ~Mathlib.Algebra.Order.ToIntervalMod instructions -18.7%
+ ~Mathlib.Algebra.Polynomial.Module.Basic instructions -9.1%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -14.6%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -20.8%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -26.7%
+ ~Mathlib.Analysis.Analytic.Basic instructions -10.0%
+ ~Mathlib.Analysis.Analytic.CPolynomial instructions -11.9%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -9.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -10.4%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds instructions -7.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -10.4%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -13.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -9.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions -10.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Measurable instructions -12.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -10.2%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -11.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -24.2%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -15.2%
+ ~Mathlib.Analysis.Calculus.LineDeriv.Basic instructions -16.0%
+ ~Mathlib.Analysis.Calculus.Rademacher instructions -16.8%
+ ~Mathlib.Analysis.Convex.Function instructions -31.6%
+ ~Mathlib.Analysis.Convex.Gauge instructions -15.4%
+ ~Mathlib.Analysis.Convex.Jensen instructions -19.7%
+ ~Mathlib.Analysis.Convex.Mul instructions -15.0%
+ ~Mathlib.Analysis.Convex.Segment instructions -19.9%
+ ~Mathlib.Analysis.Convolution instructions -10.8%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -7.9%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -10.2%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -8.3%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -21.6%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -9.9%
+ ~Mathlib.Analysis.NormedSpace.BallAction instructions -21.9%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -13.5%
+ ~Mathlib.Analysis.NormedSpace.MStructure instructions -30.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -13.3%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -12.6%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -17.8%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -18.2%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Prod instructions -14.6%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions -5.5%
+ ~Mathlib.Analysis.NormedSpace.SphereNormEquiv instructions -41.6%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances instructions -9.3%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -12.0%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -20.5%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -6.9%
+ ~Mathlib.Analysis.Seminorm instructions -15.4%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -9.1%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -20.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.3%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.9%
+ ~Mathlib.Data.Finset.Pointwise instructions -9.0%
+ ~Mathlib.Data.Matrix.Basic instructions -14.4%
+ ~Mathlib.Data.Num.Lemmas instructions -15.5%
+ ~Mathlib.Data.Set.Pointwise.Interval instructions -15.4%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -10.3%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -14.8%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -6.7%
+ ~Mathlib.GroupTheory.HNNExtension instructions -8.9%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -12.0%
+ ~Mathlib.GroupTheory.PushoutI instructions -17.5%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -16.1%
+ ~Mathlib.LinearAlgebra.Dual instructions -4.6%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -10.0%
+ ~Mathlib.LinearAlgebra.LinearPMap instructions -8.8%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -28.4%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -21.2%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions -9.0%
+ ~Mathlib.LinearAlgebra.Ray instructions -17.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -8.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Graded.External instructions -3.4%
+ ~Mathlib.LinearAlgebra.TensorProduct.RightExactness instructions -7.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -20.4%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -10.2%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -8.2%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -10.2%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -18.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -9.2%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -9.4%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -7.8%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -17.9%
+ ~Mathlib.MeasureTheory.Measure.Haar.Unique instructions -16.3%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -16.7%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -9.8%
+ ~Mathlib.RepresentationTheory.GroupCohomology.LowDegree instructions -8.2%
+ ~Mathlib.RingTheory.Derivation.Basic instructions -15.4%
+ ~Mathlib.RingTheory.IntegralRestrict instructions -6.5%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -15.8%
+ ~Mathlib.RingTheory.Kaehler instructions -8.8%
+ ~Mathlib.RingTheory.Localization.Basic instructions -11.5%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -7.6%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -16.0%
+ ~Mathlib.Topology.Algebra.Group.Basic instructions -15.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -8.5%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -12.1%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -10.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -9.3%
+ ~Mathlib.Topology.Homotopy.Path instructions -17.2%
Here are the benchmark results for commit 9c70cea4a1f565ce854d256660cc093e9afb1898. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
======================================================================
+ ~Mathlib.Analysis.Convex.Function instructions -15.7%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -15.2%
+ ~Mathlib.CategoryTheory.Limits.Shapes.Diagonal instructions -3.4%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -16.9%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -9.5%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -14.3%
Here are the benchmark results for commit 1da642dd126dfeade23a2e61c00a9e895ac19ea2. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
========================================================================================================
+ build instructions -5.1%
+ build task-clock -5.5%
+ build typeclass inference -17.0%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -14.0%
+ ~Mathlib.Algebra.Algebra.Quasispectrum instructions -16.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -17.0%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -25.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -29.5%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -6.1%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -12.2%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -14.4%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -12.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -11.7%
+ ~Mathlib.Algebra.Order.Module.Defs instructions -17.0%
+ ~Mathlib.Algebra.Order.ToIntervalMod instructions -18.7%
+ ~Mathlib.Algebra.Polynomial.Module.Basic instructions -15.9%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -14.7%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -20.7%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -26.7%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions -7.7%
+ ~Mathlib.Analysis.Analytic.Basic instructions -10.0%
+ ~Mathlib.Analysis.Analytic.CPolynomial instructions -11.9%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -9.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -10.5%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds instructions -7.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -10.4%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -13.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -9.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions -10.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Measurable instructions -12.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -10.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -11.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -24.2%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -15.2%
+ ~Mathlib.Analysis.Calculus.LineDeriv.Basic instructions -16.0%
+ ~Mathlib.Analysis.Calculus.Rademacher instructions -16.8%
+ ~Mathlib.Analysis.Convex.Function instructions -31.6%
+ ~Mathlib.Analysis.Convex.Gauge instructions -15.3%
+ ~Mathlib.Analysis.Convex.Jensen instructions -19.6%
+ ~Mathlib.Analysis.Convex.Mul instructions -15.0%
+ ~Mathlib.Analysis.Convex.Segment instructions -19.9%
+ ~Mathlib.Analysis.Convolution instructions -10.7%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -7.9%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -10.2%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -8.3%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -21.6%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -9.9%
+ ~Mathlib.Analysis.NormedSpace.BallAction instructions -21.9%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -13.7%
+ ~Mathlib.Analysis.NormedSpace.MStructure instructions -30.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -13.3%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -12.6%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -17.8%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -18.2%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Prod instructions -14.7%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions -6.5%
+ ~Mathlib.Analysis.NormedSpace.SphereNormEquiv instructions -41.6%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances instructions -9.3%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -12.4%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -20.5%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -7.0%
+ ~Mathlib.Analysis.Seminorm instructions -15.3%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -9.1%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -20.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.4%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.9%
+ ~Mathlib.Data.Finset.Pointwise instructions -9.0%
+ ~Mathlib.Data.Matrix.Basic instructions -14.4%
+ ~Mathlib.Data.Num.Lemmas instructions -15.8%
+ ~Mathlib.Data.Set.Pointwise.Interval instructions -15.3%
+ ~Mathlib.FieldTheory.KummerExtension instructions -8.9%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -10.3%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -14.8%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -6.7%
+ ~Mathlib.GroupTheory.HNNExtension instructions -9.1%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -12.0%
+ ~Mathlib.GroupTheory.PushoutI instructions -18.4%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -16.1%
+ ~Mathlib.LinearAlgebra.Dual instructions -4.6%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -10.1%
+ ~Mathlib.LinearAlgebra.LinearPMap instructions -8.8%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -28.4%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -21.2%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic instructions -6.8%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions -9.1%
+ ~Mathlib.LinearAlgebra.Ray instructions -17.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -8.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Graded.External instructions -3.4%
+ ~Mathlib.LinearAlgebra.TensorProduct.RightExactness instructions -7.6%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -20.4%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -10.2%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -8.7%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -12.5%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -18.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -9.3%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -9.4%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -7.9%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -17.9%
+ ~Mathlib.MeasureTheory.Measure.Haar.Unique instructions -16.3%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -16.7%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -10.0%
+ ~Mathlib.RepresentationTheory.GroupCohomology.LowDegree instructions -8.2%
+ ~Mathlib.RingTheory.Derivation.Basic instructions -15.4%
+ ~Mathlib.RingTheory.IntegralRestrict instructions -7.9%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -15.8%
+ ~Mathlib.RingTheory.Kaehler instructions -9.4%
+ ~Mathlib.RingTheory.Localization.Basic instructions -11.7%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -7.9%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -16.1%
+ ~Mathlib.Topology.Algebra.Group.Basic instructions -15.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -8.6%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -12.0%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -10.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -9.3%
+ ~Mathlib.Topology.Homotopy.Path instructions -17.2%
!bench
The improvement here is that the canonical instance optimization is applies more often.
Here are the benchmark results for commit 19e89728de7de4194b5abc82e7e2c7ec79f91521. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
========================================================================================================
+ build instructions -5.1%
+ build task-clock -5.4%
+ build typeclass inference -16.2%
+ lint wall-clock -5.7%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -14.0%
+ ~Mathlib.Algebra.Algebra.Quasispectrum instructions -16.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -17.0%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -25.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -29.5%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -6.1%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -12.2%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -14.4%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -12.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -11.7%
+ ~Mathlib.Algebra.Order.Module.Defs instructions -17.0%
+ ~Mathlib.Algebra.Order.ToIntervalMod instructions -18.7%
+ ~Mathlib.Algebra.Polynomial.Module.Basic instructions -16.4%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -14.6%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -20.7%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -26.7%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions -7.7%
+ ~Mathlib.Analysis.Analytic.Basic instructions -10.0%
+ ~Mathlib.Analysis.Analytic.CPolynomial instructions -11.9%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -9.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -10.5%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds instructions -7.2%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -10.4%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -13.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -9.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions -10.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Measurable instructions -12.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -10.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -11.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -24.2%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -15.2%
+ ~Mathlib.Analysis.Calculus.LineDeriv.Basic instructions -16.0%
+ ~Mathlib.Analysis.Calculus.Rademacher instructions -16.8%
+ ~Mathlib.Analysis.Convex.Function instructions -31.6%
+ ~Mathlib.Analysis.Convex.Gauge instructions -15.3%
+ ~Mathlib.Analysis.Convex.Jensen instructions -19.6%
+ ~Mathlib.Analysis.Convex.Mul instructions -15.0%
+ ~Mathlib.Analysis.Convex.Segment instructions -19.9%
+ ~Mathlib.Analysis.Convolution instructions -10.7%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -7.9%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -10.2%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -8.3%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -21.6%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -9.9%
+ ~Mathlib.Analysis.NormedSpace.BallAction instructions -21.9%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -13.7%
+ ~Mathlib.Analysis.NormedSpace.MStructure instructions -30.1%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -13.3%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -12.6%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -17.8%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -18.2%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Prod instructions -14.7%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions -6.5%
+ ~Mathlib.Analysis.NormedSpace.SphereNormEquiv instructions -41.6%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances instructions -9.3%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -12.4%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -20.5%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -7.0%
+ ~Mathlib.Analysis.Seminorm instructions -15.3%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -9.1%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -20.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.4%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.9%
+ ~Mathlib.Data.Finset.Pointwise instructions -9.0%
+ ~Mathlib.Data.Matrix.Basic instructions -14.4%
+ ~Mathlib.Data.Num.Lemmas instructions -15.8%
+ ~Mathlib.Data.Set.Pointwise.Interval instructions -15.3%
+ ~Mathlib.FieldTheory.KummerExtension instructions -8.9%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -10.3%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -14.8%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -6.7%
+ ~Mathlib.GroupTheory.HNNExtension instructions -9.1%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -12.0%
+ ~Mathlib.GroupTheory.PushoutI instructions -18.4%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -16.1%
+ ~Mathlib.LinearAlgebra.Dual instructions -4.6%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -10.1%
+ ~Mathlib.LinearAlgebra.LinearPMap instructions -8.8%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -28.4%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -21.2%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic instructions -6.7%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions -9.2%
+ ~Mathlib.LinearAlgebra.Ray instructions -17.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -8.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Graded.External instructions -3.4%
+ ~Mathlib.LinearAlgebra.TensorProduct.RightExactness instructions -7.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -20.4%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -10.2%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -8.6%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -12.5%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -18.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -9.3%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -9.4%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -7.9%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -17.9%
+ ~Mathlib.MeasureTheory.Measure.Haar.Unique instructions -16.3%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -16.7%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -10.4%
+ ~Mathlib.RepresentationTheory.GroupCohomology.LowDegree instructions -8.2%
+ ~Mathlib.RingTheory.DedekindDomain.Different instructions -6.6%
+ ~Mathlib.RingTheory.Derivation.Basic instructions -15.4%
+ ~Mathlib.RingTheory.IntegralRestrict instructions -7.9%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -15.8%
+ ~Mathlib.RingTheory.Kaehler instructions -9.6%
+ ~Mathlib.RingTheory.Localization.Basic instructions -11.6%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -8.2%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -16.1%
+ ~Mathlib.Topology.Algebra.Group.Basic instructions -15.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -8.5%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -12.0%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -10.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -9.3%
+ ~Mathlib.Topology.Homotopy.Path instructions -17.2%
Some more statistics (extracted from the last comparison):
lint: -463.96 * 10⁹ (-3.80%)
build: -6036.9 * 10⁹ (-5.10%)
Files that got slower:
Mathlib.CategoryTheory.Preadditive.EilenbergMoore: +8.1559 * 10⁹ (+3.44%)
Mathlib.RepresentationTheory.Action.Basic: +3.9758 * 10⁹ (+2.86%)
Mathlib.CategoryTheory.DifferentialObject: +1.5048 * 10⁹ (+1.11%)
Mathlib.RingTheory.Noetherian: +1.4284 * 10⁹ (+1.43%)
Mathlib.CategoryTheory.Category.Cat.Limit: +1.4264 * 10⁹ (+1.43%)
Mathlib.CategoryTheory.Monoidal.Discrete: +1.0840 * 10⁹ (+0.964%)
And there are 1127(!) Mathlib files that got faster by at least 10⁹ instructions. I won't paste the complete list; it starts with
Files that got faster:
Mathlib.Algebra.Star.NonUnitalSubalgebra: -74.055 * 10⁹ (-20.7%)
Mathlib.CategoryTheory.Monoidal.Braided.Basic: -53.659 * 10⁹ (-20.4%)
Mathlib.CategoryTheory.Bicategory.Adjunction: -49.013 * 10⁹ (-20.0%)
Mathlib.RingTheory.Kaehler: -47.704 * 10⁹ (-9.59%)
Mathlib.Analysis.NormedSpace.Multilinear.Basic: -47.664 * 10⁹ (-13.3%)
Mathlib.Analysis.Calculus.ContDiff.Basic: -46.439 * 10⁹ (-10.5%)
Mathlib.Analysis.Calculus.FDeriv.Mul: -46.255 * 10⁹ (-10.7%)
Mathlib.Algebra.TrivSqZeroExt: -44.136 * 10⁹ (-26.7%)
Mathlib.LinearAlgebra.TensorProduct.Tower: -43.443 * 10⁹ (-20.3%)
Mathlib.Analysis.Convolution: -40.219 * 10⁹ (-10.7%)
Mathlib.Analysis.Calculus.ContDiff.Defs: -36.745 * 10⁹ (-10.4%)
Mathlib.Analysis.Convex.Function: -33.361 * 10⁹ (-31.6%)
Mathlib.LinearAlgebra.Matrix.ToLin: -32.998 * 10⁹ (-21.2%)
Mathlib.NumberTheory.RamificationInertia: -31.936 * 10⁹ (-10.4%)
Mathlib.Analysis.NormedSpace.TrivSqZeroExt: -29.778 * 10⁹ (-20.5%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear: -29.611 * 10⁹ (-18.2%)
Mathlib.Geometry.Manifold.ContMDiff.NormedSpace: -29.223 * 10⁹ (-14.8%)
Mathlib.Algebra.Lie.Weights.Killing: -28.422 * 10⁹ (-12.2%)
Mathlib.Analysis.Analytic.Basic: -28.004 * 10⁹ (-9.98%)
Mathlib.CategoryTheory.Monoidal.Rigid.Basic: -27.757 * 10⁹ (-10.9%)
Mathlib.Analysis.Seminorm: -26.623 * 10⁹ (-15.3%)
Mathlib.Analysis.NormedSpace.Multilinear.Curry: -26.365 * 10⁹ (-12.6%)
Mathlib.LinearAlgebra.Matrix.SchurComplement: -26.122 * 10⁹ (-28.4%)
Mathlib.Algebra.Module.LocalizedModule: -25.112 * 10⁹ (-12.1%)
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings: -24.818 * 10⁹ (-6.06%)
Mathlib.MeasureTheory.Integral.SetToL1: -24.242 * 10⁹ (-7.87%)
Mathlib.Algebra.Algebra.NonUnitalSubalgebra: -23.699 * 10⁹ (-14.0%)
Mathlib.Analysis.NormedSpace.Star.Multiplier: -23.057 * 10⁹ (-12.4%)
Mathlib.RingTheory.TensorProduct.Basic: -22.828 * 10⁹ (-8.19%)
Mathlib.Topology.Algebra.Module.Basic: -22.688 * 10⁹ (-8.52%)
Mathlib.MeasureTheory.Integral.Bochner: -22.354 * 10⁹ (-9.30%)
Mathlib.Analysis.InnerProductSpace.Projection: -22.142 * 10⁹ (-9.88%)
Mathlib.Analysis.InnerProductSpace.Basic: -21.738 * 10⁹ (-8.30%)
Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus:
-21.322 * 10⁹ (-10.1%)
Mathlib.Analysis.Fourier.FourierTransformDeriv: -21.042 * 10⁹ (-10.2%)
Mathlib.LinearAlgebra.TensorProduct.Basic: -20.725 * 10⁹ (-7.99%)
Mathlib.Analysis.Calculus.FDeriv.Symmetric: -20.608 * 10⁹ (-24.2%)
Mathlib.Algebra.Algebra.Unitization: -20.381 * 10⁹ (-25.3%)
(these are the ones with a difference of at least 20*10⁹ instructions).
Here are the benchmark results for commit fa6377ad55d15fbb165437cc74d6ae552b0ff9c6. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
========================================================================================================
+ build instructions -5.1%
+ build task-clock -6.2%
+ build typeclass inference -18.0%
+ build wall-clock -5.9%
+ lint wall-clock -5.9%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -14.0%
+ ~Mathlib.Algebra.Algebra.Quasispectrum instructions -16.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -17.1%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -25.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -29.5%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -6.1%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -12.2%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -14.4%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -12.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -11.7%
+ ~Mathlib.Algebra.Order.Module.Defs instructions -17.0%
+ ~Mathlib.Algebra.Order.ToIntervalMod instructions -18.7%
+ ~Mathlib.Algebra.Polynomial.Module.Basic instructions -15.9%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -14.6%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -20.7%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -26.7%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions -7.7%
+ ~Mathlib.Analysis.Analytic.Basic instructions -10.0%
+ ~Mathlib.Analysis.Analytic.CPolynomial instructions -11.9%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -9.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -10.5%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds instructions -7.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -10.4%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -13.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -9.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions -10.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Measurable instructions -12.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -10.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -11.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -24.2%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -15.2%
+ ~Mathlib.Analysis.Calculus.LineDeriv.Basic instructions -16.0%
+ ~Mathlib.Analysis.Calculus.Rademacher instructions -16.8%
+ ~Mathlib.Analysis.Convex.Function instructions -31.6%
+ ~Mathlib.Analysis.Convex.Gauge instructions -15.3%
+ ~Mathlib.Analysis.Convex.Jensen instructions -19.6%
+ ~Mathlib.Analysis.Convex.Mul instructions -15.0%
+ ~Mathlib.Analysis.Convex.Segment instructions -19.9%
+ ~Mathlib.Analysis.Convolution instructions -10.7%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -7.9%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -10.2%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -8.3%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -21.5%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -9.9%
+ ~Mathlib.Analysis.NormedSpace.BallAction instructions -21.9%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -13.7%
+ ~Mathlib.Analysis.NormedSpace.MStructure instructions -30.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -13.4%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -12.6%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -17.8%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -18.2%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Prod instructions -14.6%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions -7.2%
+ ~Mathlib.Analysis.NormedSpace.SphereNormEquiv instructions -41.6%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances instructions -9.3%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -12.4%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -20.5%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -7.0%
+ ~Mathlib.Analysis.Seminorm instructions -15.3%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -9.1%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -20.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.4%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.9%
+ ~Mathlib.Data.Finset.Pointwise instructions -9.0%
+ ~Mathlib.Data.Matrix.Basic instructions -14.4%
+ ~Mathlib.Data.Num.Lemmas instructions -15.7%
+ ~Mathlib.Data.Set.Pointwise.Interval instructions -15.3%
+ ~Mathlib.FieldTheory.KummerExtension instructions -8.9%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -10.3%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -14.8%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -6.7%
+ ~Mathlib.GroupTheory.HNNExtension instructions -9.1%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -12.0%
+ ~Mathlib.GroupTheory.PushoutI instructions -18.4%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -16.1%
+ ~Mathlib.LinearAlgebra.Dual instructions -4.6%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -10.1%
+ ~Mathlib.LinearAlgebra.LinearPMap instructions -8.8%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -28.4%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -21.2%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic instructions -6.8%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions -9.1%
+ ~Mathlib.LinearAlgebra.Ray instructions -17.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -8.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Graded.External instructions -3.4%
+ ~Mathlib.LinearAlgebra.TensorProduct.RightExactness instructions -7.6%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -20.4%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -10.2%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -8.6%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -12.5%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -18.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -9.3%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -9.4%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -7.9%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -17.9%
+ ~Mathlib.MeasureTheory.Measure.Haar.Unique instructions -16.3%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -16.7%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -10.0%
+ ~Mathlib.RepresentationTheory.GroupCohomology.LowDegree instructions -8.2%
+ ~Mathlib.RingTheory.Derivation.Basic instructions -15.4%
+ ~Mathlib.RingTheory.IntegralRestrict instructions -7.9%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -15.8%
+ ~Mathlib.RingTheory.Kaehler instructions -9.4%
+ ~Mathlib.RingTheory.Localization.Basic instructions -11.7%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -7.9%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -16.1%
+ ~Mathlib.Topology.Algebra.Group.Basic instructions -15.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -8.6%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -12.0%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -10.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -9.3%
+ ~Mathlib.Topology.Homotopy.Path instructions -17.2%
!bench
I now properly did the loop detection. But it should give at most a very small improvement.
Here are the benchmark results for commit fcef64eb535f8f9bf96b6c4931684255c3902967. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
========================================================================================================
+ build instructions -5.1%
+ build typeclass inference -15.3%
+ lint wall-clock -5.9%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -14.1%
+ ~Mathlib.Algebra.Algebra.Quasispectrum instructions -16.2%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -17.1%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -25.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -29.6%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -6.1%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -12.2%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -14.4%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -12.2%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -11.8%
+ ~Mathlib.Algebra.Order.Module.Defs instructions -17.0%
+ ~Mathlib.Algebra.Order.ToIntervalMod instructions -18.7%
+ ~Mathlib.Algebra.Polynomial.Module.Basic instructions -16.0%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -14.7%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -20.8%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -26.8%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions -7.7%
+ ~Mathlib.Analysis.Analytic.Basic instructions -10.0%
+ ~Mathlib.Analysis.Analytic.CPolynomial instructions -11.9%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -9.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -10.5%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds instructions -7.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -10.4%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -13.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -9.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions -10.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Measurable instructions -12.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -10.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -11.8%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -24.2%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -15.2%
+ ~Mathlib.Analysis.Calculus.LineDeriv.Basic instructions -16.1%
+ ~Mathlib.Analysis.Calculus.Rademacher instructions -16.8%
+ ~Mathlib.Analysis.Convex.Function instructions -31.7%
+ ~Mathlib.Analysis.Convex.Gauge instructions -15.4%
+ ~Mathlib.Analysis.Convex.Jensen instructions -19.7%
+ ~Mathlib.Analysis.Convex.Mul instructions -15.0%
+ ~Mathlib.Analysis.Convex.Segment instructions -20.0%
+ ~Mathlib.Analysis.Convolution instructions -10.8%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -8.0%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -10.2%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -8.3%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -21.6%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -9.9%
+ ~Mathlib.Analysis.NormedSpace.BallAction instructions -21.9%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -13.7%
+ ~Mathlib.Analysis.NormedSpace.MStructure instructions -30.3%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -13.3%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -12.6%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -17.8%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -18.2%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Prod instructions -14.7%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions -6.4%
+ ~Mathlib.Analysis.NormedSpace.SphereNormEquiv instructions -41.6%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances instructions -9.3%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -12.4%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -20.5%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -7.0%
+ ~Mathlib.Analysis.Seminorm instructions -15.4%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -9.1%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -20.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.4%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.9%
+ ~Mathlib.Data.Finset.Pointwise instructions -9.0%
+ ~Mathlib.Data.Matrix.Basic instructions -14.4%
+ ~Mathlib.Data.Num.Lemmas instructions -15.7%
+ ~Mathlib.Data.Set.Pointwise.Interval instructions -15.4%
+ ~Mathlib.FieldTheory.KummerExtension instructions -8.8%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -10.4%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -14.8%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -6.7%
+ ~Mathlib.GroupTheory.HNNExtension instructions -9.1%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -12.0%
+ ~Mathlib.GroupTheory.PushoutI instructions -18.4%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -16.1%
+ ~Mathlib.LinearAlgebra.Dual instructions -4.6%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -10.1%
+ ~Mathlib.LinearAlgebra.LinearPMap instructions -8.8%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -28.4%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -21.2%
+ ~Mathlib.LinearAlgebra.Multilinear.Basic instructions -6.8%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions -9.1%
+ ~Mathlib.LinearAlgebra.Ray instructions -17.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -8.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Graded.External instructions -3.5%
+ ~Mathlib.LinearAlgebra.TensorProduct.RightExactness instructions -7.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -20.4%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -10.2%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -8.7%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -12.5%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -18.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -9.3%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -9.4%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -7.9%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -17.9%
+ ~Mathlib.MeasureTheory.Measure.Haar.Unique instructions -16.3%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -16.7%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -10.0%
+ ~Mathlib.RepresentationTheory.GroupCohomology.LowDegree instructions -8.3%
+ ~Mathlib.RingTheory.Derivation.Basic instructions -15.4%
+ ~Mathlib.RingTheory.IntegralRestrict instructions -7.9%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -15.8%
+ ~Mathlib.RingTheory.Kaehler instructions -9.4%
+ ~Mathlib.RingTheory.Localization.Basic instructions -11.5%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -8.0%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -16.1%
+ ~Mathlib.Topology.Algebra.Group.Basic instructions -15.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -8.6%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -12.1%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -10.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -9.3%
+ ~Mathlib.Topology.Homotopy.Path instructions -17.2%
!bench
I added an isDefEq check that is technically necessary (but it not being there didn't cause any problems). Let's see how it affects speed.
Here are the benchmark results for commit 41e7240089c9732628e25ee65ca6ed906e74cbdf. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
========================================================================================================
+ build instructions -5.0%
+ build task-clock -5.1%
+ build typeclass inference -16.5%
+ build wall-clock -5.1%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -14.0%
+ ~Mathlib.Algebra.Algebra.Quasispectrum instructions -16.1%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -16.9%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -25.3%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -29.5%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -6.1%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -10.7%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -14.4%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -12.0%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -11.7%
+ ~Mathlib.Algebra.Order.Module.Defs instructions -16.9%
+ ~Mathlib.Algebra.Order.ToIntervalMod instructions -18.6%
+ ~Mathlib.Algebra.Polynomial.Module.Basic instructions -15.9%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -14.7%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -20.7%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -26.6%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions -7.5%
+ ~Mathlib.Analysis.Analytic.Basic instructions -9.9%
+ ~Mathlib.Analysis.Analytic.CPolynomial instructions -11.8%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -9.2%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -10.3%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds instructions -7.1%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -10.3%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -13.8%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -9.5%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions -10.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Measurable instructions -12.7%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -10.5%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -11.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -24.0%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -15.1%
+ ~Mathlib.Analysis.Calculus.LineDeriv.Basic instructions -16.0%
+ ~Mathlib.Analysis.Calculus.Rademacher instructions -16.5%
+ ~Mathlib.Analysis.Convex.Function instructions -31.6%
+ ~Mathlib.Analysis.Convex.Gauge instructions -15.3%
+ ~Mathlib.Analysis.Convex.Jensen instructions -19.6%
+ ~Mathlib.Analysis.Convex.Mul instructions -15.0%
+ ~Mathlib.Analysis.Convex.Segment instructions -19.8%
+ ~Mathlib.Analysis.Convolution instructions -10.5%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -7.9%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -9.8%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -8.3%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -21.4%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -9.8%
+ ~Mathlib.Analysis.NormedSpace.BallAction instructions -21.8%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -13.4%
+ ~Mathlib.Analysis.NormedSpace.MStructure instructions -30.0%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -13.2%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -12.3%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -17.8%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -18.0%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Prod instructions -14.3%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions -6.5%
+ ~Mathlib.Analysis.NormedSpace.SphereNormEquiv instructions -41.6%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances instructions -9.2%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -12.5%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -20.4%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -7.0%
+ ~Mathlib.Analysis.Seminorm instructions -15.3%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -8.7%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -19.9%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.4%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.9%
+ ~Mathlib.Data.Finset.Pointwise instructions -9.0%
+ ~Mathlib.Data.Matrix.Basic instructions -14.3%
+ ~Mathlib.Data.Num.Lemmas instructions -15.6%
+ ~Mathlib.Data.Set.Pointwise.Interval instructions -15.2%
+ ~Mathlib.FieldTheory.RatFunc.Basic instructions -5.0%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -10.3%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -14.2%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -6.2%
+ ~Mathlib.GroupTheory.HNNExtension instructions -9.1%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -11.9%
+ ~Mathlib.GroupTheory.PushoutI instructions -18.4%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -16.1%
+ ~Mathlib.LinearAlgebra.Dual instructions -4.4%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -10.0%
+ ~Mathlib.LinearAlgebra.LinearPMap instructions -8.8%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -28.4%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -21.1%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions -9.0%
+ ~Mathlib.LinearAlgebra.Ray instructions -16.9%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -8.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.RightExactness instructions -7.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -20.2%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -10.1%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -8.6%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -12.4%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -18.4%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -9.3%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -9.3%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -7.8%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -17.8%
+ ~Mathlib.MeasureTheory.Measure.Haar.Unique instructions -16.3%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -16.6%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -9.0%
+ ~Mathlib.RepresentationTheory.GroupCohomology.LowDegree instructions -8.2%
+ ~Mathlib.RingTheory.Derivation.Basic instructions -15.4%
+ ~Mathlib.RingTheory.IntegralRestrict instructions -7.8%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -15.7%
+ ~Mathlib.RingTheory.Kaehler instructions -8.9%
+ ~Mathlib.RingTheory.Localization.Basic instructions -11.4%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -8.2%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -16.1%
+ ~Mathlib.Topology.Algebra.Group.Basic instructions -15.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -8.6%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -11.9%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -10.1%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -8.7%
+ ~Mathlib.Topology.Homotopy.Path instructions -17.2%
!bench
I added a check so that the intermediate caching isn't used for outParam type classes. Hopefully that doesn't slow it down.
Here are the benchmark results for commit 4c58a5cf682bfac8bc496fec97eb2b4955acd594. There were significant changes against commit ce4bfeec5e50bb4cac5251e8cb6c5fb99c064e93:
Benchmark Metric Change
========================================================================================================
+ build task-clock -5.2%
+ build typeclass inference -15.2%
+ build wall-clock -5.5%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -12.6%
+ ~Mathlib.Algebra.Algebra.Quasispectrum instructions -14.9%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -16.6%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -23.9%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -28.3%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -5.9%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -12.0%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -12.9%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -11.4%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -10.6%
+ ~Mathlib.Algebra.Order.Module.Defs instructions -15.8%
+ ~Mathlib.Algebra.Order.ToIntervalMod instructions -17.7%
+ ~Mathlib.Algebra.Polynomial.Module.Basic instructions -15.2%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -12.7%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -19.1%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -25.8%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions -6.7%
+ ~Mathlib.Analysis.Analytic.Basic instructions -9.2%
+ ~Mathlib.Analysis.Analytic.CPolynomial instructions -11.0%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -8.9%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -9.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Bounds instructions -6.7%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -9.6%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -13.3%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -9.0%
+ ~Mathlib.Analysis.Calculus.FDeriv.Basic instructions -9.3%
+ ~Mathlib.Analysis.Calculus.FDeriv.Measurable instructions -12.2%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -10.1%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -10.3%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -23.9%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -14.1%
+ ~Mathlib.Analysis.Calculus.LineDeriv.Basic instructions -15.1%
+ ~Mathlib.Analysis.Calculus.Rademacher instructions -16.3%
+ ~Mathlib.Analysis.Convex.Function instructions -30.7%
+ ~Mathlib.Analysis.Convex.Jensen instructions -18.9%
+ ~Mathlib.Analysis.Convex.Mul instructions -14.5%
+ ~Mathlib.Analysis.Convex.Segment instructions -19.1%
+ ~Mathlib.Analysis.Convolution instructions -9.8%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -7.2%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -9.7%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -7.8%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -21.0%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -9.3%
+ ~Mathlib.Analysis.NormedSpace.BallAction instructions -21.2%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -14.4%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -12.9%
+ ~Mathlib.Analysis.NormedSpace.MStructure instructions -29.3%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -12.6%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -12.0%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -16.6%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -17.6%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Prod instructions -14.4%
+ ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions -3.4%
+ ~Mathlib.Analysis.NormedSpace.SphereNormEquiv instructions -41.3%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances instructions -9.0%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -11.4%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -19.0%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -6.4%
+ ~Mathlib.Analysis.Seminorm instructions -13.9%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -8.9%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -20.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.2%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.7%
+ ~Mathlib.Data.Finset.Pointwise instructions -8.5%
+ ~Mathlib.Data.Matrix.Basic instructions -13.2%
+ ~Mathlib.Data.Num.Lemmas instructions -15.3%
+ ~Mathlib.Data.Set.Pointwise.Interval instructions -14.8%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -9.4%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -14.5%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -6.4%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -11.1%
+ ~Mathlib.GroupTheory.PushoutI instructions -17.5%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -14.7%
+ ~Mathlib.LinearAlgebra.Dual instructions -4.1%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -25.8%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -20.4%
+ ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions -8.3%
+ ~Mathlib.LinearAlgebra.Ray instructions -15.9%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -6.9%
+ ~Mathlib.LinearAlgebra.TensorProduct.Graded.External instructions -3.8%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -19.1%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -9.7%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -8.1%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -11.9%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -16.9%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -8.4%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -8.7%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -7.2%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -17.6%
+ ~Mathlib.MeasureTheory.Measure.Haar.Unique instructions -15.7%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -16.0%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -9.9%
+ ~Mathlib.RingTheory.Derivation.Basic instructions -13.8%
+ ~Mathlib.RingTheory.IntegralRestrict instructions -7.1%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -14.7%
+ ~Mathlib.RingTheory.Kaehler instructions -9.1%
+ ~Mathlib.RingTheory.Localization.Basic instructions -10.8%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -7.6%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -15.1%
+ ~Mathlib.Topology.Algebra.Group.Basic instructions -14.9%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -7.3%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -11.3%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -9.0%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -9.2%
+ ~Mathlib.Topology.Homotopy.Path instructions -14.8%