mathlib4

mathlib4 copied to clipboard

---

!bench

Here are the benchmark results for commit 336a2f71e167150b8e59a9c0813d4d99bc8d1158. There were significant changes against commit 9f012931d33003deda3b46137791fbfa457adb3e:

  Benchmark                                              Metric         Change
  ============================================================================
+ ~Mathlib.AlgebraicGeometry.Gluing                      instructions   -25.5%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated    instructions    -7.3%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing   instructions    -3.4%

I just labelled this PR with a best guess as to its current state. Feel free to adjust if you know better!

I removed the comments in Topology/Sheaves/* as the file is designed to have this instance on.

Can you add a description to summarize the changes, perhaps linking the Zulip thread(s)?

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style

Late to the party, but here are more detailed results from the comparison above:

General information:
  lint:                                                -260.80 * 10⁹ (-2.16%)
  build:                                               -161.69 * 10⁹ (-0.139%)

No file got slower by at least 10⁹ instructions.

No file got slower by at least 10%.

Files that got faster by at least 10⁹ instructions:
  Mathlib.AlgebraicGeometry.Gluing:                    -24.491 * 10⁹ (-25.5%)
  Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing:
                                                       -13.181 * 10⁹ (-3.40%)
  Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated:  -10.915 * 10⁹ (-7.32%)
  Mathlib.AlgebraicGeometry.Restrict:                  -8.9381 * 10⁹ (-3.99%)
  Mathlib.Geometry.RingedSpace.PresheafedSpace:        -8.5588 * 10⁹ (-8.30%)
  Mathlib.Geometry.RingedSpace.OpenImmersion:          -8.5006 * 10⁹ (-4.41%)
  Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties:
                                                       -8.1320 * 10⁹ (-2.52%)
  Mathlib.Topology.Category.TopCat.Limits.Products:    -7.5619 * 10⁹ (-16.8%)
  Mathlib.Topology.Sheaves.Stalks:                     -7.5011 * 10⁹ (-5.55%)
  Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits:
                                                       -6.7390 * 10⁹ (-4.83%)
  Mathlib.Topology.Category.TopCat.Limits.Pullbacks:   -5.4874 * 10⁹ (-12.0%)
  Mathlib.AlgebraicGeometry.OpenImmersion:             -5.3314 * 10⁹ (-7.88%)
  Mathlib.Geometry.RingedSpace.Stalks:                 -4.6689 * 10⁹ (-9.69%)
  Mathlib.AlgebraicGeometry.Properties:                -4.2538 * 10⁹ (-7.51%)
  Mathlib.Topology.Gluing:                             -4.0383 * 10⁹ (-6.38%)
  Mathlib.AlgebraicGeometry.AffineScheme:              -3.3577 * 10⁹ (-1.43%)
  Mathlib.Topology.Category.TopCat.OpenNhds:           -3.2756 * 10⁹ (-14.0%)
  Mathlib.Topology.Sheaves.Presheaf:                   -3.0251 * 10⁹ (-2.82%)
  Mathlib.AlgebraicGeometry.Spec:                      -2.8423 * 10⁹ (-2.52%)
  Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact:    -2.5017 * 10⁹ (-5.89%)
  Mathlib.Topology.Category.TopCat.Opens:              -2.3966 * 10⁹ (-4.73%)
  Mathlib.AlgebraicGeometry.FunctionField:             -1.5437 * 10⁹ (-5.05%)
  Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm:
                                                       -1.4668 * 10⁹ (-0.532%)
  Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits:
                                                       -1.0794 * 10⁹ (-3.07%)
  Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit:
                                                       -1.0399 * 10⁹ (-2.65%)

Files that got faster by at leat 10%:
  Mathlib.AlgebraicGeometry.Gluing:                                   -25.5%
  Mathlib.Topology.Category.TopCat.Limits.Products:                   -16.8%
  Mathlib.Topology.Category.TopCat.OpenNhds:                          -14.0%
  Mathlib.Topology.Category.TopCat.Limits.Pullbacks:                  -12.0%