let's not crank maxHeartbeats as low as possible

Stream: mathlib4

[Scott Morrison]

Sometime when setting maxHeartbeats, people are inclined to set it as low as possible. I think this is counterproductive --- when small changes earlier in the library tip the declaration back over the limit, it is annoying to the editor who is suddenly faced with an error far away in the library.

I recommend using the least number 2^k * 200000 which suffices.

You can use the command count_heartbeats in which will automatically suggest a number of this form.

(Just pinging @Jujian Zhang as the most recent example I encountered of this problem was from you. :-)

[Scott Morrison]

(e.g. set_option maxHeartbeats 1643256 in has no useful content. :-)

[Jireh Loreaux]

I disagree to some extent. Allowing up to a factor of 2 is an awful lot. I agree there should be some buffer so that changes throughout the library aren't guaranteed to trip them, but something like 10-20% higher than required seems reasonable. This should alert the user that maybe something they did broke something.

[Scott Morrison]

Is 1.2 okay? I'm very happy to merge a change to count_heartbeats!

[Jujian Zhang]

Ha, I used count_heartbeats to find the smallest number possible. Sorry about that, I will use 1.2 factors now.

[Scott Morrison]

This was why I made count_heartbeats print a suggestion. I knew that people would use it to write set_option maxHeartbeats 1643256 otherwise. :-)

[Mario Carneiro]

does it have a code action?

[Mario Carneiro]

In addition to being approximately 1.2 of the true value, I would suggest that it be rounded to 2 significant figures

[Mario Carneiro]

Mario Carneiro said:

does it have a code action?

It has a Try this code action but it apparently reformats the command. I think it should just replace count_heartbeats with set_option maxHeartbeats N instead of the whole command

[Marcus Rossel]

What actually is the benefit of keeping the heartbeats low?
My experience with them so far has always been that something hits the limit, so I increase it until it works. What is the downside of just setting it to 10000000000 immediately?

[Mario Carneiro]

you miss an opportunity for review if it later spikes a lot more

[Mario Carneiro]

that is, adding set_option maxHeartbeats is a code smell, and increasing the limit is also a code smell

[Marcus Rossel]

Mario Carneiro said:

you miss an opportunity for review if it later spikes a lot more

So it acts kind of like linter warning you of code that you should probably redo/refactor?

[Yury G. Kudryashov]

@Scott Morrison I have a timeout in #5610 but count_heartbeats tells me a number below the limit.

[Yury G. Kudryashov]

Does it count time spent in processing attributes?

[Yury G. Kudryashov]

I think that the @[simps!] makes it go over the limit.

[Scott Morrison]

Hmm, I thought count_heartbeats in would be counting everything that follows!

[Kyle Miller]

count_heartbeats in looks like it's counting everything that follows, and I've never seen anything that could reset the value of IO.getNumHeartbeats. This function reads the value of m_heartbeat in the heap data structure, and it's only ever incremented.

There's a chance that it could be unreliable if there's work being done on a separate thread. The m_heartbeat field counts how many small memory allocations (and also how many expression comparisons) are performed for a particular thread.

(There's also a separate heartbeat system that counts how many times the check_system() function is run, and it seems like it might only be settable by the timeout command line option.)

[Riccardo Brasca]

Do we have a version of count_heartbeats in but for synthInstance.maxHeartbeats?

[Riccardo Brasca]

BTW I've noticed a small bug (or at least an unpleasant behavior) in count_heartbeats: if the theorem has long lines that have been split in several lines manually, after clicking on the suggestion to replace count_heartbeats by set_option maxHeartbeats ... those lines are long again.

[Scott Morrison]

Yes, we need to work out how to have the "Try this:" span for count_heartbeats in not include the command. If you look at the current definition it does, but when I wrote it I couldn't see how to avoid this: I couldn't generate valid syntax terminating in in.

[Scott Morrison]

(But no, to your first question. I don't know where or if the counter for synthInstance.maxHeartbeats is exposed.)