toolchain

[mattrobball]

---

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6f654cb.
There were significant changes against commit e0219f6:

  Benchmark                                                   Metric         Change
  =================================================================================
+ build                                                       elaboration     -5.7%
- build                                                       wall-clock      36.9%
+ ~Mathlib.Algebra.DirectLimit                                instructions   -15.7%
+ ~Mathlib.Algebra.Lie.Quotient                               instructions   -72.4%
+ ~Mathlib.Algebra.Module.Submodule.Localization              instructions   -52.1%
+ ~Mathlib.Analysis.Normed.Group.Quotient                     instructions   -75.2%
+ ~Mathlib.CategoryTheory.Generator                           instructions   -48.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure           instructions   -44.0%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits   instructions   -11.6%
+ ~Mathlib.GroupTheory.Coset                                  instructions   -79.1%
+ ~Mathlib.GroupTheory.GroupAction.Quotient                   instructions   -76.8%
+ ~Mathlib.GroupTheory.QuotientGroup                          instructions   -34.3%
+ ~Mathlib.LinearAlgebra.Isomorphisms                         instructions   -58.1%
+ ~Mathlib.LinearAlgebra.Quotient                             instructions   -28.7%
+ ~Mathlib.LinearAlgebra.QuotientPi                           instructions   -68.3%
+ ~Mathlib.LinearAlgebra.SModEq                               instructions   -89.4%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient                instructions   -54.9%
+ ~Mathlib.RingTheory.Smooth.Basic                            instructions   -42.6%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring              instructions   -22.5%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module                instructions   -60.3%
+ ~Mathlib.Topology.Instances.AddCircle                       instructions   -59.4%

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 4753ee1.
There were significant changes against commit e0219f6:

  Benchmark                                                   Metric         Change
  =================================================================================
+ build                                                       elaboration     -6.6%
+ ~Mathlib.Algebra.DirectLimit                                instructions   -15.7%
+ ~Mathlib.Algebra.Lie.Quotient                               instructions   -72.4%
+ ~Mathlib.Algebra.Module.Submodule.Localization              instructions   -52.1%
+ ~Mathlib.Analysis.Normed.Group.Quotient                     instructions   -75.2%
+ ~Mathlib.CategoryTheory.Generator                           instructions   -48.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure           instructions   -44.0%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits   instructions   -11.6%
+ ~Mathlib.GroupTheory.Coset                                  instructions   -79.1%
+ ~Mathlib.GroupTheory.GroupAction.Quotient                   instructions   -76.8%
+ ~Mathlib.GroupTheory.QuotientGroup                          instructions   -34.3%
+ ~Mathlib.LinearAlgebra.Isomorphisms                         instructions   -58.1%
+ ~Mathlib.LinearAlgebra.Quotient                             instructions   -28.7%
+ ~Mathlib.LinearAlgebra.QuotientPi                           instructions   -68.3%
+ ~Mathlib.LinearAlgebra.SModEq                               instructions   -89.4%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient                instructions   -54.9%
+ ~Mathlib.RingTheory.Smooth.Basic                            instructions   -42.6%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring              instructions   -22.5%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module                instructions   -60.3%
+ ~Mathlib.Topology.Instances.AddCircle                       instructions   -59.4%