set_option maxHeartbeats with no "in"

Stream: general

[Kevin Buzzard]

Am I right in thinking that this line set_option maxHeartbeats 800000 (perhaps inadvertently) sets the max heartbeats to 800000 for the rest of the entire file, because of the lack of in? This is not the first time I have seen this happen either. I'm currently trying to fix raised maxHeartbeats issues and this is an extra piece of noise which I've only just realised is happening.

If I'm right, am I also right in thinking that someone who knows a bit about shell scripting or something could search mathlib for all the times that this is occurring and then fix them (if this is indeed something we think is worth fixing?)

[Damiano Testa]

I am not sure about the Lean question, but this is where these heartbeats appear unleashed:

regex: "maxHeartbeats [0-9]*$"
Mathlib/CategoryTheory/Monoidal/Braided.lean:479:set_option maxHeartbeats 400000
Mathlib/FieldTheory/Adjoin.lean:1212:set_option synthInstance.maxHeartbeats 30000
Mathlib/FieldTheory/IsAlgClosed/Basic.lean:302:set_option maxHeartbeats 800000
Mathlib/FieldTheory/IsAlgClosed/Basic.lean:303:set_option synthInstance.maxHeartbeats 400000
Mathlib/RepresentationTheory/GroupCohomology/Basic.lean:202:set_option maxHeartbeats 6400000
Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean:345:set_option maxHeartbeats 800000
Mathlib/Topology/MetricSpace/GromovHausdorff.lean:415:set_option maxHeartbeats 300000

[Kevin Buzzard]

Thank you Damiano!

[Damiano Testa]

#6206

[Damiano Testa]

Let's see what happens!

[Kevin Buzzard]

Thank you even more!

[Kevin Buzzard]

Damiano Testa said:

Let's see what happens!

Yes -- the build might fail because declarations below the targetted ones might also need raised heartbeats (if my understanding of all this is correct).

[Damiano Testa]

I would agree with your interpretation.

[Damiano Testa]

Indeed, here is the first timeout:

Error: ./././Mathlib/CategoryTheory/Monoidal/Braided.lean:662:14: error: (deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

[Riccardo Brasca]

There are indeed errors, but we surely want in everywhere.

[Damiano Testa]

I was going to add the heartbeats, but I must have broken something about my lean configuration. I'm fixing it now, but if someone else wants to add the first missing heartbeat, feel free to do so!

[Damiano Testa]

Ok, my issue was that I ran out of memory. Braided only required raising more heartbeat limit, at least on my computer.

[Kevin Buzzard]

You can use count_heartbeats in to find the official number which is supposed to be there! It should be a power of two multiplied by the default amount (this convention helps a lot when doing the kind of debugging that I'm doing)

[Damiano Testa]

I did that for the first timeout, I am now checking the remaining files: the only files that my computer did not check yet are RepThy.GpCoho.{ Basic + Resol }.

[Damiano Testa]

The PR has no timeouts on my computer! The conclusion seems to be that the missing ins only shielded docs#CategoryTheory.associator_monoidal either consciously or not!

[Damiano Testa]

And the PR is now building the library_search cache (that maybe should be renamed to exact? also for CI?)!

[Damiano Testa]

The PR got merged: all the declarations that need to raise the maxHeartbeats should be doing this encased in their own set_option [synthInstance.]maxHeartbeats xxx in section.

[Damiano Testa]

I wonder if it would be better/possible/desirable to have

• set_option [synthInstance.]maxHeartbeats xxx mean the same as set_option [synthInstance.]maxHeartbeats xxx in and
• set_option [synthInstance.]maxHeartbeats xxx all mean the current interpretation without the in.

[Eric Wieser]

I think we should have this instead:

Eric Wieser said:

Should we have a bump_heartbeats N in foo command that means something like "count_heartbeats, but error if the result differs from N by more than 20%"?

[Eric Wieser]

Then we just ban set_option entirely

[Damiano Testa]

Ah, I had forgotten about your suggestion! I like yours better than mine!

[Siddhartha Gadgil]

While my use case is not common, I do set very large heartbeats for files because I am running programs non-interactively. There are likely to be other such uses (for example running in the background in a Task even when working interactively).

I feel limiting capabilities is not a good thing - one can switch penalties by requiring set_option maxHeartbeats xxx henceforth with in being the default option.

[Siddhartha Gadgil]

Of course one can have a linter in mathib to enforce whatever is the consensus of the mathlib community.

[Eric Rodriguez]

I think the idea would be to ban it in mathlib, not globally, and only in the final PR'd code