Zulip Chat Archive

Stream: lean4

Topic: Heartbeats


view this post on Zulip François G. Dorais (Jan 30 2021 at 22:58):

For the past few nightlies, I've been hitting the maxHeartbeat limits in some of my code ported from Lean 3. I've been using set_option synthInstance.maxHeartbeats 0 and set_option maxHeartbeats 0 to disable these limits. After all, I'm current focused on making things work, I'm not yet working on making them efficient. However, I would perhaps prefer setting a reasonably lax limit to detect highly inefficient code early.

What's a heartbeat? What does it measure? When and how does the count reset?

view this post on Zulip Mario Carneiro (Jan 30 2021 at 23:15):

Lean 3 also has heartbeats, they are the unit of "time" in set_option timeout and the associated (deterministic) timeout error you sometimes see

view this post on Zulip Mario Carneiro (Jan 30 2021 at 23:16):

it's an abstraction of the timeout to measure something a bit more... deterministic; I believe it's something like the number of allocations to create new exprs and other objects

view this post on Zulip Leonardo de Moura (Jan 30 2021 at 23:26):

It is similar for Lean 4: it is the number of small object allocations in thousands.

view this post on Zulip François G. Dorais (Jan 30 2021 at 23:35):

Thanks for the quick responses!

I still wonder when and how does the count reset? Perhaps a better question is what is actually measured against the limit? For example, would breaking up a long proof in lemmas help avoiding the maxHeartbeat limit?

view this post on Zulip Leonardo de Moura (Jan 30 2021 at 23:39):

Yes, it will help. The counter is reset before each command.

view this post on Zulip François G. Dorais (Jan 30 2021 at 23:50):

Great. By "command" do you mean the command syntax category or something more general?

view this post on Zulip Leonardo de Moura (Jan 30 2021 at 23:53):

Yes, commands such as def, inductive, theorem, #check, etc.


Last updated: May 18 2021 at 23:14 UTC