Lean pr testing 4276

[JovanGerb]

trafficstars

---

[JovanGerb]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5dee5a9ca4d9591572a7429eb65bf8b550b379ba. There were significant changes against commit 8529a6466928bc66b13cb815424a8a7b9de9f39d:

  Benchmark                                                         Metric         Change
  =======================================================================================
+ ~Batteries.Data.Array.Lemmas                                      instructions   -87.8%
+ ~Batteries.Data.List.Lemmas                                       instructions   -40.2%
- ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                 instructions     3.3%
- ~Mathlib.Algebra.Lie.Basic                                        instructions    11.7%
- ~Mathlib.Algebra.Lie.Weights.Killing                              instructions     7.0%
- ~Mathlib.Algebra.Module.LinearMap.Polynomial                      instructions    11.9%
- ~Mathlib.Algebra.Module.PID                                       instructions    34.1%
- ~Mathlib.Algebra.Star.NonUnitalSubalgebra                         instructions     3.0%
- ~Mathlib.AlgebraicGeometry.Gluing                                 instructions    24.0%
- ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties            instructions    15.7%
- ~Mathlib.AlgebraicGeometry.Restrict                               instructions    13.2%
- ~Mathlib.Analysis.Calculus.ContDiff.Defs                          instructions     5.0%
- ~Mathlib.Analysis.Calculus.FDeriv.Mul                             instructions     3.7%
+ ~Mathlib.Analysis.Convex.Strict                                   instructions   -33.8%
- ~Mathlib.Analysis.Convolution                                     instructions     6.6%
- ~Mathlib.Analysis.NormedSpace.Multilinear.Basic                   instructions     4.3%
- ~Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm   instructions     9.1%
+ ~Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four                instructions   -15.4%
- ~Mathlib.CategoryTheory.DifferentialObject                        instructions    18.5%
- ~Mathlib.CategoryTheory.GradedObject.Trifunctor                   instructions     7.8%
- ~Mathlib.CategoryTheory.Idempotents.FunctorExtension              instructions     9.3%
- ~Mathlib.CategoryTheory.Limits.Constructions.Over.Products        instructions     8.0%
- ~Mathlib.CategoryTheory.Limits.Shapes.Diagonal                    instructions     8.1%
- ~Mathlib.CategoryTheory.Linear.FunctorCategory                    instructions    29.8%
- ~Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory         instructions    14.2%
- ~Mathlib.CategoryTheory.Monoidal.Mon_                             instructions     9.4%
- ~Mathlib.CategoryTheory.Preadditive.EilenbergMoore                instructions    24.4%
- ~Mathlib.CategoryTheory.Preadditive.EndoFunctor                   instructions    25.3%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa                   instructions   -68.4%
+ ~Mathlib.Computability.Halting                                    instructions   -62.4%
+ ~Mathlib.Computability.PartrecCode                                instructions   -24.7%
+ ~Mathlib.FieldTheory.AbelRuffini                                  instructions   -33.7%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Affine                 instructions   -20.8%
- ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace                  instructions     6.7%
- ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing              instructions     6.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                    instructions   -13.3%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace                         instructions    31.6%
- ~Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup                  instructions    17.6%
+ ~Mathlib.LinearAlgebra.Matrix.ToLinearEquiv                       instructions   -50.0%
- ~Mathlib.LinearAlgebra.TensorProduct.Graded.External              instructions    12.5%
- ~Mathlib.MeasureTheory.Integral.SetToL1                           instructions     5.6%
+ ~Mathlib.NumberTheory.PythagoreanTriples                          instructions   -46.2%
- ~Mathlib.NumberTheory.RamificationInertia                         instructions    11.5%
+ ~Mathlib.Probability.Martingale.Basic                             instructions   -36.8%
- ~Mathlib.RepresentationTheory.Action.Basic                        instructions    21.1%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution          instructions    10.7%
- ~Mathlib.RingTheory.Kaehler                                       instructions     3.2%
- ~Mathlib.RingTheory.TensorProduct.Basic                           instructions     4.1%
+ ~Mathlib.RingTheory.UniqueFactorizationDomain                     instructions   -15.6%
+ ~Mathlib.SetTheory.Game.Short                                     instructions   -58.9%

[grunweg]

Coming here for triaging old PRs: is this one still relevant? The relevant Lean PR looks like it has been stale for more than ten months. @JovanGerb Can you clarify the status, please? Thanks!