perf: try reverting #21330

[grunweg]

By now, mathlib is on a Lean version including leanprover/lean4#7428 (for which #21330 was a workaround).
Let's measure the performance implications of reverting that change.

---

[github-actions]

PR summary 8277e451a7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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).

[JovanGerb]

My suspicion is that the rfl_cat trick is still beneficial for performance, but that the impact will be less pronounced. Let's see!

[grunweg]

I'm not sure how to fix the last sorry (and cannot benchmark without that, it seems). Do you have an idea?

[JovanGerb]

The problem was that in kerAdjunction, the aesop tactic was for some reason using the variable U. This is really sneaky and evil, because as a result, the type of kerAdjunction has changed to include the argument U.

[grunweg]

The problem was that in kerAdjunction, the aesop tactic was for some reason using the variable U. This is really sneaky and evil, because as a result, the type of kerAdjunction has changed to include the argument U.

Oh wow. Thanks for catching and fixing this! (And I wonder if this issue also occurs in other places in mathlib... though I am not sure how to test for this.)

[ghost]

!bench

[JovanGerb]

This can only happen in definitions, since theorems determine their type before elaborating the proof. And hopefully definitions get used, so that this kind of change gets caught immediately. But maybe with instances it can be less obvious when this problem arises.

[grunweg]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8277e45.
There were significant changes against commit c7f51d8:

  Benchmark                                                        Metric         Change
  ======================================================================================
- build                                                            aesop           20.3%
- ~Mathlib.Algebra.Category.Grp.LeftExactFunctor                   instructions    54.2%
- ~Mathlib.Algebra.Category.ModuleCat.Topology.Basic               instructions     7.9%
- ~Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion             instructions    45.6%
- ~Mathlib.AlgebraicTopology.SimplicialNerve                       instructions    42.1%
- ~Mathlib.AlgebraicTopology.SimplicialObject.Basic                instructions    11.2%
- ~Mathlib.CategoryTheory.Comma.StructuredArrow.Basic              instructions     7.2%
- ~Mathlib.CategoryTheory.Monoidal.Internal.Module                 instructions    27.7%
- ~Mathlib.CategoryTheory.Skeletal                                 instructions    77.0%
- ~Mathlib.Condensed.Discrete.LocallyConstant                      instructions    68.3%
- ~Mathlib.Order.Category.BoolAlg                                  instructions    48.7%
- ~Mathlib.Order.Category.FinBoolAlg                               instructions    60.1%
- ~Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections   instructions    16.1%

[grunweg]

It seems this optimisation is still useful: thus, let's keep this (but only update the comment). #25482 does so.

[grunweg]

The performance changes does appear small than in #21330 which introduced it: but it's still significant enough, in my opinion.

[JovanGerb]

By the way, does the speedcenter website work for you? when I click the significant changes link, it doesn't manage to load the data.

[grunweg]

I get the same error.

[grunweg]

Now the comparison page loads fine: mathlib slows down by 600*10⁹ instructions (~0.44%) --- which is about a third of the original magnitude of #21330. In other words: it's great to confirm that this change is less required, but it's still worth keeping.