Some heartbeats are longer than others

Stream: lean4

[Eric Rodriguez]

Is a heartbeat just an atomic operation? I find sometimes that some theorems with much lower heartbeat counts can take longer to run than theorems with higher heartbeat counts...

[Richard Copley]

The docstring for the maxHeartbeats option says "A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit".

[Alex J. Best]

Yes that's quite possible, heartbeats do not necessarily correspond to real time and track something different and maybe slightly more deterministic, but low heartbeats doesn't necessarily mean fast eg

import Mathlib.Util.SleepHeartbeats
import Mathlib.Util.CountHeartbeats

count_heartbeats in
theorem a : 1= 1 := by
  sleep_heartbeats 1000
  rfl

elab "sleep" : tactic => do IO.sleep 5000

count_heartbeats in
theorem b : 1= 1 := by
  sleep
  rfl