feat: always record per-declaration heartbeat costs with no performance degradation

[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.

[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)

[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)