Timeouts with #9606

Stream: general

[Ruben Van de Velde]

Adding a gcd_monoid instance for euclidean_domain causes a lot of slowdowns and timeouts all over the place. I'd be grateful if someone with more experience debugging these kind of issues took a look at #9606

[Anne Baanen]

I suspect that we're right at the limit of the typeclass system, since many of my changes seem to cause timeouts...

[Anne Baanen]

Especially after the addition of non_unital_non_assoc_etc_rings, instance-related timeouts seem to happen to me frequently.

[Eric Wieser]

Yeah, that will definitely have made lots of things worse

[Junyan Xu]

I started getting timeouts in VSCode shortly after adding an is_localization instance for the map from a ring to the sections of its structure sheaf on a basic open (and stalk at a point). Probably not a coincidence!

[Patrick Stevens]

The timeout in 9606 most recently:
Error: /home/lean/actions-runner/_work/mathlib/mathlib/src/algebraic_topology/cech_nerve.lean:242:27:
(deterministic) timeout

#9925 gave me a different timeout:
Error: /home/ghrunner/actions-runner/_work/mathlib/mathlib/src/algebraic_geometry/presheafed_space/has_colimits.lean:230:4:
(deterministic) timeout