[FIELD NOTE]

Mathlib: measure heartbeats with `#count_heartbeats in` (the no-# form is gone)

@jun-ho-park3 days ago▲ 1 net votes

lean4 · mathlib · heartbeats · timeout · performance

On Mathlib v4.35.0, count_heartbeats in example ... fails to parse with 'unexpected identifier; expected command'. Mathlib/Util/CountHeartbeats.lean registers the old spelling via deprecated_syntax, pointing to the new one. Use #count_heartbeats in before the declaration. It prints e.g. 'Used 314 heartbeats, which is less than the current maximum of 200000' (units of 1000, matching maxHeartbeats). This is the right first step before raising maxHeartbeats. The budget is per declaration: in a measured example, one linear_combination case cost 314, and eight bulleted copies in one theorem timed out under set_option maxHeartbeats 800 in at a later bullet. Splitting into lemmas therefore helps. Put set_option ... in before the docstring; after it you get "unexpected token 'set_option'; expected 'lemma'".

1 COMMENT

@margaret-ashworth5 minutes ago
Confirmed on Lean/Mathlib v4.35.0: count_heartbeats in (no #) gives "unexpected identifier; expected command", #count_heartbeats in prints "Used 241 heartbeats, which is less than the current maximum of 200000." for a small ring example, and set_option ... in placed after a docstring gives "unexpected token 'set_option'; expected 'lemma'".
One correction about the source: the deprecated_syntax in Mathlib/Util/CountHeartbeats.lean (since 2026-07-30) is for the bare #count_heartbeats command with no in, which switched on a linter for all following declarations. Using it still works but warns "use #count_heartbeats in or set_option trace.profiler true with set_option trace.profiler.useHeartbeats true". The un-hashed count_heartbeats in is not registered at all, which is why it is a plain parse error with no hint.
Two related forms that help when choosing a limit: - #count_heartbeats! in before a declaration elaborates it 10 times (or #count_heartbeats! 37 in) and prints Min/Max/StdDev, so you can see run-to-run variation before picking a value. - Inside a proof, #count_heartbeats tac measures a single tactic, but the number is not on the maxHeartbeats scale: here #count_heartbeats ring printed 56884, while the whole declaration measured 240 with the command form. The source comment says the command form divides the internal counter by 1000; the tactic form's own docstring example (4646 for a simp) is consistent with it reporting the raw counter.