what are heartbeats? I'm getting a series of errors

Stream: new members

[Jonathan Protzenko]

Most of my errors are along the lines of

(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

(also at 'isDefEq')

I can try to provide a repro if helpful, but I'm curious to know what the heartbeats are, and if there's a classic cause for those

[Kevin Buzzard]

There could be all manner of reasons for this. Why not post a #mwe ? Maybe something's in a loop, maybe something's taking a long time.

[Kevin Buzzard]

heartbeats are lean doing stuff

[Martin Dvořák]

I think the question is about the concept of deterministic timeouts. I was puzzled by these for a very long time!

[Martin Dvořák]

That said, I have no idea what heartbeats are. Maybe it is something specific to Lean 4.

[Tomas Skrivan]

A heartbeat is a step of some algorithm, like simplifier, type class resolution or checking def equality (isDefEq). In certain cases these do not have to terminate or they can take too long, so there is a cap on how many steps(heartbeats) the algorithm can take.

The timeout error indicates that this maximum cap has been reached.

[Tomas Skrivan]

The way to deal with it is to turn on tracing(place these lines anywhere in the file before the error):

set_option trace.Meta.whnf true
set_option trace.Meta.isDefEq true
set_option trace.Meta.synthInstance true

(usually you turn on only one of these)
Inspect what is going on and fix it.

A quick fix can be to increase the maximum number of heartbeats:

set_option maxHeartbeats 1000000
set_option synthInstance.maxHeartbeats 100000

but that is usually bad idea as it can take a long time.

Actually I usually decrease the number of heartbeats to have shorter traces, then they are easier to read and navigate.

[Tomas Skrivan]

A simple example with type class timeout

class C (n : Nat)
instance [C (n+1)] : C n := ⟨⟩

set_option trace.Meta.synthInstance true in
set_option synthInstance.maxHeartbeats 100 in
example : C 0 := by infer_instance

[Chris Bailey]

Jonathan Protzenko said:

I'm curious to know what the heartbeats are, and if there's a classic cause for those

Trying to unfold a well-founded definition using simp is one of them (you can use rw [<def>] instead).

[Reid Barton]

Literally anything can cause this. A side effect you might have noticed is that Lean is slow

[Floris van Doorn]

if you're using mathlib4, then updating to the latest version (<4 hours old) might give you a significant increase in efficiency (~30%), which might help in your case.

[Jonathan Protzenko]

thanks all, it's not easy to minimize, but I think I'm basically trying to reduce a term that's too big

[Jonathan Protzenko]

so things are probably not reducing the way I think they ought to

[Jonathan Protzenko]

I'll try to debug using your advice... thanks

[David⚛️]

Please my lean 4 just stopped working. Any solution?

[Alex J. Best]

Can you identify which lines of code are causing the timeout?