mathlib4
mathlib4 copied to clipboard
leanprover-community
Lean pr testing 4206
The bug fix lean4#4206 causes some change in the behaviour of congr, convert and friends. So some proofs need to be fixed, usually by providing more arguments.
Here are the benchmark results for commit 4f3c460cc1668820c9af8418a87a23db44c7acab. There were significant changes against commit b3faac95adcd7958b82fc6d00cdc994362936fda:
Benchmark Metric Change
=====================================================================================================
+ build elaboration -9.6%
+ build linting -5.7%
+ build tactic execution -5.6%
+ open Mathlib task-clock -20.4% (-23.2 σ)
+ ~Batteries.Data.Array.Lemmas instructions -87.8%
+ ~Batteries.Data.List.Lemmas instructions -40.3%
- ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions 2.5%
+ ~Mathlib.Algebra.DirectLimit instructions -15.3%
+ ~Mathlib.Algebra.Lie.Quotient instructions -72.1%
- ~Mathlib.Algebra.Module.LinearMap.Polynomial instructions 11.7%
- ~Mathlib.Algebra.Module.PID instructions 42.5%
+ ~Mathlib.Algebra.Module.Submodule.Localization instructions -49.9%
+ ~Mathlib.AlgebraicGeometry.FunctionField instructions -27.7%
- ~Mathlib.Analysis.Calculus.ContDiff.Defs instructions 4.8%
- ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions 3.8%
+ ~Mathlib.Analysis.Convex.Strict instructions -33.9%
- ~Mathlib.Analysis.Convolution instructions 6.5%
+ ~Mathlib.Analysis.Normed.Group.Quotient instructions -74.9%
- ~Mathlib.Analysis.NormedSpace.Multilinear.Basic instructions 3.0%
- ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm instructions 5.6%
+ ~Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four instructions -15.7%
+ ~Mathlib.CategoryTheory.Generator instructions -42.0%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa instructions -68.5%
+ ~Mathlib.Computability.Halting instructions -62.6%
+ ~Mathlib.Computability.PartrecCode instructions -24.7%
+ ~Mathlib.FieldTheory.AbelRuffini instructions -34.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure instructions -43.5%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Affine instructions -20.9%
- ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace instructions 6.7%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits instructions -7.2%
+ ~Mathlib.GroupTheory.Coset instructions -78.7%
+ ~Mathlib.GroupTheory.GroupAction.Quotient instructions -76.4%
+ ~Mathlib.GroupTheory.QuotientGroup instructions -33.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading instructions -13.9%
+ ~Mathlib.LinearAlgebra.Isomorphisms instructions -57.1%
+ ~Mathlib.LinearAlgebra.Matrix.ToLinearEquiv instructions -49.4%
+ ~Mathlib.LinearAlgebra.Quotient instructions -27.8%
+ ~Mathlib.LinearAlgebra.QuotientPi instructions -67.4%
+ ~Mathlib.LinearAlgebra.SModEq instructions -89.4%
+ ~Mathlib.LinearAlgebra.StdBasis instructions -51.9%
- ~Mathlib.MeasureTheory.Integral.SetToL1 instructions 3.4%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient instructions -53.9%
+ ~Mathlib.NumberTheory.PythagoreanTriples instructions -46.3%
+ ~Mathlib.Probability.Martingale.Basic instructions -36.9%
+ ~Mathlib.RingTheory.Jacobson instructions -25.0%
- ~Mathlib.RingTheory.Kaehler instructions 2.1%
+ ~Mathlib.RingTheory.Smooth.Basic instructions -41.1%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain instructions -15.7%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring instructions -20.0%
+ ~Mathlib.SetTheory.Game.Short instructions -59.3%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module instructions -60.2%
+ ~Mathlib.Topology.Instances.AddCircle instructions -58.9%
