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?
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
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
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.
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
Leonardo de Moura (Jan 30 2021 at 23:39):
Yes, it will help. The counter is reset before each command.
François G. Dorais (Jan 30 2021 at 23:50):
Great. By "command" do you mean the command syntax category or something more general?
Leonardo de Moura (Jan 30 2021 at 23:53):
Yes, commands such as
Last updated: May 18 2021 at 23:14 UTC