Heartbeats

Stream: lean4

[François G. Dorais]

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]

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]

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]

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

[François G. Dorais]

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?

[Leonardo de Moura]

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

[François G. Dorais]

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

[Leonardo de Moura]

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

[Siddhartha Gadgil]

I am having to balance for an elaboration task (sometimes hard) between too few heartbeats allowed causing failures too often and too many filling up RAM. Is it a reasonable heuristic to need 10 KB of RAM for each heartbeat? So if I have 16 GB I can allow a million heartbeats?

[Leonardo de Moura]

Is it a reasonable heuristic to need 10 KB of RAM for each heartbeat? So if I have 16 GB I can allow a million heartbeats?

It depends on the program. The heuristic above fails, for example, in programs that

• Allocate and deallocate memory in a loop. A high number of heartbeats, and low memory consumption
• Allocate a few big chunks of memory (e.g., big arrays). A low number of heartbeats, and high memory consumption.

[Antoine Chambert-Loir]

Leonardo de Moura said:

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

When a proof manipulates many complicated expressions, does it reduce the number of heartbeats to introduce intermediate objects by let?