Zulip Chat Archive

Stream: mathlib4

Topic: Random AG failure

Patrick Massot (Oct 05 2023 at 02:12):

I rebased my widget PR on master and now CI fails in some totally unrelated algebraic geometry files:

Error: ./././Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean:513:23: error: (deterministic) timeout at 'isDefEq', maximum number of heartbeats (700000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
Error: ./././Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean:513:25: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (700000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
Error: ./././Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean:513:25: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (700000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

Patrick Massot (Oct 05 2023 at 02:13):

https://github.com/leanprover-community/mathlib4/actions/runs/6413179694/job/17411697711?pr=7260

Patrick Massot (Oct 05 2023 at 02:14):

less than 20 files away from a successful build of mathlib :cry:

Patrick Massot (Oct 05 2023 at 02:15):

Does any AG speed experts such as @Matthew Ballard want to tell to simply bump the maxHeartbeats limit?

Matthew Ballard (Oct 05 2023 at 02:18):

I don't think that there any AG speed experts currently.

Matthew Ballard (Oct 05 2023 at 02:19):

You will not mar any beautiful edifice with a bump

Patrick Massot (Oct 05 2023 at 02:29):

Ok, I did it.

Patrick Massot (Oct 05 2023 at 02:29):

I pushed the 700000 to 1000000

Patrick Massot (Oct 05 2023 at 02:30):

I hope I will never have to open that file again.

Matthew Ballard (Oct 05 2023 at 02:32):

Until you do mirror symmetry at least

Patrick Massot (Oct 05 2023 at 02:33):

I feel safe for a couple of years...

Matthew Ballard (Oct 05 2023 at 02:34):

Hopefully it will be in better shape by then

Kevin Buzzard (Oct 05 2023 at 06:36):

Maybe this file is the new RingTheory.Kaehler

Kevin Buzzard (Oct 05 2023 at 07:45):

Rather than bumping up the numbers randomly it might be nice to stick to the power of two rule: every bump should be 2^n*default for some natural n

Kevin Buzzard (Oct 05 2023 at 07:47):

That way someone won't come along later and discover that they can change 1000000 to 800000 and incorrectly deduce that their unrelated change had an effect here

Scott Morrison (Oct 05 2023 at 07:49):

This had been my original suggestion with count_heartbeats ...

Antoine Chambert-Loir (Oct 05 2023 at 08:58):

what in the system does check count_heartbeats? could it be possible to define logcount_heartbeats as a natural number so that count_heartbeats is de facto 2 ^ logcount_heartbeats * default?

Kevin Buzzard (Oct 05 2023 at 09:06):

The system already reports the relevant power of 2 :-)

Scott Morrison (Oct 05 2023 at 09:08):

But people ignore the suggestion and want to write a smaller number. (Specifically to annoy Patrick? Hopefully not. :-)

Matthew Ballard (Oct 05 2023 at 13:01):

It seems you more than made up for the bump :laughing:

Last updated: Dec 20 2023 at 11:08 UTC