RingCon algebraic TC instances

Stream: mathlib4

[Matthew Ballard]

Sanity check: docs#RingCon.instNonUnitalNonAssocSemiringQuotientToAddToDistribToMul and its friends in that section are problematic for Lean 4 structures but great for flat structures, right?

[Eric Wieser]

Those should be fine for Lean4 structures as long as Function.Surjective.nonUnitalNonAssocSemiring and friends are implemented without with

[Matthew Ballard]

Some are and some aren't. #6854 tried to remove the with's and things slowed down

[Matthew Ballard]

In particular, AG and RingTheory.Kaehler both suffered in a familiar way to #7257

[Matthew Ballard]

:test_tube:

[Matthew Ballard]

@Chris Hughes pointed out to Kevin who pointed out to me #6874 which builds in more direct inheritance to some of these instances. It does help.

I am guessing it will complement lean4#2478 but won’t have a chance to merge and test for a bit.

[Chris Hughes]

See also #7401 which also speeds up RingTheory.Kaehler.

[Matthew Ballard]

Basically the sum of the improvement and the regression for Kaehler Bench

[Matthew Ballard]

There is a bit noise since the baseline PR is a bit old.

[Matthew Ballard]

I delegated #6874 since it seems orthogonal to (in terms of effect) lean4#2478.

I am believing more the theory that Function.Injective/Surjective is repeatedly exposing (mildly) slow defeqs.

[Matthew Ballard]

Combining #6874 with a refactor to build in direct inheritance for RingCon algebraic classes goes well

[Matthew Ballard]

Next to see how it interacts with lean4#2478

[Matthew Ballard]

It made the regression in RingTheory.Kaehler less bad

[Matthew Ballard]

+5% vs +30% before

[Matthew Ballard]

LinearAlgebra.FreeModule.Norm/PID both turned green

RingTheory.AdjoinRoot got worse.

The rest stayed the same

[Kevin Buzzard]

I'll say again -- I think another measure of success would be not percentage change but absolute change in instructions. Stuff like "RingTheory.Kaehler got 9.5% quicker" is an incredible success because that file takes forever to compile. Let's say some other file got 300% slower. This looks like a huge net loss, but then if you find out that the other file is only 40 lines long and compiles instantly then all of a sudden you're back looking at a big win.

To try and explain why this is important, here's a screenshot of the times changing in RingTheory files:

Screenshot-from-2023-09-29-08-44-25.png

RingTheory.Kaehler is now faster by 72 billion time units and RingTheory.Jacobson by 84 billion. These numbers just seem to dwarf eveything else. Most files don't even take 84 billion time units to compile. The percentage changes being reported by the speedcenter do not highlight this phenomenon. Oh -- can this be read off from "build instructions"?

[Sebastian Ullrich]

Yes, "build instructions" should be (roughly?) the sum of all module metrics

[Matthew Ballard]

Yes. I think the first question when evaluating a PR is the percentage change in total build instructions. If this is positive, other things can be forgiven. For example, build time currently is controlled by the path to AlgebraicGeometry.Morphisms.RingHomProperties so even if you zeroed out the build times for 8 of 10 most CPU intense files including RepresentationTheory.GroupCohomology.Basic/Resolution, Analysis.NormedSpace.OperatorNorm/Multilinear, CategoryTheory.Abelian.Projective/InjectiveResolution etc you would not affect the build time. You would drop total instructions by almost 10% however

[Matthew Ballard]

Here are other files following the (anti-?)pattern

Mathlib/FieldTheory/Subfield.lean
Mathlib/GroupTheory/Subgroup/Basic.lean
Mathlib/GroupTheory/Submonoid/Operations.lean
Mathlib/GroupTheory/Subsemigroup/Operations.lean
Mathlib/RingTheory/NonUnitalSubring/Basic.lean
Mathlib/RingTheory/Subring/Basic.lean
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
Mathlib/RingTheory/Subsemiring/Basic.lean
Mathlib/LinearAlgebra/Alternating.lean
Mathlib/LinearAlgebra/Quotient.lean
Mathlib/Data/Finsupp/Defs.lean
Mathlib/Algebra/Order/Nonneg/Ring.lean
Mathlib/Topology/LocallyConstant/Algebra.lean
Mathlib/Algebra/Module/Submodule/Basic.lean
Mathlib/Topology/Sets/Compacts.lean
Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean
Mathlib/Topology/Algebra/Module/Alternating.lean
Mathlib/Topology/Algebra/Module/Multilinear.lean
Mathlib/Algebra/Group/Opposite.lean
Mathlib/Algebra/Group/ULift.lean

[Matthew Ballard]

In each of these, there are multiple uses of Function.Injective/Surjective.x in parallel when building type classes. Eg

instance : Monoid X := Function.Injective/Surjective.monoid ...
instance : Semigroup X := Function.Injective/Surjective.semigroup ...
instance : Group X := Function.Injective/Surjective.group ...
...

Lean has to unify all the arguments into Function.Injective/Surjective.xwhich seems to come at a higher cost that a more direct to parent construction pattern

[Eric Wieser]

Does inline help at all here?

[Matthew Ballard]

Checking my understanding: inline the Function.InjSurj.x’s?

[Eric Wieser]

I mean that we maybe want them inclined into the call site, and that with an even stronger "maybe" the @[inline] attribute helps somehow

[Sebastian Ullrich]

I think another measure of success would be not percentage change but absolute change in instructions

While I don't think we have any volunteers for making this change in the Java/TypeScript speedcenter code, a far simpler change that indeed we only have to touch code in mathlib4 for just came to mind: we could stop tracking any "small" files below a certain instruction threshold at all. Do you think this would be helpful?

[Joscha Mennicken]

This might hide a jump where a small file suddenly increases by a lot from significance checks, I think

[Sebastian Ullrich]

Yes, that "new benchmark" is not a significant event is problematic for this

[Sebastian Ullrich]

Note that for two adjacent commits we can at least sort the table by absolute change. So one workaround is to always make sure that the base commit for the comparison is the parent commit and then use the commit view instead of comparison view

[Kevin Buzzard]

When I'm making a PR which I want to bench I'm always very careful about making sure I'm branching off a commit on master which is already benched.

[Matthew Ballard]

Eric Wieser said:

I mean that we maybe want them inclined into the call site, and that with an even stronger "maybe" the @[inline] attribute helps somehow

From the profiler, there doesn't seem to be much time spent getting in to the Function.Inj/Surj.x's but it is easy enough to check

[Matthew Ballard]

Bench @Eric Wieser let me know if I am doing it wrong. I think I understand the principle behind it but perhaps @[inline] doesn’t behave as I want

[Eric Wieser]

I'm probably telling you to do it wrong

[Matthew Ballard]

We have movement in AG

[Matthew Ballard]

Dumping all the changes in together give much more movement in AG.

[Matthew Ballard]

It’s not reported as headline but ring gets 2x faster

[Matthew Ballard]

Sadly RingHomProperties doesn’t change much so sees its lead in CPU instructions grow to about 3x the second place file