Instance order sensitivity in `Topology/Sheaves/Stalks.lean`

Stream: mathlib4

[Anne Baanen]

I'm debugging a build failure on #18734 and it looks like this is caused by the import order changing the instance definition order. Namely, I can replicate the failure by inserting, just before, docs#TopCat.Presheaf.germToPullbackStalk a line that changes the priority:

attribute [instance 100] OmegaCompletePartialOrder.toPartialOrder

And conversely, if I do the opposite change in #18734 and either give this instance a higher than default priority or give OrderedAddCommMonoid.toPartialOrder a lower priority, the build also succeeds.

The weird thing is, we are not close at all to the maxHeartbeats in the current situation (somewhere between 7500 and 8000 where the default limit is 20000). So presumably there is some bad path involving OrderedAddCommMonoid that takes too long to fail.

Anyone have any suggestions on how to deal with this?

[Anne Baanen]

One option would be either to raise the OmegaCompletePartialOrder.toPartialOrder priority or to lower the OrderedAddCommMonoid.toPartialOrder priority globally, but that seems a very heavy hammer to hit this issue with.

[Anne Baanen]

(I am currently tracing out the OrderedAddCommMonoid synth log, but seeing nothing that particularly jumps out. It simply seems to try a few instances that have cached failures, and then continues with the OmegaCompletePartialOrder branch.)

[Anne Baanen]

I can't find any useful way to do this change globally, and it would likely interfere with the uncoupling/priority lowering proposed in the Ways to speed up Mathlib topic. So I will keep it at a local change. A bit hacky but eh.

[Anne Baanen]

(Another slightly evil alternative is trying to avoid importing OrderedMonoid in that file entirely :P)

[Matthew Ballard]

It is fairly easy to disconnect from OrderedAddCommMonoid. You need to move the results specific to CommRingCat elsewhere.

[Anne Baanen]

In fact, that's what I ended up doing after all :D

[Anne Baanen]

PR coming up in a few minutes...

[Matthew Ballard]

That's the most principled approach in my mind

[Anne Baanen]

This import graph is just too tempting... from-Mathlib.Algebra.Order.Monoid.Defs-to-Mathlib.Topology.Sheaves.Stalks.pdf

[Anne Baanen]

#18762