Aesop forward benchmark: master no-precomp

[JLimperg]

Not a real PR, just for benchmarking.

[JLimperg]

!bench

[github-actions]

PR summary 7d48d4483c

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]

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

  Benchmark                      Metric         Change
  ====================================================
+ ~Batteries.Data.Array.Lemmas   instructions   -91.9%
- ~Mathlib.Tactic.Module         instructions     9.0%

[github-actions]

File	Instructions	%
build	+461.41⬝10⁹	(+0.30%)
lint	-12.431⬝10⁹	(-0.16%)
Mathlib.Tactic.Module	+13.974⬝10⁹	(+9.03%)

2 files, Instructions +7.0⬝10⁹

File	Instructions	%
Mathlib.Lean.Meta.RefinedDiscrTree.Encode	+7.811⬝10⁹	(+20.79%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order	+7.103⬝10⁹	(+3.76%)

4 files, Instructions +4.0⬝10⁹

File	Instructions	%
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital	+4.713⬝10⁹	(+2.01%)
Mathlib.SetTheory.Game.PGame	+4.419⬝10⁹	(+6.64%)
Mathlib.Probability.StrongLaw	+4.304⬝10⁹	(+5.71%)
Mathlib.Analysis.Analytic.Inverse	+4.141⬝10⁹	(+3.19%)

2 files, Instructions +3.0⬝10⁹

File	Instructions	%
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic	+3.635⬝10⁹	(+2.58%)
Mathlib.MeasureTheory.Measure.Haar.OfBasis	+3.340⬝10⁹	(+6.75%)

8 files, Instructions +2.0⬝10⁹

File	Instructions	%
Mathlib.SetTheory.Game.Basic	+2.768⬝10⁹	(+3.32%)
Mathlib.Algebra.BigOperators.Finprod	+2.598⬝10⁹	(+5.09%)
Batteries.Data.Array.Match	+2.468⬝10⁹	(+169.68%)
Batteries.Data.LazyList	+2.430⬝10⁹	(+35.27%)
Mathlib.LinearAlgebra.LinearIndependent	+2.152⬝10⁹	(+1.50%)
Mathlib.Data.Nat.Factors	+2.99⬝10⁹	(+23.16%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart	+2.89⬝10⁹	(+1.67%)
Mathlib.RingTheory.Regular.RegularSequence	+2.20⬝10⁹	(+2.24%)

17 files, Instructions +1.0⬝10⁹

File	Instructions	%
Mathlib.Combinatorics.SimpleGraph.Path	+1.912⬝10⁹	(+4.71%)
Mathlib.LinearAlgebra.Matrix.FixedDetMatrices	+1.802⬝10⁹	(+6.01%)
Mathlib.SetTheory.Lists	+1.725⬝10⁹	(+10.27%)
Mathlib.Tactic.FailIfNoProgress	+1.698⬝10⁹	(+44.11%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic	+1.692⬝10⁹	(+0.87%)
Mathlib.Algebra.Order.BigOperators.Ring.Finset	+1.503⬝10⁹	(+3.68%)
Mathlib.Combinatorics.Enumerative.IncidenceAlgebra	+1.373⬝10⁹	(+2.21%)
Mathlib.Analysis.Calculus.ContDiff.Basic	+1.339⬝10⁹	(+0.30%)
Mathlib.Algebra.Algebra.Subalgebra.Centralizer	+1.241⬝10⁹	(+3.68%)
Mathlib.Analysis.Convolution	+1.115⬝10⁹	(+0.29%)
Mathlib.LinearAlgebra.PerfectPairing.Restrict	+1.112⬝10⁹	(+1.66%)
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed	+1.78⬝10⁹	(+3.95%)
Mathlib.RingTheory.Flat.FaithfullyFlat.Basic	+1.67⬝10⁹	(+1.52%)
Mathlib.Analysis.Complex.Tietze	+1.59⬝10⁹	(+5.45%)
Mathlib.Computability.AkraBazzi.AkraBazzi	+1.44⬝10⁹	(+0.64%)
Mathlib.RingTheory.TensorProduct.Basic	+1.24⬝10⁹	(+0.31%)
Mathlib.Analysis.Convex.Combination	+1.9⬝10⁹	(+0.85%)

5 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.AlgebraicGeometry.AffineSpace	-1.2⬝10⁹	(-0.41%)
Mathlib.Algebra.Category.ModuleCat.Presheaf	-1.66⬝10⁹	(-0.41%)
Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing	-1.96⬝10⁹	(-0.39%)
Mathlib.Tactic.CC.Addition	-1.251⬝10⁹	(-1.29%)
Mathlib.CategoryTheory.Triangulated.Functor	-1.781⬝10⁹	(-0.58%)

File	Instructions	%
Batteries.Data.Array.Monadic	-2.611⬝10⁹	(-24.61%)
Batteries.Data.Array.Lemmas	-19.282⬝10⁹	(-91.90%)
CI run