Aesop forward benchmark: forward no-precomp rpinf pr-release by JLimperg · Pull Request #21608 · leanprover-community/mathlib4

JLimperg · 2025-02-09T16:52:48Z

Not a real PR, just for benchmarking.

…htly-2025-01-24

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kim Morrison <kim@tqft.net>

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Johan Commelin <johan@commelin.net>

JLimperg · 2025-02-09T16:53:10Z

!bench

github-actions · 2025-02-09T16:53:46Z

PR summary cbce97806d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ instance (n : ℕ) : TopologicalSpace (Vector α n) := by unfold Vector; infer_instance
- instance (n : ℕ) : TopologicalSpace (List.Vector α n) := by unfold List.Vector; infer_instance

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

leanprover-bot · 2025-02-09T17:23:37Z

Here are the benchmark results for commit cbce978.
There were significant changes against commit 50c9a9b:

  Benchmark                                                           Metric         Change
  =========================================================================================
- build                                                               aesop           33.4%
- ~Aesop.RuleSet                                                      instructions    88.0%
- ~Aesop.Search.Main                                                  instructions   151.3%
+ ~Batteries.Data.Array.Lemmas                                        instructions   -91.9%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order   instructions    13.5%
- ~Mathlib.Analysis.Convex.Visible                                    instructions    34.0%
- ~Mathlib.CategoryTheory.Triangulated.Functor                        instructions     7.6%
- ~Mathlib.CategoryTheory.Triangulated.TriangleShift                  instructions     9.7%
- ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct                  instructions    10.6%
- ~Mathlib.Probability.Kernel.Proper                                  instructions   113.2%
- ~Mathlib.Tactic.Module                                              instructions     9.1%

github-actions · 2025-02-09T17:24:00Z

File	Instructions	%
`build`	+1457.509⬝10⁹	(+0.96%)
`lint`	-12.749⬝10⁹	(-0.16%)
`Mathlib.Probability.Kernel.Proper`	+67.218⬝10⁹	(+113.17%)
`Aesop.Search.Main`	+63.348⬝10⁹	(+151.31%)
`Mathlib.Analysis.Convex.Visible`	+33.92⬝10⁹	(+33.98%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	+25.520⬝10⁹	(+13.50%)
`Mathlib.CategoryTheory.Triangulated.Functor`	+23.271⬝10⁹	(+7.58%)
`Mathlib.LinearAlgebra.QuadraticForm.TensorProduct`	+16.49⬝10⁹	(+10.62%)
`Mathlib.Tactic.Module`	+14.22⬝10⁹	(+9.06%)
`Mathlib.CategoryTheory.Triangulated.TriangleShift`	+13.553⬝10⁹	(+9.65%)
`Aesop.RuleSet`	+11.757⬝10⁹	(+88.04%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital`	+9.739⬝10⁹	(+4.15%)
`Mathlib.LinearAlgebra.BilinearForm.TensorProduct`	+8.128⬝10⁹	(+12.51%)

4 files, Instructions +7.0⬝10⁹

File	Instructions	%
`Mathlib.Lean.Meta.RefinedDiscrTree.Encode`	+7.809⬝10⁹	(+20.79%)
`Mathlib.Algebra.Homology.HomotopyCategory.HomComplex`	+7.599⬝10⁹	(+9.00%)
`Mathlib.Algebra.Homology.Bifunctor`	+7.146⬝10⁹	(+6.40%)
`Mathlib.CategoryTheory.Dialectica.Basic`	+7.17⬝10⁹	(+36.79%)

2 files, Instructions +6.0⬝10⁹

File	Instructions	%
`Aesop.Saturate`	+6.556⬝10⁹	(+71.90%)
`Mathlib.Combinatorics.SimpleGraph.Matching`	+6.388⬝10⁹	(+13.94%)

6 files, Instructions +5.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Limits.Cones`	+5.918⬝10⁹	(+1.90%)
`Mathlib.AlgebraicGeometry.Morphisms.AffineAnd`	+5.639⬝10⁹	(+17.57%)
`Mathlib.CategoryTheory.ComposableArrows`	+5.466⬝10⁹	(+1.80%)
`Mathlib.MeasureTheory.Measure.Haar.OfBasis`	+5.425⬝10⁹	(+10.96%)
`Mathlib.CategoryTheory.Comma.StructuredArrow.Basic`	+5.266⬝10⁹	(+1.67%)
`Mathlib.Probability.StrongLaw`	+5.127⬝10⁹	(+6.80%)

13 files, Instructions +4.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Comma.Basic`	+4.975⬝10⁹	(+2.58%)
`Mathlib.CategoryTheory.Comma.Over`	+4.910⬝10⁹	(+1.62%)
`Aesop.Search.Expansion.Norm`	+4.867⬝10⁹	(+39.30%)
`Mathlib.Algebra.Homology.HomotopyCategory.Shift`	+4.832⬝10⁹	(+9.67%)
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic`	+4.747⬝10⁹	(+3.37%)
`Mathlib.Analysis.CStarAlgebra.ApproximateUnit`	+4.571⬝10⁹	(+3.13%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances`	+4.549⬝10⁹	(+2.37%)
`Mathlib.SetTheory.Game.PGame`	+4.508⬝10⁹	(+6.77%)
`Mathlib.CategoryTheory.Limits.Shapes.Biproducts`	+4.457⬝10⁹	(+1.72%)
`Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion`	+4.327⬝10⁹	(+32.36%)
`Mathlib.Analysis.Analytic.Inverse`	+4.195⬝10⁹	(+3.23%)
`Mathlib.LinearAlgebra.ExteriorPower.Basic`	+4.58⬝10⁹	(+6.28%)
`Mathlib.LinearAlgebra.Matrix.FixedDetMatrices`	+4.12⬝10⁹	(+13.38%)

8 files, Instructions +3.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.WithTerminal`	+3.796⬝10⁹	(+3.05%)
`Mathlib.CategoryTheory.Whiskering`	+3.702⬝10⁹	(+1.43%)
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart`	+3.610⬝10⁹	(+2.88%)
`Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence`	+3.584⬝10⁹	(+3.56%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`	+3.510⬝10⁹	(+2.13%)
`Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory`	+3.459⬝10⁹	(+2.33%)
`Mathlib.Combinatorics.Additive.FreimanHom`	+3.421⬝10⁹	(+6.59%)
`Aesop.Search.Expansion`	+3.377⬝10⁹	(+15.18%)

33 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Aesop.RuleTac.Forward`	+2.993⬝10⁹	(+43.97%)
`Mathlib.Algebra.BigOperators.Finprod`	+2.920⬝10⁹	(+5.72%)
`Mathlib.SetTheory.Game.Basic`	+2.909⬝10⁹	(+3.49%)
`Mathlib.Analysis.RCLike.Basic`	+2.831⬝10⁹	(+2.48%)
`Mathlib.AlgebraicTopology.SimplicialNerve`	+2.756⬝10⁹	(+2.08%)
`Mathlib.CategoryTheory.Products.Basic`	+2.710⬝10⁹	(+3.13%)
`Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic`	+2.656⬝10⁹	(+3.05%)
`Mathlib.Computability.AkraBazzi.AkraBazzi`	+2.547⬝10⁹	(+1.56%)
`Mathlib.CategoryTheory.Triangulated.Opposite.Triangle`	+2.506⬝10⁹	(+1.88%)
`Mathlib.NumberTheory.ArithmeticFunction`	+2.471⬝10⁹	(+3.29%)
`Batteries.Data.Array.Match`	+2.468⬝10⁹	(+169.68%)
`Mathlib.CategoryTheory.Skeletal`	+2.466⬝10⁹	(+6.33%)
`Batteries.Data.LazyList`	+2.430⬝10⁹	(+35.28%)
`Mathlib.CategoryTheory.Functor.Trifunctor`	+2.327⬝10⁹	(+1.38%)
`Mathlib.LinearAlgebra.LinearIndependent`	+2.290⬝10⁹	(+1.60%)
`Aesop.Builder.Forward`	+2.259⬝10⁹	(+41.86%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic`	+2.257⬝10⁹	(+1.16%)
`Mathlib.CategoryTheory.MorphismProperty.OverAdjunction`	+2.250⬝10⁹	(+2.32%)
`Mathlib.CategoryTheory.Square`	+2.197⬝10⁹	(+3.08%)
`Mathlib.Combinatorics.SimpleGraph.Path`	+2.161⬝10⁹	(+5.32%)
`Mathlib.CategoryTheory.Comma.Presheaf.Basic`	+2.148⬝10⁹	(+1.46%)
`Mathlib.Data.Nat.Factors`	+2.127⬝10⁹	(+23.47%)
`Mathlib.RingTheory.IntegralClosure.IntegrallyClosed`	+2.124⬝10⁹	(+7.79%)
`Mathlib.CategoryTheory.Functor.CurryingThree`	+2.95⬝10⁹	(+1.23%)
`Aesop.Tree.AddRapp`	+2.93⬝10⁹	(+18.93%)
`Mathlib.Combinatorics.Enumerative.IncidenceAlgebra`	+2.87⬝10⁹	(+3.36%)
`Mathlib.CategoryTheory.Pi.Basic`	+2.75⬝10⁹	(+2.23%)
`Mathlib.RingTheory.Regular.RegularSequence`	+2.65⬝10⁹	(+2.29%)
`Mathlib.CategoryTheory.Bicategory.Free`	+2.62⬝10⁹	(+1.86%)
`Mathlib.RingTheory.HahnSeries.Multiplication`	+2.29⬝10⁹	(+2.51%)
`Mathlib.CategoryTheory.Monoidal.Functor`	+2.26⬝10⁹	(+1.41%)
`Mathlib.CategoryTheory.Monoidal.Mon_`	+2.12⬝10⁹	(+1.40%)
`Mathlib.Algebra.Homology.ShortComplex.Preadditive`	+2.3⬝10⁹	(+2.05%)

110 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Category.Ring.Basic`	+1.984⬝10⁹	(+4.15%)
`Aesop.RuleTac.GoalDiff`	+1.933⬝10⁹	(+28.86%)
`Mathlib.CategoryTheory.GradedObject.Trifunctor`	+1.894⬝10⁹	(+0.75%)
`Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete`	+1.869⬝10⁹	(+2.06%)
`Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone`	+1.863⬝10⁹	(+1.83%)
`Mathlib.Algebra.Order.BigOperators.Ring.Finset`	+1.841⬝10⁹	(+4.51%)
`Mathlib.CategoryTheory.Limits.ConeCategory`	+1.813⬝10⁹	(+2.12%)
`Aesop.Tree.Tracing`	+1.796⬝10⁹	(+32.35%)
`Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks`	+1.782⬝10⁹	(+1.45%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital`	+1.777⬝10⁹	(+1.21%)
`Mathlib.SetTheory.Lists`	+1.763⬝10⁹	(+10.49%)
`Mathlib.Topology.Category.TopCat.Opens`	+1.733⬝10⁹	(+3.28%)
`Mathlib.Algebra.Module.CharacterModule`	+1.733⬝10⁹	(+2.85%)
`Mathlib.CategoryTheory.Monoidal.Category`	+1.729⬝10⁹	(+1.57%)
`Mathlib.Analysis.InnerProductSpace.Positive`	+1.700⬝10⁹	(+4.55%)
`Mathlib.Tactic.FailIfNoProgress`	+1.697⬝10⁹	(+44.10%)
`Aesop.Util.Basic`	+1.675⬝10⁹	(+15.80%)
`Mathlib.CategoryTheory.Limits.Constructions.Over.Products`	+1.670⬝10⁹	(+2.05%)
`Mathlib.Analysis.Convex.Birkhoff`	+1.630⬝10⁹	(+4.85%)
`Mathlib.AlgebraicTopology.SimplicialObject.Basic`	+1.628⬝10⁹	(+0.78%)
`Mathlib.Algebra.Algebra.Subalgebra.Centralizer`	+1.627⬝10⁹	(+4.83%)
`Mathlib.AlgebraicTopology.CechNerve`	+1.620⬝10⁹	(+0.89%)
`Mathlib.Analysis.Normed.Group.SemiNormedGrp`	+1.618⬝10⁹	(+7.28%)
`Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex`	+1.593⬝10⁹	(+2.88%)
`Mathlib.LinearAlgebra.PerfectPairing.Restrict`	+1.577⬝10⁹	(+2.36%)
`Mathlib.CategoryTheory.Endofunctor.Algebra`	+1.570⬝10⁹	(+2.46%)
`Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear`	+1.545⬝10⁹	(+2.24%)
`Mathlib.CategoryTheory.Elements`	+1.535⬝10⁹	(+2.21%)
`Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves`	+1.530⬝10⁹	(+2.59%)
`Mathlib.Combinatorics.SimpleGraph.Operations`	+1.515⬝10⁹	(+7.95%)
`Mathlib.CategoryTheory.Yoneda`	+1.509⬝10⁹	(+1.34%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf`	+1.508⬝10⁹	(+0.58%)
`Mathlib.Algebra.Homology.ShortComplex.LeftHomology`	+1.498⬝10⁹	(+2.83%)
`Mathlib.CategoryTheory.Opposites`	+1.488⬝10⁹	(+3.32%)
`Mathlib.CategoryTheory.Limits.HasLimits`	+1.471⬝10⁹	(+1.85%)
`Mathlib.CategoryTheory.Adjunction.Over`	+1.456⬝10⁹	(+1.56%)
`Mathlib.GroupTheory.Coxeter.Matrix`	+1.447⬝10⁹	(+1.73%)
`Mathlib.Algebra.Homology.ShortComplex.Basic`	+1.441⬝10⁹	(+4.72%)
`Mathlib.CategoryTheory.Monoidal.CommMon_`	+1.408⬝10⁹	(+1.35%)
`Mathlib.CategoryTheory.Monoidal.Center`	+1.406⬝10⁹	(+2.15%)
`Mathlib.Algebra.Category.MonCat.Basic`	+1.392⬝10⁹	(+2.31%)
`Mathlib.CategoryTheory.Monoidal.Internal.Types`	+1.391⬝10⁹	(+2.65%)
`Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts`	+1.389⬝10⁹	(+1.41%)
`Mathlib.Analysis.Calculus.ContDiff.Basic`	+1.382⬝10⁹	(+0.31%)
`Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers`	+1.382⬝10⁹	(+3.56%)
`Mathlib.CategoryTheory.Limits.Shapes.IsTerminal`	+1.381⬝10⁹	(+3.90%)
`Mathlib.CategoryTheory.Subobject.MonoOver`	+1.379⬝10⁹	(+1.25%)
`Mathlib.CategoryTheory.FiberedCategory.BasedCategory`	+1.374⬝10⁹	(+3.76%)
`Mathlib.MeasureTheory.Group.GeometryOfNumbers`	+1.366⬝10⁹	(+3.94%)
`Mathlib.Algebra.Homology.TotalComplex`	+1.340⬝10⁹	(+3.59%)
`Mathlib.CategoryTheory.GradedObject`	+1.336⬝10⁹	(+2.21%)
`Mathlib.Algebra.Homology.HomologySequence`	+1.318⬝10⁹	(+1.87%)
`Mathlib.CategoryTheory.Bicategory.Coherence`	+1.317⬝10⁹	(+1.09%)
`Mathlib.CategoryTheory.Limits.Shapes.Diagonal`	+1.305⬝10⁹	(+0.83%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique`	+1.297⬝10⁹	(+0.85%)
`Mathlib.Algebra.Homology.ShortComplex.RightHomology`	+1.292⬝10⁹	(+1.95%)
`Aesop.Search.RuleSelection`	+1.292⬝10⁹	(+56.78%)
`Mathlib.Data.Matroid.Closure`	+1.286⬝10⁹	(+2.21%)
`Mathlib.Condensed.Discrete.Module`	+1.273⬝10⁹	(+1.11%)
`Mathlib.Probability.Kernel.Disintegration.Density`	+1.272⬝10⁹	(+2.93%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral`	+1.260⬝10⁹	(+3.30%)
`Mathlib.Topology.Homotopy.HomotopyGroup`	+1.235⬝10⁹	(+1.47%)
`Mathlib.Algebra.Homology.ShortComplex.Linear`	+1.231⬝10⁹	(+2.28%)
`Mathlib.LinearAlgebra.Matrix.SesquilinearForm`	+1.228⬝10⁹	(+0.96%)
`Mathlib.GroupTheory.Coset.Card`	+1.218⬝10⁹	(+9.35%)
`Mathlib.RingTheory.Flat.FaithfullyFlat.Basic`	+1.215⬝10⁹	(+1.73%)
`Mathlib.Analysis.Normed.Group.ZeroAtInfty`	+1.204⬝10⁹	(+14.58%)
`Mathlib.Algebra.Lie.LieTheorem`	+1.197⬝10⁹	(+1.68%)
`Mathlib.CategoryTheory.Monoidal.Bimon_`	+1.194⬝10⁹	(+1.40%)
`Mathlib.Analysis.Complex.Tietze`	+1.183⬝10⁹	(+6.09%)
`Mathlib.CategoryTheory.Monad.Algebra`	+1.181⬝10⁹	(+2.17%)
`Mathlib.CategoryTheory.Limits.IsLimit`	+1.181⬝10⁹	(+1.28%)
`Aesop.Util.UnionFind`	+1.176⬝10⁹	(+38.40%)
`Mathlib.CategoryTheory.Action.Basic`	+1.170⬝10⁹	(+1.99%)
`Mathlib.Analysis.Analytic.OfScalars`	+1.169⬝10⁹	(+2.36%)
`Mathlib.CategoryTheory.Adjunction.Basic`	+1.160⬝10⁹	(+1.97%)
`Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections`	+1.160⬝10⁹	(+1.33%)
`Mathlib.CategoryTheory.Monad.Products`	+1.154⬝10⁹	(+1.94%)
`Mathlib.CategoryTheory.Limits.Final`	+1.147⬝10⁹	(+0.63%)
`Mathlib.Analysis.CStarAlgebra.Module.Constructions`	+1.146⬝10⁹	(+1.51%)
`Mathlib.Data.Sym.Sym2`	+1.141⬝10⁹	(+4.55%)
`Mathlib.CategoryTheory.Triangulated.Rotate`	+1.135⬝10⁹	(+2.95%)
`Mathlib.Analysis.Convolution`	+1.126⬝10⁹	(+0.29%)
`Mathlib.Algebra.Homology.Additive`	+1.116⬝10⁹	(+1.51%)
`Mathlib.CategoryTheory.Monoidal.Braided.Basic`	+1.112⬝10⁹	(+1.29%)
`Mathlib.Analysis.Distribution.SchwartzSpace`	+1.109⬝10⁹	(+0.48%)
`Mathlib.Algebra.Category.Grp.Basic`	+1.104⬝10⁹	(+2.60%)
`Mathlib.Algebra.Homology.ShortComplex.SnakeLemma`	+1.104⬝10⁹	(+1.12%)
`Mathlib.CategoryTheory.Functor.FunctorHom`	+1.101⬝10⁹	(+2.77%)
`Mathlib.CategoryTheory.Abelian.Images`	+1.94⬝10⁹	(+3.29%)
`Mathlib.Analysis.Convex.Jensen`	+1.90⬝10⁹	(+2.39%)
`Aesop.Tree.ExtractScript`	+1.85⬝10⁹	(+12.55%)
`Mathlib.CategoryTheory.Adjunction.Limits`	+1.79⬝10⁹	(+1.89%)
`Mathlib.Condensed.Discrete.LocallyConstant`	+1.76⬝10⁹	(+1.29%)
`Mathlib.CategoryTheory.Triangulated.Basic`	+1.69⬝10⁹	(+3.43%)
`Mathlib.RingTheory.TensorProduct.Basic`	+1.62⬝10⁹	(+0.32%)
`Mathlib.LinearAlgebra.PiTensorProduct`	+1.54⬝10⁹	(+0.71%)
`Mathlib.Algebra.Lie.Weights.Basic`	+1.54⬝10⁹	(+0.93%)
`Mathlib.CategoryTheory.Linear.Yoneda`	+1.49⬝10⁹	(+1.57%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+1.45⬝10⁹	(+0.25%)
`Mathlib.Analysis.Convex.Combination`	+1.41⬝10⁹	(+0.88%)
`Mathlib.CategoryTheory.Triangulated.Pretriangulated`	+1.40⬝10⁹	(+2.31%)
`Mathlib.CategoryTheory.Monoidal.Internal.Module`	+1.39⬝10⁹	(+0.73%)
`Mathlib.CategoryTheory.Bicategory.SingleObj`	+1.35⬝10⁹	(+5.67%)
`Mathlib.Algebra.Category.ModuleCat.Basic`	+1.30⬝10⁹	(+1.17%)
`Mathlib.Algebra.Homology.HomologicalBicomplex`	+1.29⬝10⁹	(+2.40%)
`Mathlib.Algebra.Module.Presentation.Differentials`	+1.21⬝10⁹	(+1.58%)
`Mathlib.CategoryTheory.MorphismProperty.Comma`	+1.15⬝10⁹	(+2.82%)
`Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer`	+1.10⬝10⁹	(+1.11%)
`Aesop.Main`	+1.7⬝10⁹	(+16.33%)

3 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.AlgebraicGeometry.AffineSpace`	-1.0⬝10⁹	(-0.40%)
`Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing`	-1.85⬝10⁹	(-0.38%)
`Mathlib.Tactic.CC.Addition`	-1.239⬝10⁹	(-1.27%)

File	Instructions	%
`Batteries.Data.Array.Monadic`	-2.611⬝10⁹	(-24.61%)
`Mathlib.Topology.Sheaves.Presheaf`	-4.108⬝10⁹	(-5.58%)
`Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated`	-5.239⬝10⁹	(-4.20%)
`Batteries.Data.Array.Lemmas`	-19.282⬝10⁹	(-91.90%)
CI run

JLimperg · 2025-02-19T23:32:50Z

!bench

leanprover-bot · 2025-02-20T00:54:37Z

Here are the benchmark results for commit 43858d3.
There were significant changes against commit 50c9a9b:

  Benchmark                                                           Metric         Change
  =========================================================================================
- build                                                               aesop           33.1%
- ~Aesop.RuleSet                                                      instructions    88.0%
- ~Aesop.Search.Main                                                  instructions   151.3%
+ ~Batteries.Data.Array.Lemmas                                        instructions   -91.9%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order   instructions    13.5%
- ~Mathlib.Analysis.Convex.Visible                                    instructions    34.0%
- ~Mathlib.CategoryTheory.Triangulated.Functor                        instructions     7.6%
- ~Mathlib.CategoryTheory.Triangulated.TriangleShift                  instructions     9.7%
- ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct                  instructions    10.6%
- ~Mathlib.Probability.Kernel.Proper                                  instructions   113.2%
- ~Mathlib.Tactic.Module                                              instructions     9.1%

github-actions · 2025-02-20T00:55:03Z

File	Instructions	%
`build`	+1463.852⬝10⁹	(+0.97%)
`lint`	-13.39⬝10⁹	(-0.16%)
`Mathlib.Probability.Kernel.Proper`	+67.236⬝10⁹	(+113.20%)
`Aesop.Search.Main`	+63.354⬝10⁹	(+151.33%)
`Mathlib.Analysis.Convex.Visible`	+33.90⬝10⁹	(+33.98%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	+25.524⬝10⁹	(+13.51%)
`Mathlib.CategoryTheory.Triangulated.Functor`	+23.255⬝10⁹	(+7.58%)
`Mathlib.LinearAlgebra.QuadraticForm.TensorProduct`	+16.66⬝10⁹	(+10.64%)
`Mathlib.Tactic.Module`	+14.12⬝10⁹	(+9.05%)
`Mathlib.CategoryTheory.Triangulated.TriangleShift`	+13.553⬝10⁹	(+9.65%)
`Aesop.RuleSet`	+11.756⬝10⁹	(+88.03%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital`	+9.737⬝10⁹	(+4.15%)
`Mathlib.LinearAlgebra.BilinearForm.TensorProduct`	+8.140⬝10⁹	(+12.52%)

4 files, Instructions +7.0⬝10⁹

File	Instructions	%
`Mathlib.Lean.Meta.RefinedDiscrTree.Encode`	+7.809⬝10⁹	(+20.79%)
`Mathlib.Algebra.Homology.HomotopyCategory.HomComplex`	+7.603⬝10⁹	(+9.00%)
`Mathlib.Algebra.Homology.Bifunctor`	+7.157⬝10⁹	(+6.41%)
`Mathlib.CategoryTheory.Dialectica.Basic`	+7.19⬝10⁹	(+36.81%)

2 files, Instructions +6.0⬝10⁹

File	Instructions	%
`Aesop.Saturate`	+6.553⬝10⁹	(+71.87%)
`Mathlib.Combinatorics.SimpleGraph.Matching`	+6.390⬝10⁹	(+13.94%)

6 files, Instructions +5.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Limits.Cones`	+5.926⬝10⁹	(+1.91%)
`Mathlib.AlgebraicGeometry.Morphisms.AffineAnd`	+5.637⬝10⁹	(+17.57%)
`Mathlib.CategoryTheory.ComposableArrows`	+5.503⬝10⁹	(+1.81%)
`Mathlib.MeasureTheory.Measure.Haar.OfBasis`	+5.428⬝10⁹	(+10.97%)
`Mathlib.CategoryTheory.Comma.StructuredArrow.Basic`	+5.260⬝10⁹	(+1.67%)
`Mathlib.Probability.StrongLaw`	+5.129⬝10⁹	(+6.81%)

13 files, Instructions +4.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Comma.Basic`	+4.975⬝10⁹	(+2.58%)
`Mathlib.CategoryTheory.Comma.Over`	+4.937⬝10⁹	(+1.63%)
`Aesop.Search.Expansion.Norm`	+4.869⬝10⁹	(+39.31%)
`Mathlib.Algebra.Homology.HomotopyCategory.Shift`	+4.832⬝10⁹	(+9.67%)
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic`	+4.748⬝10⁹	(+3.37%)
`Mathlib.Analysis.CStarAlgebra.ApproximateUnit`	+4.576⬝10⁹	(+3.14%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances`	+4.540⬝10⁹	(+2.37%)
`Mathlib.SetTheory.Game.PGame`	+4.514⬝10⁹	(+6.78%)
`Mathlib.CategoryTheory.Limits.Shapes.Biproducts`	+4.451⬝10⁹	(+1.72%)
`Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion`	+4.328⬝10⁹	(+32.36%)
`Mathlib.Analysis.Analytic.Inverse`	+4.189⬝10⁹	(+3.22%)
`Mathlib.LinearAlgebra.ExteriorPower.Basic`	+4.58⬝10⁹	(+6.29%)
`Mathlib.LinearAlgebra.Matrix.FixedDetMatrices`	+4.11⬝10⁹	(+13.38%)

8 files, Instructions +3.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.WithTerminal`	+3.807⬝10⁹	(+3.06%)
`Mathlib.CategoryTheory.Whiskering`	+3.696⬝10⁹	(+1.42%)
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart`	+3.613⬝10⁹	(+2.89%)
`Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence`	+3.603⬝10⁹	(+3.58%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`	+3.509⬝10⁹	(+2.13%)
`Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory`	+3.467⬝10⁹	(+2.33%)
`Mathlib.Combinatorics.Additive.FreimanHom`	+3.425⬝10⁹	(+6.60%)
`Aesop.Search.Expansion`	+3.376⬝10⁹	(+15.17%)

33 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Aesop.RuleTac.Forward`	+2.993⬝10⁹	(+43.97%)
`Mathlib.Algebra.BigOperators.Finprod`	+2.921⬝10⁹	(+5.72%)
`Mathlib.SetTheory.Game.Basic`	+2.908⬝10⁹	(+3.49%)
`Mathlib.Analysis.RCLike.Basic`	+2.831⬝10⁹	(+2.48%)
`Mathlib.AlgebraicTopology.SimplicialNerve`	+2.756⬝10⁹	(+2.08%)
`Mathlib.CategoryTheory.Products.Basic`	+2.717⬝10⁹	(+3.14%)
`Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic`	+2.664⬝10⁹	(+3.06%)
`Mathlib.Computability.AkraBazzi.AkraBazzi`	+2.546⬝10⁹	(+1.56%)
`Mathlib.CategoryTheory.Triangulated.Opposite.Triangle`	+2.499⬝10⁹	(+1.87%)
`Mathlib.CategoryTheory.Skeletal`	+2.471⬝10⁹	(+6.34%)
`Mathlib.NumberTheory.ArithmeticFunction`	+2.470⬝10⁹	(+3.29%)
`Batteries.Data.Array.Match`	+2.468⬝10⁹	(+169.68%)
`Batteries.Data.LazyList`	+2.430⬝10⁹	(+35.27%)
`Mathlib.CategoryTheory.Functor.Trifunctor`	+2.348⬝10⁹	(+1.39%)
`Mathlib.LinearAlgebra.LinearIndependent`	+2.284⬝10⁹	(+1.59%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic`	+2.261⬝10⁹	(+1.17%)
`Aesop.Builder.Forward`	+2.259⬝10⁹	(+41.86%)
`Mathlib.CategoryTheory.MorphismProperty.OverAdjunction`	+2.244⬝10⁹	(+2.32%)
`Mathlib.CategoryTheory.Square`	+2.207⬝10⁹	(+3.09%)
`Mathlib.Combinatorics.SimpleGraph.Path`	+2.165⬝10⁹	(+5.33%)
`Mathlib.CategoryTheory.Comma.Presheaf.Basic`	+2.155⬝10⁹	(+1.47%)
`Mathlib.Data.Nat.Factors`	+2.129⬝10⁹	(+23.49%)
`Mathlib.RingTheory.IntegralClosure.IntegrallyClosed`	+2.124⬝10⁹	(+7.79%)
`Mathlib.CategoryTheory.Functor.CurryingThree`	+2.121⬝10⁹	(+1.25%)
`Aesop.Tree.AddRapp`	+2.93⬝10⁹	(+18.92%)
`Mathlib.Combinatorics.Enumerative.IncidenceAlgebra`	+2.84⬝10⁹	(+3.35%)
`Mathlib.CategoryTheory.Pi.Basic`	+2.74⬝10⁹	(+2.23%)
`Mathlib.CategoryTheory.Bicategory.Free`	+2.74⬝10⁹	(+1.87%)
`Mathlib.RingTheory.Regular.RegularSequence`	+2.68⬝10⁹	(+2.29%)
`Mathlib.RingTheory.HahnSeries.Multiplication`	+2.29⬝10⁹	(+2.52%)
`Mathlib.CategoryTheory.Monoidal.Functor`	+2.27⬝10⁹	(+1.41%)
`Mathlib.CategoryTheory.Monoidal.Mon_`	+2.12⬝10⁹	(+1.40%)
`Mathlib.Algebra.Homology.ShortComplex.Preadditive`	+2.3⬝10⁹	(+2.05%)

111 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Category.Ring.Basic`	+1.986⬝10⁹	(+4.16%)
`Aesop.RuleTac.GoalDiff`	+1.933⬝10⁹	(+28.86%)
`Mathlib.CategoryTheory.GradedObject.Trifunctor`	+1.904⬝10⁹	(+0.76%)
`Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete`	+1.869⬝10⁹	(+2.06%)
`Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone`	+1.864⬝10⁹	(+1.84%)
`Mathlib.Algebra.Order.BigOperators.Ring.Finset`	+1.844⬝10⁹	(+4.52%)
`Mathlib.CategoryTheory.Limits.ConeCategory`	+1.816⬝10⁹	(+2.12%)
`Aesop.Tree.Tracing`	+1.800⬝10⁹	(+32.42%)
`Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks`	+1.783⬝10⁹	(+1.45%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital`	+1.782⬝10⁹	(+1.21%)
`Mathlib.SetTheory.Lists`	+1.765⬝10⁹	(+10.50%)
`Mathlib.Algebra.Module.CharacterModule`	+1.735⬝10⁹	(+2.85%)
`Mathlib.Topology.Category.TopCat.Opens`	+1.735⬝10⁹	(+3.28%)
`Mathlib.CategoryTheory.Monoidal.Category`	+1.731⬝10⁹	(+1.57%)
`Mathlib.Analysis.InnerProductSpace.Positive`	+1.701⬝10⁹	(+4.55%)
`Mathlib.Tactic.FailIfNoProgress`	+1.697⬝10⁹	(+44.10%)
`Aesop.Util.Basic`	+1.675⬝10⁹	(+15.80%)
`Mathlib.CategoryTheory.Limits.Constructions.Over.Products`	+1.659⬝10⁹	(+2.04%)
`Mathlib.AlgebraicTopology.SimplicialObject.Basic`	+1.631⬝10⁹	(+0.78%)
`Mathlib.Analysis.Convex.Birkhoff`	+1.630⬝10⁹	(+4.84%)
`Mathlib.AlgebraicTopology.CechNerve`	+1.623⬝10⁹	(+0.89%)
`Mathlib.Algebra.Algebra.Subalgebra.Centralizer`	+1.623⬝10⁹	(+4.82%)
`Mathlib.Analysis.Normed.Group.SemiNormedGrp`	+1.617⬝10⁹	(+7.27%)
`Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex`	+1.595⬝10⁹	(+2.88%)
`Mathlib.CategoryTheory.Endofunctor.Algebra`	+1.579⬝10⁹	(+2.47%)
`Mathlib.LinearAlgebra.PerfectPairing.Restrict`	+1.574⬝10⁹	(+2.36%)
`Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear`	+1.548⬝10⁹	(+2.25%)
`Mathlib.CategoryTheory.Elements`	+1.541⬝10⁹	(+2.22%)
`Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves`	+1.530⬝10⁹	(+2.59%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf`	+1.527⬝10⁹	(+0.59%)
`Mathlib.CategoryTheory.Yoneda`	+1.510⬝10⁹	(+1.34%)
`Mathlib.Combinatorics.SimpleGraph.Operations`	+1.509⬝10⁹	(+7.91%)
`Mathlib.Algebra.Homology.ShortComplex.LeftHomology`	+1.498⬝10⁹	(+2.83%)
`Mathlib.CategoryTheory.Opposites`	+1.492⬝10⁹	(+3.33%)
`Mathlib.CategoryTheory.Limits.HasLimits`	+1.482⬝10⁹	(+1.86%)
`Mathlib.CategoryTheory.Adjunction.Over`	+1.471⬝10⁹	(+1.58%)
`Mathlib.GroupTheory.Coxeter.Matrix`	+1.446⬝10⁹	(+1.73%)
`Mathlib.Algebra.Homology.ShortComplex.Basic`	+1.443⬝10⁹	(+4.73%)
`Mathlib.CategoryTheory.Monoidal.CommMon_`	+1.413⬝10⁹	(+1.36%)
`Mathlib.CategoryTheory.Monoidal.Center`	+1.412⬝10⁹	(+2.16%)
`Mathlib.Algebra.Category.MonCat.Basic`	+1.408⬝10⁹	(+2.33%)
`Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts`	+1.399⬝10⁹	(+1.42%)
`Mathlib.CategoryTheory.Limits.Shapes.IsTerminal`	+1.395⬝10⁹	(+3.94%)
`Mathlib.Analysis.Calculus.ContDiff.Basic`	+1.385⬝10⁹	(+0.31%)
`Mathlib.CategoryTheory.Monoidal.Internal.Types`	+1.382⬝10⁹	(+2.63%)
`Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers`	+1.381⬝10⁹	(+3.56%)
`Mathlib.CategoryTheory.Subobject.MonoOver`	+1.377⬝10⁹	(+1.25%)
`Mathlib.CategoryTheory.FiberedCategory.BasedCategory`	+1.373⬝10⁹	(+3.76%)
`Mathlib.MeasureTheory.Group.GeometryOfNumbers`	+1.368⬝10⁹	(+3.94%)
`Mathlib.Algebra.Homology.TotalComplex`	+1.340⬝10⁹	(+3.59%)
`Mathlib.CategoryTheory.GradedObject`	+1.337⬝10⁹	(+2.21%)
`Mathlib.CategoryTheory.Bicategory.Coherence`	+1.325⬝10⁹	(+1.10%)
`Mathlib.Algebra.Homology.HomologySequence`	+1.324⬝10⁹	(+1.88%)
`Mathlib.CategoryTheory.Limits.Shapes.Diagonal`	+1.309⬝10⁹	(+0.83%)
`Mathlib.Algebra.Homology.ShortComplex.RightHomology`	+1.303⬝10⁹	(+1.97%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique`	+1.297⬝10⁹	(+0.85%)
`Aesop.Search.RuleSelection`	+1.293⬝10⁹	(+56.80%)
`Mathlib.Data.Matroid.Closure`	+1.287⬝10⁹	(+2.22%)
`Mathlib.Condensed.Discrete.Module`	+1.274⬝10⁹	(+1.11%)
`Mathlib.Probability.Kernel.Disintegration.Density`	+1.271⬝10⁹	(+2.93%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral`	+1.262⬝10⁹	(+3.30%)
`Mathlib.Algebra.Homology.ShortComplex.Linear`	+1.238⬝10⁹	(+2.29%)
`Mathlib.LinearAlgebra.Matrix.SesquilinearForm`	+1.229⬝10⁹	(+0.96%)
`Mathlib.RingTheory.Flat.FaithfullyFlat.Basic`	+1.219⬝10⁹	(+1.74%)
`Mathlib.GroupTheory.Coset.Card`	+1.218⬝10⁹	(+9.35%)
`Mathlib.Topology.Homotopy.HomotopyGroup`	+1.212⬝10⁹	(+1.44%)
`Mathlib.Analysis.Normed.Group.ZeroAtInfty`	+1.205⬝10⁹	(+14.59%)
`Mathlib.CategoryTheory.Monoidal.Bimon_`	+1.202⬝10⁹	(+1.41%)
`Mathlib.Algebra.Lie.LieTheorem`	+1.200⬝10⁹	(+1.69%)
`Mathlib.CategoryTheory.Monad.Algebra`	+1.193⬝10⁹	(+2.19%)
`Mathlib.CategoryTheory.Limits.IsLimit`	+1.185⬝10⁹	(+1.28%)
`Mathlib.Analysis.Complex.Tietze`	+1.183⬝10⁹	(+6.09%)
`Aesop.Util.UnionFind`	+1.175⬝10⁹	(+38.39%)
`Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections`	+1.175⬝10⁹	(+1.35%)
`Mathlib.CategoryTheory.Action.Basic`	+1.172⬝10⁹	(+1.99%)
`Mathlib.Analysis.Analytic.OfScalars`	+1.169⬝10⁹	(+2.36%)
`Mathlib.CategoryTheory.Adjunction.Basic`	+1.167⬝10⁹	(+1.98%)
`Mathlib.CategoryTheory.Monad.Products`	+1.163⬝10⁹	(+1.96%)
`Mathlib.CategoryTheory.Limits.Final`	+1.151⬝10⁹	(+0.63%)
`Mathlib.Analysis.CStarAlgebra.Module.Constructions`	+1.148⬝10⁹	(+1.51%)
`Mathlib.CategoryTheory.Triangulated.Rotate`	+1.138⬝10⁹	(+2.96%)
`Mathlib.Data.Sym.Sym2`	+1.135⬝10⁹	(+4.53%)
`Mathlib.Analysis.Convolution`	+1.132⬝10⁹	(+0.29%)
`Mathlib.Algebra.Homology.Additive`	+1.119⬝10⁹	(+1.52%)
`Mathlib.CategoryTheory.Monoidal.Braided.Basic`	+1.117⬝10⁹	(+1.30%)
`Mathlib.Algebra.Homology.ShortComplex.SnakeLemma`	+1.115⬝10⁹	(+1.13%)
`Mathlib.Analysis.Distribution.SchwartzSpace`	+1.114⬝10⁹	(+0.49%)
`Mathlib.Algebra.Category.Grp.Basic`	+1.106⬝10⁹	(+2.60%)
`Mathlib.CategoryTheory.Functor.FunctorHom`	+1.104⬝10⁹	(+2.78%)
`Mathlib.CategoryTheory.Abelian.Images`	+1.99⬝10⁹	(+3.31%)
`Mathlib.Analysis.Convex.Jensen`	+1.94⬝10⁹	(+2.39%)
`Aesop.Tree.ExtractScript`	+1.85⬝10⁹	(+12.54%)
`Mathlib.CategoryTheory.Adjunction.Limits`	+1.84⬝10⁹	(+1.90%)
`Mathlib.Condensed.Discrete.LocallyConstant`	+1.79⬝10⁹	(+1.30%)
`Mathlib.CategoryTheory.Triangulated.Basic`	+1.70⬝10⁹	(+3.43%)
`Mathlib.LinearAlgebra.PiTensorProduct`	+1.58⬝10⁹	(+0.71%)
`Mathlib.Algebra.Lie.Weights.Basic`	+1.50⬝10⁹	(+0.93%)
`Mathlib.CategoryTheory.Bicategory.SingleObj`	+1.45⬝10⁹	(+5.72%)
`Mathlib.CategoryTheory.Linear.Yoneda`	+1.43⬝10⁹	(+1.56%)
`Mathlib.Analysis.Convex.Combination`	+1.42⬝10⁹	(+0.88%)
`Mathlib.CategoryTheory.Triangulated.Pretriangulated`	+1.40⬝10⁹	(+2.31%)
`Mathlib.Algebra.Category.ModuleCat.Basic`	+1.38⬝10⁹	(+1.18%)
`Mathlib.Algebra.Homology.HomologicalBicomplex`	+1.35⬝10⁹	(+2.41%)
`Mathlib.CategoryTheory.Monoidal.Internal.Module`	+1.34⬝10⁹	(+0.73%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+1.34⬝10⁹	(+0.24%)
`Mathlib.RingTheory.TensorProduct.Basic`	+1.32⬝10⁹	(+0.32%)
`Mathlib.Algebra.Module.Presentation.Differentials`	+1.28⬝10⁹	(+1.59%)
`Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer`	+1.26⬝10⁹	(+1.12%)
`Mathlib.CategoryTheory.MorphismProperty.Comma`	+1.16⬝10⁹	(+2.82%)
`Aesop.Main`	+1.9⬝10⁹	(+16.36%)
`Mathlib.CategoryTheory.Limits.Shapes.Terminal`	+1.2⬝10⁹	(+4.62%)

3 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.AlgebraicGeometry.AffineSpace`	-1.6⬝10⁹	(-0.41%)
`Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing`	-1.68⬝10⁹	(-0.38%)
`Mathlib.Tactic.CC.Addition`	-1.255⬝10⁹	(-1.29%)

File	Instructions	%
`Batteries.Data.Array.Monadic`	-2.611⬝10⁹	(-24.61%)
`Mathlib.Topology.Sheaves.Presheaf`	-4.77⬝10⁹	(-5.53%)
`Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated`	-5.194⬝10⁹	(-4.17%)
`Batteries.Data.Array.Lemmas`	-19.282⬝10⁹	(-91.90%)
CI run

This is for the rule pattern indexing optimisation.

JLimperg · 2025-02-21T22:15:41Z

!bench

leanprover-bot · 2025-02-21T23:03:42Z

Here are the benchmark results for commit c1c080c.
There were significant changes against commit 50c9a9b:

  Benchmark                                                           Metric         Change
  =========================================================================================
- ~Aesop.RuleSet                                                      instructions    88.1%
- ~Aesop.Search.Main                                                  instructions   151.3%
+ ~Batteries.Data.Array.Lemmas                                        instructions   -91.9%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order   instructions    13.2%
- ~Mathlib.Analysis.Convex.Visible                                    instructions    33.3%
+ ~Mathlib.CategoryTheory.ComposableArrows                            instructions    -4.5%
- ~Mathlib.CategoryTheory.Triangulated.Functor                        instructions     4.3%
- ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct                  instructions    10.3%
- ~Mathlib.Probability.Kernel.Proper                                  instructions   112.4%
- ~Mathlib.Tactic.Module                                              instructions     9.1%

github-actions · 2025-02-21T23:04:06Z

File	Instructions	%
`build`	+867.53⬝10⁹	(+0.57%)
`lint`	-13.128⬝10⁹	(-0.17%)
`Mathlib.Probability.Kernel.Proper`	+66.789⬝10⁹	(+112.44%)
`Aesop.Search.Main`	+63.352⬝10⁹	(+151.32%)
`Mathlib.Analysis.Convex.Visible`	+32.462⬝10⁹	(+33.33%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	+24.872⬝10⁹	(+13.16%)
`Mathlib.LinearAlgebra.QuadraticForm.TensorProduct`	+15.599⬝10⁹	(+10.33%)
`Mathlib.Tactic.Module`	+14.27⬝10⁹	(+9.06%)
`Mathlib.CategoryTheory.Triangulated.Functor`	+13.256⬝10⁹	(+4.32%)
`Aesop.RuleSet`	+11.761⬝10⁹	(+88.06%)

2 files, Instructions +7.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.BilinearForm.TensorProduct`	+7.957⬝10⁹	(+12.24%)
`Mathlib.Lean.Meta.RefinedDiscrTree.Encode`	+7.816⬝10⁹	(+20.81%)

4 files, Instructions +6.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital`	+6.616⬝10⁹	(+2.82%)
`Aesop.Saturate`	+6.571⬝10⁹	(+72.07%)
`Mathlib.Algebra.Homology.HomotopyCategory.HomComplex`	+6.414⬝10⁹	(+7.59%)
`Mathlib.Combinatorics.SimpleGraph.Matching`	+6.36⬝10⁹	(+13.17%)

4 files, Instructions +5.0⬝10⁹

File	Instructions	%
`Mathlib.AlgebraicGeometry.Morphisms.AffineAnd`	+5.238⬝10⁹	(+16.32%)
`Mathlib.CategoryTheory.Triangulated.TriangleShift`	+5.182⬝10⁹	(+3.69%)
`Mathlib.Algebra.Homology.Bifunctor`	+5.58⬝10⁹	(+4.53%)
`Mathlib.MeasureTheory.Measure.Haar.OfBasis`	+5.35⬝10⁹	(+10.17%)

7 files, Instructions +4.0⬝10⁹

File	Instructions	%
`Aesop.Search.Expansion.Norm`	+4.871⬝10⁹	(+39.33%)
`Mathlib.Probability.StrongLaw`	+4.777⬝10⁹	(+6.34%)
`Mathlib.SetTheory.Game.PGame`	+4.519⬝10⁹	(+6.79%)
`Mathlib.Algebra.Homology.HomotopyCategory.Shift`	+4.452⬝10⁹	(+8.91%)
`Mathlib.Analysis.CStarAlgebra.ApproximateUnit`	+4.357⬝10⁹	(+2.98%)
`Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion`	+4.273⬝10⁹	(+31.95%)
`Mathlib.Analysis.Analytic.Inverse`	+4.193⬝10⁹	(+3.22%)

6 files, Instructions +3.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances`	+3.925⬝10⁹	(+2.04%)
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic`	+3.877⬝10⁹	(+2.75%)
`Mathlib.LinearAlgebra.Matrix.FixedDetMatrices`	+3.769⬝10⁹	(+12.57%)
`Mathlib.LinearAlgebra.ExteriorPower.Basic`	+3.717⬝10⁹	(+5.76%)
`Aesop.Search.Expansion`	+3.376⬝10⁹	(+15.17%)
`Mathlib.Combinatorics.Additive.FreimanHom`	+3.111⬝10⁹	(+5.99%)

13 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Aesop.RuleTac.Forward`	+2.992⬝10⁹	(+43.95%)
`Mathlib.SetTheory.Game.Basic`	+2.907⬝10⁹	(+3.49%)
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart`	+2.853⬝10⁹	(+2.28%)
`Mathlib.Algebra.BigOperators.Finprod`	+2.711⬝10⁹	(+5.31%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric`	+2.704⬝10⁹	(+1.64%)
`Mathlib.Analysis.RCLike.Basic`	+2.532⬝10⁹	(+2.22%)
`Batteries.Data.Array.Match`	+2.468⬝10⁹	(+169.68%)
`Batteries.Data.LazyList`	+2.430⬝10⁹	(+35.27%)
`Aesop.Builder.Forward`	+2.259⬝10⁹	(+41.86%)
`Mathlib.NumberTheory.ArithmeticFunction`	+2.199⬝10⁹	(+2.93%)
`Mathlib.Data.Nat.Factors`	+2.129⬝10⁹	(+23.48%)
`Aesop.Tree.AddRapp`	+2.93⬝10⁹	(+18.93%)
`Mathlib.RingTheory.Regular.RegularSequence`	+2.60⬝10⁹	(+2.28%)

34 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.LinearIndependent`	+1.949⬝10⁹	(+1.36%)
`Aesop.RuleTac.GoalDiff`	+1.932⬝10⁹	(+28.85%)
`Mathlib.RingTheory.IntegralClosure.IntegrallyClosed`	+1.931⬝10⁹	(+7.08%)
`Mathlib.Combinatorics.SimpleGraph.Path`	+1.927⬝10⁹	(+4.75%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic`	+1.857⬝10⁹	(+0.96%)
`Mathlib.Computability.AkraBazzi.AkraBazzi`	+1.834⬝10⁹	(+1.12%)
`Aesop.Tree.Tracing`	+1.798⬝10⁹	(+32.37%)
`Mathlib.SetTheory.Lists`	+1.762⬝10⁹	(+10.48%)
`Mathlib.Tactic.FailIfNoProgress`	+1.697⬝10⁹	(+44.10%)
`Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone`	+1.695⬝10⁹	(+1.67%)
`Aesop.Util.Basic`	+1.675⬝10⁹	(+15.81%)
`Mathlib.Algebra.Order.BigOperators.Ring.Finset`	+1.648⬝10⁹	(+4.04%)
`Mathlib.Analysis.InnerProductSpace.Positive`	+1.557⬝10⁹	(+4.17%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital`	+1.541⬝10⁹	(+1.05%)
`Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear`	+1.444⬝10⁹	(+2.09%)
`Mathlib.Analysis.Convex.Birkhoff`	+1.436⬝10⁹	(+4.27%)
`Mathlib.Combinatorics.Enumerative.IncidenceAlgebra`	+1.424⬝10⁹	(+2.29%)
`Mathlib.Analysis.Calculus.ContDiff.Basic`	+1.391⬝10⁹	(+0.32%)
`Aesop.Search.RuleSelection`	+1.293⬝10⁹	(+56.83%)
`Mathlib.Algebra.Algebra.Subalgebra.Centralizer`	+1.264⬝10⁹	(+3.75%)
`Mathlib.LinearAlgebra.PerfectPairing.Restrict`	+1.218⬝10⁹	(+1.82%)
`Aesop.Util.UnionFind`	+1.176⬝10⁹	(+38.39%)
`Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic`	+1.171⬝10⁹	(+1.34%)
`Mathlib.Probability.Kernel.Disintegration.Density`	+1.170⬝10⁹	(+2.70%)
`Mathlib.Analysis.Convolution`	+1.134⬝10⁹	(+0.29%)
`Mathlib.Analysis.Complex.Tietze`	+1.121⬝10⁹	(+5.77%)
`Mathlib.Analysis.Normed.Group.ZeroAtInfty`	+1.100⬝10⁹	(+13.32%)
`Aesop.Tree.ExtractScript`	+1.83⬝10⁹	(+12.52%)
`Mathlib.RingTheory.Flat.FaithfullyFlat.Basic`	+1.79⬝10⁹	(+1.54%)
`Mathlib.Analysis.Normed.Group.SemiNormedGrp`	+1.77⬝10⁹	(+4.84%)
`Mathlib.RingTheory.TensorProduct.Basic`	+1.65⬝10⁹	(+0.33%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+1.44⬝10⁹	(+0.25%)
`Aesop.Main`	+1.7⬝10⁹	(+16.34%)
`Mathlib.Algebra.Lie.Weights.Basic`	+1.6⬝10⁹	(+0.89%)

32 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings`	-1.4⬝10⁹	(-1.40%)
`Mathlib.Algebra.Module.Presentation.Tensor`	-1.14⬝10⁹	(-6.01%)
`Mathlib.CategoryTheory.Linear.Yoneda`	-1.25⬝10⁹	(-1.54%)
`Mathlib.Algebra.Polynomial.Module.AEval`	-1.47⬝10⁹	(-1.19%)
`Mathlib.AlgebraicGeometry.AffineSpace`	-1.50⬝10⁹	(-0.42%)
`Mathlib.CategoryTheory.Limits.Final`	-1.62⬝10⁹	(-0.58%)
`Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing`	-1.67⬝10⁹	(-0.38%)
`Mathlib.CategoryTheory.MorphismProperty.OverAdjunction`	-1.111⬝10⁹	(-1.15%)
`Mathlib.CategoryTheory.GradedObject.Bifunctor`	-1.163⬝10⁹	(-1.67%)
`Mathlib.CategoryTheory.Products.Basic`	-1.173⬝10⁹	(-1.35%)
`Mathlib.Algebra.Homology.DifferentialObject`	-1.199⬝10⁹	(-2.20%)
`Mathlib.Tactic.CC.Addition`	-1.228⬝10⁹	(-1.26%)
`Mathlib.Algebra.Homology.HomologicalBicomplex`	-1.240⬝10⁹	(-2.89%)
`Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory`	-1.268⬝10⁹	(-2.02%)
`Mathlib.CategoryTheory.Action.Basic`	-1.271⬝10⁹	(-2.16%)
`Mathlib.AlgebraicTopology.SimplicialNerve`	-1.314⬝10⁹	(-0.99%)
`Mathlib.CategoryTheory.Subobject.Lattice`	-1.329⬝10⁹	(-0.99%)
`Mathlib.Algebra.Homology.HomologySequence`	-1.336⬝10⁹	(-1.90%)
`Mathlib.CategoryTheory.Monoidal.Internal.Types`	-1.368⬝10⁹	(-2.60%)
`Mathlib.CategoryTheory.Limits.Constructions.Filtered`	-1.379⬝10⁹	(-1.97%)
`Mathlib.CategoryTheory.Elements`	-1.383⬝10⁹	(-1.99%)
`Mathlib.CategoryTheory.Subobject.MonoOver`	-1.556⬝10⁹	(-1.41%)
`Mathlib.CategoryTheory.Adjunction.Limits`	-1.677⬝10⁹	(-2.94%)
`Mathlib.CategoryTheory.Limits.HasLimits`	-1.683⬝10⁹	(-2.12%)
`Mathlib.CategoryTheory.Limits.Constructions.Over.Products`	-1.737⬝10⁹	(-2.14%)
`Mathlib.CategoryTheory.Abelian.Images`	-1.790⬝10⁹	(-5.39%)
`Mathlib.CategoryTheory.Monoidal.Mon_`	-1.809⬝10⁹	(-1.26%)
`Mathlib.CategoryTheory.Whiskering`	-1.816⬝10⁹	(-0.70%)
`Mathlib.CategoryTheory.Monoidal.Internal.Module`	-1.856⬝10⁹	(-1.31%)
`Mathlib.CategoryTheory.Monad.Algebra`	-1.860⬝10⁹	(-3.41%)
`Mathlib.CategoryTheory.Functor.CurryingThree`	-1.891⬝10⁹	(-1.11%)
`Mathlib.CategoryTheory.Closed.FunctorCategory.Basic`	-1.987⬝10⁹	(-6.08%)

13 files, Instructions -3.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Limits.ConeCategory`	-2.127⬝10⁹	(-2.49%)
`Mathlib.CategoryTheory.Triangulated.Rotate`	-2.130⬝10⁹	(-5.54%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf`	-2.207⬝10⁹	(-0.85%)
`Mathlib.CategoryTheory.Comma.StructuredArrow.Basic`	-2.275⬝10⁹	(-0.72%)
`Mathlib.CategoryTheory.Monoidal.Center`	-2.326⬝10⁹	(-3.56%)
`Mathlib.CategoryTheory.Triangulated.Opposite.Triangle`	-2.425⬝10⁹	(-1.81%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward`	-2.429⬝10⁹	(-1.93%)
`Batteries.Data.Array.Monadic`	-2.611⬝10⁹	(-24.61%)
`Mathlib.CategoryTheory.Square`	-2.657⬝10⁹	(-3.73%)
`Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence`	-2.677⬝10⁹	(-2.66%)
`Mathlib.CategoryTheory.Endofunctor.Algebra`	-2.778⬝10⁹	(-4.35%)
`Mathlib.AlgebraicTopology.CechNerve`	-2.799⬝10⁹	(-1.55%)
`Mathlib.CategoryTheory.Monad.Products`	-2.978⬝10⁹	(-5.03%)

6 files, Instructions -4.0⬝10⁹

File	Instructions	%
`Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts`	-3.159⬝10⁹	(-2.67%)
`Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer`	-3.176⬝10⁹	(-3.48%)
`Mathlib.CategoryTheory.Adjunction.Over`	-3.200⬝10⁹	(-3.44%)
`Mathlib.CategoryTheory.Monoidal.Bimon_`	-3.203⬝10⁹	(-3.76%)
`Mathlib.CategoryTheory.Adjunction.Evaluation`	-3.419⬝10⁹	(-4.21%)
`Mathlib.CategoryTheory.Functor.Currying`	-3.910⬝10⁹	(-3.63%)

6 files, Instructions -5.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Limits.Shapes.Biproducts`	-4.43⬝10⁹	(-1.56%)
`Mathlib.CategoryTheory.Monad.EquivMon`	-4.159⬝10⁹	(-10.02%)
`Mathlib.CategoryTheory.GradedObject.Trifunctor`	-4.269⬝10⁹	(-1.70%)
`Mathlib.AlgebraicTopology.SimplicialObject.Basic`	-4.323⬝10⁹	(-2.07%)
`Mathlib.CategoryTheory.Comma.Basic`	-4.470⬝10⁹	(-2.32%)
`Mathlib.CategoryTheory.Comma.Over`	-4.641⬝10⁹	(-1.53%)

3 files, Instructions -6.0⬝10⁹

File	Instructions	%
`Mathlib.Topology.Sheaves.Presheaf`	-5.393⬝10⁹	(-7.32%)
`Mathlib.Algebra.Homology.ShortComplex.SnakeLemma`	-5.447⬝10⁹	(-5.56%)
`Mathlib.CategoryTheory.Functor.Trifunctor`	-5.659⬝10⁹	(-3.37%)

2 files, Instructions -8.0⬝10⁹

File	Instructions	%
`Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated`	-7.37⬝10⁹	(-5.65%)
`Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory`	-7.688⬝10⁹	(-5.18%)

File	Instructions	%
`Mathlib.CategoryTheory.Limits.Cones`	-8.170⬝10⁹	(-2.63%)
`Mathlib.CategoryTheory.ComposableArrows`	-13.623⬝10⁹	(-4.49%)
`Batteries.Data.Array.Lemmas`	-19.282⬝10⁹	(-91.90%)
CI run

JLimperg · 2025-02-26T14:41:56Z

!bench

leanprover-bot · 2025-02-26T15:13:17Z

Here are the benchmark results for commit b41ea7f.
There were significant changes against commit 50c9a9b:

  Benchmark                                  Metric         Change
  ================================================================
+ build                                      aesop           -7.5%
- ~Aesop.RuleSet                             instructions    88.0%
- ~Aesop.Search.Main                         instructions   151.3%
+ ~Batteries.Data.Array.Lemmas               instructions   -91.9%
+ ~Mathlib.CategoryTheory.ComposableArrows   instructions    -4.5%
- ~Mathlib.Tactic.Module                     instructions     9.1%

github-actions · 2025-02-26T15:13:51Z

File	Instructions	%
`build`	+612.210⬝10⁹	(+0.40%)
`lint`	-13.122⬝10⁹	(-0.17%)
`Aesop.Search.Main`	+63.328⬝10⁹	(+151.26%)
`Mathlib.Tactic.Module`	+14.17⬝10⁹	(+9.06%)
`Aesop.RuleSet`	+11.758⬝10⁹	(+88.04%)

2 files, Instructions +7.0⬝10⁹

File	Instructions	%
`Mathlib.Lean.Meta.RefinedDiscrTree.Encode`	+7.817⬝10⁹	(+20.81%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order`	+7.142⬝10⁹	(+3.78%)

File	Instructions	%
`Aesop.Saturate`	+6.569⬝10⁹	(+72.04%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital`	+5.790⬝10⁹	(+2.47%)

4 files, Instructions +4.0⬝10⁹

File	Instructions	%
`Aesop.Search.Expansion.Norm`	+4.873⬝10⁹	(+39.34%)
`Mathlib.SetTheory.Game.PGame`	+4.512⬝10⁹	(+6.78%)
`Mathlib.Probability.StrongLaw`	+4.345⬝10⁹	(+5.76%)
`Mathlib.Analysis.Analytic.Inverse`	+4.193⬝10⁹	(+3.22%)

3 files, Instructions +3.0⬝10⁹

File	Instructions	%
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic`	+3.863⬝10⁹	(+2.74%)
`Aesop.Search.Expansion`	+3.375⬝10⁹	(+15.16%)
`Mathlib.MeasureTheory.Measure.Haar.OfBasis`	+3.158⬝10⁹	(+6.38%)

10 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Aesop.RuleTac.Forward`	+2.993⬝10⁹	(+43.97%)
`Mathlib.SetTheory.Game.Basic`	+2.912⬝10⁹	(+3.49%)
`Mathlib.Algebra.BigOperators.Finprod`	+2.709⬝10⁹	(+5.31%)
`Batteries.Data.Array.Match`	+2.468⬝10⁹	(+169.69%)
`Batteries.Data.LazyList`	+2.430⬝10⁹	(+35.27%)
`Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart`	+2.293⬝10⁹	(+1.83%)
`Aesop.Builder.Forward`	+2.259⬝10⁹	(+41.87%)
`Mathlib.Data.Nat.Factors`	+2.129⬝10⁹	(+23.48%)
`Aesop.Tree.AddRapp`	+2.93⬝10⁹	(+18.92%)
`Mathlib.RingTheory.Regular.RegularSequence`	+2.59⬝10⁹	(+2.28%)

25 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.LinearAlgebra.LinearIndependent`	+1.947⬝10⁹	(+1.36%)
`Aesop.RuleTac.GoalDiff`	+1.933⬝10⁹	(+28.86%)
`Mathlib.Combinatorics.SimpleGraph.Path`	+1.926⬝10⁹	(+4.74%)
`Mathlib.LinearAlgebra.Matrix.FixedDetMatrices`	+1.840⬝10⁹	(+6.14%)
`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic`	+1.839⬝10⁹	(+0.95%)
`Aesop.Tree.Tracing`	+1.797⬝10⁹	(+32.36%)
`Mathlib.SetTheory.Lists`	+1.763⬝10⁹	(+10.49%)
`Mathlib.Tactic.FailIfNoProgress`	+1.697⬝10⁹	(+44.08%)
`Aesop.Util.Basic`	+1.674⬝10⁹	(+15.80%)
`Mathlib.Algebra.Order.BigOperators.Ring.Finset`	+1.649⬝10⁹	(+4.04%)
`Mathlib.Computability.AkraBazzi.AkraBazzi`	+1.448⬝10⁹	(+0.89%)
`Mathlib.Combinatorics.Enumerative.IncidenceAlgebra`	+1.425⬝10⁹	(+2.29%)
`Mathlib.Analysis.Calculus.ContDiff.Basic`	+1.394⬝10⁹	(+0.32%)
`Aesop.Search.RuleSelection`	+1.292⬝10⁹	(+56.76%)
`Mathlib.Algebra.Algebra.Subalgebra.Centralizer`	+1.264⬝10⁹	(+3.75%)
`Mathlib.LinearAlgebra.PerfectPairing.Restrict`	+1.215⬝10⁹	(+1.82%)
`Aesop.Util.UnionFind`	+1.174⬝10⁹	(+38.34%)
`Mathlib.Analysis.Convolution`	+1.153⬝10⁹	(+0.30%)
`Mathlib.Analysis.Complex.Tietze`	+1.119⬝10⁹	(+5.76%)
`Aesop.Tree.ExtractScript`	+1.89⬝10⁹	(+12.59%)
`Mathlib.RingTheory.IntegralClosure.IntegrallyClosed`	+1.82⬝10⁹	(+3.97%)
`Mathlib.RingTheory.Flat.FaithfullyFlat.Basic`	+1.77⬝10⁹	(+1.53%)
`Mathlib.RingTheory.TensorProduct.Basic`	+1.68⬝10⁹	(+0.33%)
`Mathlib.Analysis.Calculus.FDeriv.Mul`	+1.29⬝10⁹	(+0.24%)
`Aesop.Main`	+1.8⬝10⁹	(+16.36%)

33 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap`	-1.2⬝10⁹	(-0.85%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings`	-1.5⬝10⁹	(-1.40%)
`Mathlib.Algebra.Module.Presentation.Tensor`	-1.14⬝10⁹	(-6.02%)
`Mathlib.CategoryTheory.Linear.Yoneda`	-1.19⬝10⁹	(-1.53%)
`Mathlib.Algebra.Polynomial.Module.AEval`	-1.48⬝10⁹	(-1.19%)
`Mathlib.AlgebraicGeometry.AffineSpace`	-1.49⬝10⁹	(-0.42%)
`Mathlib.CategoryTheory.Limits.Final`	-1.54⬝10⁹	(-0.57%)
`Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing`	-1.75⬝10⁹	(-0.38%)
`Mathlib.CategoryTheory.MorphismProperty.OverAdjunction`	-1.121⬝10⁹	(-1.16%)
`Mathlib.CategoryTheory.GradedObject.Bifunctor`	-1.164⬝10⁹	(-1.67%)
`Mathlib.CategoryTheory.Products.Basic`	-1.173⬝10⁹	(-1.35%)
`Mathlib.Algebra.Homology.DifferentialObject`	-1.198⬝10⁹	(-2.20%)
`Mathlib.Algebra.Homology.HomologicalBicomplex`	-1.235⬝10⁹	(-2.88%)
`Mathlib.Tactic.CC.Addition`	-1.238⬝10⁹	(-1.27%)
`Mathlib.CategoryTheory.Action.Basic`	-1.270⬝10⁹	(-2.16%)
`Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory`	-1.271⬝10⁹	(-2.02%)
`Mathlib.AlgebraicTopology.SimplicialNerve`	-1.317⬝10⁹	(-0.99%)
`Mathlib.CategoryTheory.Subobject.Lattice`	-1.323⬝10⁹	(-0.99%)
`Mathlib.Algebra.Homology.HomologySequence`	-1.340⬝10⁹	(-1.90%)
`Mathlib.CategoryTheory.Monoidal.Internal.Types`	-1.366⬝10⁹	(-2.60%)
`Mathlib.CategoryTheory.Limits.Constructions.Filtered`	-1.380⬝10⁹	(-1.97%)
`Mathlib.CategoryTheory.Elements`	-1.381⬝10⁹	(-1.99%)
`Mathlib.CategoryTheory.Subobject.MonoOver`	-1.560⬝10⁹	(-1.41%)
`Mathlib.CategoryTheory.Adjunction.Limits`	-1.678⬝10⁹	(-2.94%)
`Mathlib.CategoryTheory.Limits.HasLimits`	-1.682⬝10⁹	(-2.12%)
`Mathlib.CategoryTheory.Limits.Constructions.Over.Products`	-1.738⬝10⁹	(-2.14%)
`Mathlib.CategoryTheory.Abelian.Images`	-1.793⬝10⁹	(-5.40%)
`Mathlib.CategoryTheory.Monoidal.Mon_`	-1.808⬝10⁹	(-1.26%)
`Mathlib.CategoryTheory.Monoidal.Internal.Module`	-1.834⬝10⁹	(-1.29%)
`Mathlib.CategoryTheory.Whiskering`	-1.835⬝10⁹	(-0.70%)
`Mathlib.CategoryTheory.Monad.Algebra`	-1.860⬝10⁹	(-3.41%)
`Mathlib.CategoryTheory.Functor.CurryingThree`	-1.908⬝10⁹	(-1.12%)
`Mathlib.CategoryTheory.Closed.FunctorCategory.Basic`	-1.985⬝10⁹	(-6.08%)

14 files, Instructions -3.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Homology.Bifunctor`	-2.15⬝10⁹	(-1.80%)
`Mathlib.CategoryTheory.Limits.ConeCategory`	-2.123⬝10⁹	(-2.48%)
`Mathlib.CategoryTheory.Triangulated.Rotate`	-2.128⬝10⁹	(-5.54%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf`	-2.212⬝10⁹	(-0.85%)
`Mathlib.CategoryTheory.Comma.StructuredArrow.Basic`	-2.269⬝10⁹	(-0.72%)
`Mathlib.CategoryTheory.Monoidal.Center`	-2.327⬝10⁹	(-3.56%)
`Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward`	-2.445⬝10⁹	(-1.94%)
`Mathlib.CategoryTheory.Triangulated.Opposite.Triangle`	-2.450⬝10⁹	(-1.83%)
`Batteries.Data.Array.Monadic`	-2.611⬝10⁹	(-24.61%)
`Mathlib.CategoryTheory.Square`	-2.659⬝10⁹	(-3.73%)
`Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence`	-2.671⬝10⁹	(-2.65%)
`Mathlib.CategoryTheory.Endofunctor.Algebra`	-2.777⬝10⁹	(-4.35%)
`Mathlib.AlgebraicTopology.CechNerve`	-2.801⬝10⁹	(-1.55%)
`Mathlib.CategoryTheory.Monad.Products`	-2.979⬝10⁹	(-5.03%)

6 files, Instructions -4.0⬝10⁹

File	Instructions	%
`Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts`	-3.150⬝10⁹	(-2.66%)
`Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer`	-3.175⬝10⁹	(-3.48%)
`Mathlib.CategoryTheory.Adjunction.Over`	-3.203⬝10⁹	(-3.44%)
`Mathlib.CategoryTheory.Monoidal.Bimon_`	-3.204⬝10⁹	(-3.76%)
`Mathlib.CategoryTheory.Adjunction.Evaluation`	-3.421⬝10⁹	(-4.21%)
`Mathlib.CategoryTheory.Functor.Currying`	-3.910⬝10⁹	(-3.63%)

6 files, Instructions -5.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Limits.Shapes.Biproducts`	-4.52⬝10⁹	(-1.56%)
`Mathlib.CategoryTheory.Monad.EquivMon`	-4.159⬝10⁹	(-10.02%)
`Mathlib.CategoryTheory.GradedObject.Trifunctor`	-4.272⬝10⁹	(-1.70%)
`Mathlib.AlgebraicTopology.SimplicialObject.Basic`	-4.306⬝10⁹	(-2.06%)
`Mathlib.CategoryTheory.Comma.Basic`	-4.485⬝10⁹	(-2.33%)
`Mathlib.CategoryTheory.Comma.Over`	-4.652⬝10⁹	(-1.53%)

3 files, Instructions -6.0⬝10⁹

File	Instructions	%
`Mathlib.Topology.Sheaves.Presheaf`	-5.394⬝10⁹	(-7.32%)
`Mathlib.Algebra.Homology.ShortComplex.SnakeLemma`	-5.450⬝10⁹	(-5.56%)
`Mathlib.CategoryTheory.Functor.Trifunctor`	-5.648⬝10⁹	(-3.36%)

2 files, Instructions -7.0⬝10⁹

File	Instructions	%
`Mathlib.CategoryTheory.Triangulated.Functor`	-6.352⬝10⁹	(-2.07%)
`Mathlib.CategoryTheory.Triangulated.TriangleShift`	-6.852⬝10⁹	(-4.88%)

2 files, Instructions -8.0⬝10⁹

File	Instructions	%
`Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated`	-7.37⬝10⁹	(-5.65%)
`Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory`	-7.685⬝10⁹	(-5.18%)

File	Instructions	%
`Mathlib.CategoryTheory.Limits.Cones`	-8.155⬝10⁹	(-2.62%)
`Mathlib.CategoryTheory.ComposableArrows`	-13.595⬝10⁹	(-4.48%)
`Batteries.Data.Array.Lemmas`	-19.282⬝10⁹	(-91.90%)
CI run

leanprover-community-mathlib4-bot and others added 30 commits January 25, 2025 03:32

Merge master into nightly-testing

5093f11

Merge remote-tracking branch 'origin/master' into bump/v4.17.0

aa380f9

Merge commit '3e696a8a9edeb0fca0e1a9df552c7e91d2aca018' into bump/nig…

c4d9aec

…htly-2025-01-24

chore: adaptations for nightly-2025-01-24

e7a16c3

Merge branch 'bump/nightly-2025-01-24' into nightly-testing

b87ff2d

Merge master into nightly-testing

3b0ef5a

chore: adaptations for nightly-2025-01-24 (#21042)

a36212b

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kim Morrison <kim@tqft.net>

chore: bump to nightly-2025-01-25

bd03465

Merge master into nightly-testing

578b8b9

Merge master into nightly-testing

49d8404

Merge master into nightly-testing

ab4ac9f

Merge master into nightly-testing

70d13e4

Merge master into nightly-testing

114cad0

Merge master into nightly-testing

d7d567d

Merge master into nightly-testing

76bcccf

chore: bump to nightly-2025-01-26

b36f8b2

Merge master into nightly-testing

7736b66

Merge master into nightly-testing

ea52118

Merge master into nightly-testing

3933573

Merge master into nightly-testing

e7928cb

Merge master into nightly-testing

095f4e4

Merge master into nightly-testing

16e0f54

Merge master into nightly-testing

11c83ea

Merge master into nightly-testing

6184acb

chore: bump to nightly-2025-01-27

06a08ac

Merge master into nightly-testing

94c6906

Adaption for leanprover/lean4#6755

5011e47

Auto-resolved conflicts in lean-toolchain and lake-manifest.json

aab2f37

chore: adaptations for nightly-2025-01-27

a445f3c

chore: adaptations for nightly-2025-01-27 (#21124)

6e39f2c

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Johan Commelin <johan@commelin.net>

leanprover-community-mathlib4-bot and others added 13 commits February 8, 2025 12:41

Merge master into nightly-testing

3e953be

Merge master into nightly-testing

1bedc17

Merge master into nightly-testing

b500914

Merge master into nightly-testing

5c59e14

update

7edff82

Merge master into nightly-testing

43c3ae0

chore: bump to nightly-2025-02-09

47888ee

Merge master into nightly-testing

fb2055d

Merge master into nightly-testing

6163849

Add test script

72b2517

Use Aesop@forward-test-master-precomp

cf1f9c2

Increase maxHeartbeats and enable stats collection

4748210

Use Aesop with pr-release toolchain

cbce978

leanprover-community-bot-assistant 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 10, 2025

Update Aesop

43858d3

Update Aesop

c1c080c

This is for the rule pattern indexing optimisation.

Fix not_prime_zero and not_prime_one rules

b41ea7f

Conversation

JLimperg commented Feb 9, 2025

Uh oh!

JLimperg commented Feb 9, 2025

Uh oh!

github-actions bot commented Feb 9, 2025

PR summary cbce97806d

Import changes for modified files

Declarations diff

Uh oh!

leanprover-bot commented Feb 9, 2025

Uh oh!

github-actions bot commented Feb 9, 2025

Uh oh!

JLimperg commented Feb 19, 2025

Uh oh!

leanprover-bot commented Feb 20, 2025

Uh oh!

github-actions bot commented Feb 20, 2025

Uh oh!

JLimperg commented Feb 21, 2025

Uh oh!

leanprover-bot commented Feb 21, 2025

Uh oh!

github-actions bot commented Feb 21, 2025

Uh oh!

JLimperg commented Feb 26, 2025

Uh oh!

leanprover-bot commented Feb 26, 2025

Uh oh!

github-actions bot commented Feb 26, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

10 participants