feat: always record per-declaration heartbeat costs

[dennj]

This PR makes the compiler always record how many heartbeats each declaration costs and report it: compiling a module writes a .hb.json file next to the .olean (the way .ilean files are always produced), and the language server attaches the count to each 'goals accomplished' diagnostic for clients that opt in via a new heartbeatSupport client capability, so editors can display the cost of every proof as it is written.

Lean already maintains the heartbeat counter unconditionally. Every small allocation increments it to enforce maxHeartbeats. Elaboration even measures each declaration's usage in withRestoreOrSaveFull for incremental reuse, but the number is thrown away. The only way to recover it today is trace.profiler with trace.profiler.useHeartbeats, which costs 1.3×–5× compile time because it must retain and pretty-print the entire trace tree (work proportional to trace nodes, with per-declaration attribution requiring trace.profiler.output.pp and parsing declaration names back out of human-readable messages).

This PR instead reads the already-maintained counter at declaration boundaries only, so the work is proportional to declarations: two counter reads and one array push per declaration and phase (elab, kernel), pushed into one per-file sink and serialized once per module. On the elaboration side it reuses the measurement withRestoreOrSaveFull already makes, adding no counter reads at all. Auxiliary declarations (matchers, equation lemmas, generated code, deriving-generated instances) roll up to the user-written declaration that caused them, tracked by a CostOwner state machine threaded through the command and declaration elaborators.

Measured on a 615-module Mathlib slice with an interleaved, position-controlled A/B against master: wall-clock difference -0.2% (indistinguishable from noise), CPU time +0.6%. Counts are bit-for-bit reproducible across runs (they are allocation counts, not timings), which is what makes them usable as a CI metric on ordinary noisy runners.

What does this PR enable?
The motivation is that the Lean community's most visible cost metric is line count, and line count invites golfing: a readable, reusable proof can be replaced by a shorter brute-force one, and every existing signal reports the change as neutral or better while compile time quietly grows. The two proofs below prove the same statement; the numbers are this PR's own measurements:

theorem length_range_200 : (List.range 200).length = 200 :=
List.length_range -- 1.4k heartbeats

set_option maxRecDepth 10000 in
theorem length_range_200' : (List.range 200).length = 200 := by
decide -- 238k heartbeats, 170× the cost

Making the number always available lets both humans and AI tools see this difference at the moment the proof is written. As a demonstration, this vscode-lean4 branch renders the count next to each goals-accomplished marker using the new diagnostic field: https://github.com/Latinum-Formal-Methods/vscode-lean4-heartbeats

For a project like Mathlib, the per-module JSON also enables a per-declaration cost diff on every PR: baselines come from the build cache (mathlib's lake exe cache needs a one-line change to distribute the sidecar files), so no second compilation is needed. Declarations that fail or time out currently record nothing, and examples are not annotated in the editor since all examples in a namespace share one internal name.

Question

Should these entries live in the .ilean file instead of a separate <module>.hb.json?
The two artifacts have the same lifecycle: always produced, derived, non-semantic per-module metadata, and .ilean is already packed by mathlib's build cache, so folding the entries in would need no Cache/IO.lean change and would add no extra file per module.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4a37393b74d177d5e32f06cfd097ff6eb9f507b8 --onto c4e6b62c3d955ef20da94310797072f7c4c5fa2b. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-07 03:24:04)
• ✅ Mathlib branch lean-pr-testing-14712 has successfully built against this PR. (2026-08-14 07:27:58) View Log
• ✅ Mathlib branch lean-pr-testing-14712 has successfully built against this PR. (2026-08-14 10:07:49) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4a37393b74d177d5e32f06cfd097ff6eb9f507b8 --onto c4e6b62c3d955ef20da94310797072f7c4c5fa2b. You can force reference manual CI using the force-manual-ci label. (2026-08-07 03:24:06)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-14 06:35:14)

[Kha]

The only way to recover it today is trace.profiler with trace.profiler.useHeartbeats, which costs 1.3×–5× compile time because it must retain and pretty-print the entire trace tree

Did you consider combining a high trace.profiler.threshold value with trace.Elab.command? That might still have some issues with output format, e.g. more --json support could be nice here, but hopefully it should minimize the overhead

[dennj]

The only way to recover it today is trace.profiler with trace.profiler.useHeartbeats, which costs 1.3×–5× compile time because it must retain and pretty-print the entire trace tree

Did you consider combining a high trace.profiler.threshold value with trace.Elab.command? That might still have some issues with output format, e.g. more --json support could be nice here, but hopefully it should minimize the overhead

On a file of 2000 small theorems, trace.profiler.threshold=100000 with trace.Elab.command and useHeartbeats costs 1.90x versus the always-on recording in this PR, against 3.11x for threshold=1000 with output.pp (the configuration that does give per-declaration numbers).

Without output.pp the profile contains 22 distinct frame names, and they are syntax kinds rather than declarations: all 2000 theorems land in the single frame Elab.command: Lean.Parser.Command.theorem (73,842k heartbeats), alongside bare Elab.definition.value and Elab.async frames. Since the Firefox Profiler aggregates by frame name, that gives a per-file total per syntax kind, not a per-declaration cost. I can't tell an expensive proof from a cheap one, which is the comparison the PR is for.

The threshold also removes the cheap tail by construction: it is compared against raw heartbeat deltas, so at 100000 anything under 100 heartbeats (in maxHeartbeats units) never appears. In my demo file, proving (List.range 200).length = 200 by decide costs 238k and shows up, while List.length_range costs 1.4k and is filtered out. So the very comparison that motivates the feature is invisible at that threshold.

Per-declaration attribution today therefore needs output.pp plus parsing declaration names back out of human-readable trace messages, which is what the 3.11x buys and why it isn't something you would leave on.