mathlib4
mathlib4 copied to clipboard
leanprover-community
Lean pr testing 4152
Here are the benchmark results for commit 8186e4674adb99a0cfba583406b9c80333b95e17. There were significant changes against commit b5b8fe5fa963f36940408c9ddeb042a2053015d1:
Benchmark Metric Change
===============================================================================================
+ build typeclass inference -8.3%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -7.4%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -18.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -19.0%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -6.4%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -9.6%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -8.8%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -8.5%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -10.4%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -20.4%
+ ~Mathlib.Analysis.Analytic.Basic instructions -5.1%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -6.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -5.7%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -8.1%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -5.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -18.4%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -11.3%
+ ~Mathlib.Analysis.Convex.Function instructions -25.5%
+ ~Mathlib.Analysis.Convolution instructions -3.2%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -5.3%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -6.2%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -17.7%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -6.3%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -10.6%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -8.5%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -8.3%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -11.2%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -13.4%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -8.0%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -13.4%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -4.2%
+ ~Mathlib.Analysis.Seminorm instructions -9.1%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -8.5%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -19.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.4%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.7%
+ ~Mathlib.Data.Num.Lemmas instructions -13.9%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -11.2%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -9.6%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -14.5%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -22.0%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -18.1%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -6.4%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -14.7%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -13.1%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -3.8%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -12.0%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -5.4%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -10.6%
+ ~Mathlib.RingTheory.Kaehler instructions -5.6%
+ ~Mathlib.RingTheory.Localization.Basic instructions -9.4%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -4.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -5.5%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -5.4%
!bench
I modified the code, expecting it so be a little bit slower (or fail).
Here are the benchmark results for commit 9cb4b9c11406621ebd51a04fa8ea4574df8fcc15. There were significant changes against commit b5b8fe5fa963f36940408c9ddeb042a2053015d1:
Benchmark Metric Change
===============================================================================================
+ build typeclass inference -9.1%
+ ~Mathlib.Algebra.Algebra.NonUnitalSubalgebra instructions -7.4%
+ ~Mathlib.Algebra.Algebra.Unitization instructions -18.4%
+ ~Mathlib.Algebra.BigOperators.Finsupp instructions -19.0%
+ ~Mathlib.Algebra.Lie.Weights.Killing instructions -6.4%
+ ~Mathlib.Algebra.Module.LinearMap.Basic instructions -9.6%
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -8.8%
+ ~Mathlib.Algebra.Ring.CentroidHom instructions -8.5%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -10.4%
+ ~Mathlib.Algebra.TrivSqZeroExt instructions -20.4%
+ ~Mathlib.Analysis.Analytic.Basic instructions -5.1%
+ ~Mathlib.Analysis.Calculus.ContDiff.Basic instructions -6.0%
+ ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions -5.7%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -8.1%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -5.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric instructions -18.4%
+ ~Mathlib.Analysis.Calculus.Implicit instructions -11.3%
+ ~Mathlib.Analysis.Convex.Function instructions -25.5%
+ ~Mathlib.Analysis.Convolution instructions -3.2%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv instructions -5.3%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -6.2%
+ ~Mathlib.Analysis.InnerProductSpace.OfNorm instructions -17.7%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -6.3%
+ ~Mathlib.Analysis.NormedSpace.Banach instructions -10.6%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions -8.5%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry instructions -8.3%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Basic instructions -11.2%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear instructions -13.4%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -8.0%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -13.4%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -4.2%
+ ~Mathlib.Analysis.Seminorm instructions -9.1%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -8.5%
+ ~Mathlib.CategoryTheory.Bicategory.Adjunction instructions -19.0%
+ ~Mathlib.CategoryTheory.Monoidal.Braided.Basic instructions -20.4%
+ ~Mathlib.CategoryTheory.Monoidal.Rigid.Basic instructions -10.7%
+ ~Mathlib.Data.Num.Lemmas instructions -14.0%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions -11.2%
+ ~Mathlib.GroupTheory.MonoidLocalization instructions -9.6%
+ ~Mathlib.LinearAlgebra.BilinearMap instructions -14.5%
+ ~Mathlib.LinearAlgebra.Matrix.SchurComplement instructions -22.0%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -18.1%
+ ~Mathlib.LinearAlgebra.TensorProduct.Basic instructions -6.4%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower instructions -14.7%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain instructions -13.1%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -3.8%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar instructions -12.0%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -5.4%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -10.6%
+ ~Mathlib.RingTheory.Kaehler instructions -5.6%
+ ~Mathlib.RingTheory.Localization.Basic instructions -9.2%
+ ~Mathlib.RingTheory.TensorProduct.Basic instructions -4.7%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -5.5%
+ ~Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus instructions -5.4%