RingHomProperties

Stream: mathlib4

[Scott Morrison]

Is anyone working on AlgebraicGeometry.Morphisms.RingHomProperties? It has some insane maxHeartbeats, and it conspicuously delays the end of the build for me.

Could we even consider moving it back out to a PR until someone works out what is going on?

[Johan Commelin]

cc @Kevin Buzzard @Matthew Ballard since they've been looking hard at these speed problems in the past weeks.

[Scott Morrison]

Thanks, yes. From what I've been reading of their work I think no one has been directly looking at this file?

[Kevin Buzzard]

I'm away this week but don't have any speedups up my sleeve. The group cohomology files also have too many raised heartbeats

[Matthew Ballard]

I’m familiar with the file after helping to port it. I started looking at why AG was so unhappy with #6539. In general, many rw became erw’s during the port.

[Matthew Ballard]

The changes to structure instance elaboration result in a more tightly packed term. Which is great when there is no further unfolding necessary during unification.

[Matthew Ballard]

But it appears that AG as is needs to unfold and to rather large terms.

[Matthew Ballard]

Why it needs to unfold? Especially more so than other areas. I’m not sure. From a preliminary look at traces I’ve found some structure eta expansions not eliminated by the changes to the tool chain in #6359.

[Matthew Ballard]

But how much this contributes, I don’t know

[Matthew Ballard]

It’s worth noting that ModuleCat and RepresentationTheory both improved overall with #6539

[Matthew Ballard]

Everytime I build mathlib and get to the point of waiting on RingHomProperties I think of a seabird choking down a giant rock for digestion.

[Jireh Loreaux]

Pro tip: don't edit files imported by RingHomProperties :laughing: (obviously joking)

[Matthew Ballard]

Is it feasible to split this file for shorter build times? At least until we get a handle on its issues

[Johan Commelin]

Sure, I guess a split in 2 is certainly fine.

[Johan Commelin]

But it would be a bit sad to have a 1-lemma-per-file strategy...

[Ruben Van de Velde]

Would that help overall build times? Is there a lot of code that depends only on part of the file? Or would the sum of the compilation times be less than the compilation time of the sum?

[Eric Wieser]

Having separate files makes it a lot easier to edit something at the end of the file

[Matthew Ballard]

That file takes ~15 minutes to build in CI. Usually ~10 minutes of which is it building alone

[Matthew Ballard]

I’m not sure how much can be done parallel though

[Eric Wieser]

I think it's worth splitting just for the editing experience in vscode

[Eric Wieser]

If I have to wait 10 minutes to add a result to the bottom of the file, I am going to be much more sad than having 2 or 3 files to pick between

[Matthew Ballard]

Our long national nightmare is over. Thanks @Andrew Yang!

[Mauricio Collares]

16.4% overall build wall-clock reduction and there's still a set_option maxHeartbeats 4000000 in line in the same file! That's amazing.

EDIT: Now I see the build wall-clock metric is quite unstable, probably due to the fact that it depends on build scheduling. Nevertheless, -3.5 trillion instructions is a lot!

[Matthew Ballard]

Merge master now and get an extra 10-15 minutes of your life back

[Matthew Ballard]

I am 99% sure that wall clock is accurate

[Matthew Ballard]

It can bounce 2-3% or a lot more if there are some transient effects. We spend about 10 extra minutes just building this file alone so "smaller" changes (eg 3% total CPU instructions) can have huge effects

[Matthew Ballard]

The linter was spending a monstrous amount of time (edit: and instructions!) linting that file

[Mauricio Collares]

Matthew Ballard said:

I am 99% sure that wall clock is accurate

I agree. I think the run prior to the one I linked was just really unlucky with scheduling (wall clock can be a lot longer than longest path if you're unlucky with scheduling), which wasn't the case with the base commit here.

[Matthew Ballard]

So probably more like 20 minutes of your life back :lol:

[Matthew Ballard]

Run number two

[Matthew Ballard]

Looks like -6 minutes in Ryzen time

[Matthew Ballard]

Wow. An AG file is no longer the last one to finish.

[Eric Wieser]

Can you link to the PR?

[Mauricio Collares]

#7749