Fix proof profiling heartbeat undercounts

[Vilin97]

The deprecated Mathlib heartbeat linter can re-elaborate an already-declared theorem and report the failed retry's cost instead of the original proof. This PR measures Lean's synchronous command heartbeat traces, including theorem bodies and kernel checking, sums disjoint root traces, and reports values in maxHeartbeats units. Added files get an absolute profile; modified files get a base-to-head comparison.

The report validates the expected file sections and complete timing trailers. A failed or zero-phase lean --profile run shows unavailable timing and contributes nothing to timing or phase totals; errors stay visible, and a separately successful heartbeat measurement remains available. A heartbeat trace now needs both a complete real/user/sys trailer and an explicit success marker written by the measurement wrapper. Truncated or failed traces cannot appear as cheaper comparisons. If the profile log's file headers match, an incomplete timed file is excluded without erasing healthy siblings. README documents the user-facing behavior.

At head 8a4cc951237e3673a9ae615dd67d68cbcc334b1b, 37 focused Python tests passed with two optional Lean integration tests skipped. Targeted Ruff checks, shell syntax, and git diff --check passed; two independent code reviews found no remaining parser blocker. The branch includes main dae605b417397b9609ca7108b6f61664f4f12cde through a normal merge. Fresh exact-head Python CI, Lean CI, and Documentation are running.

A project-wide timing calibration has not been rerun, so historical linter totals should not be compared directly with the new command counts. The workflow's absolute log remains an in-band text stream; a crafted complete sequence of expected sections could forge timings. Eliminating that requires a separate change to how the workflow produces the log. The real-Lean end-to-end test is opt-in and skipped in Python CI, which does not install a pinned Mathlib build; a bounded local run is queued.

[Vilin97]

Focused infrastructure review of exact head cbf5092a2ac357a33dfe0e59f061cf1f2b411245: the new root command trace includes full command syntax, but parse_heartbeat_sections in scripts/proof-profile/render.py:129–140 treats any line containing error: as a compiler error before matching a heartbeat trace. A successful file with def message : String := "error: harmless text" then reports zero declarations and no usable heartbeat total; a multiline command with the same literal is also marked failed. That removes valid files from absolute and base-to-head profile reports.

The exact-head parser reproduces both false failures, while the equivalent successful control without the literal produces 37.0 heartbeat units and genuine failure controls are still rejected. The current pytest run is green but lacks this case. Please distinguish actual failed measurement status or Lean diagnostics from echoed source syntax, and add regression tests for successful single-line and multiline traces containing error: alongside a genuine failure case. This is an author-actionable P2 parser bug; no maintainer decision is needed.

[Vilin97]

Reviewed exact head 792ce2d6b92e98dc5cabec0b5740ac972dfe6414. The earlier P2 false failure for successful Lean commands containing an error: literal is resolved by the terminal-status-aware heartbeat parser and regression cases. The subsequent forged ## section case is addressed by escaping later header-shaped lines when heartbeat logs are stitched, preserving physical LF boundaries in the renderer, and rejecting direct absolute logs with unexpected, duplicate, missing, reordered, or incomplete timed sections. Rejected profile times now display as unavailable rather than zero. The latest three-file commit is byte-identical to the locally tested repair; the workflow is unchanged.

Validation: 27 focused local tests passed (2 optional Lean integration tests skipped). Exact-head hosted Python CI passed 517 tests (2 skipped), with Ruff lint and format green; the PR separation guard is green. I found no new code blocker in this draft.

The disclosed residual limitation remains: proof-profile.log is written by the workflow as an in-band stream, so a deliberately crafted complete expected header-and-timing sequence could still forge absolute timings. Eliminating that requires changing the workflow producer. A project-wide benchmark and fresh comparison with historical linter totals remain outstanding. This COMMENT does not mark the draft ready to merge.

[Vilin97]

Reviewed exact head ab669246227c138ba7ef09dca7a88369ae1d90fb against current main dae605b417397b9609ca7108b6f61664f4f12cde. The earlier false failure for successful Lean commands containing error: and the malformed-section parser case remain fixed. The new repair also makes failed or zero-phase lean --profile timings unavailable, excludes their partial phases from totals, and retains errors and independently successful heartbeat measurements. The README now explains that behavior.

The focused local suite passed 29 tests with two optional Lean integration tests skipped; exact-head Python CI, Ruff, separation, and documentation preflight are green. An independent code read-through found no remaining correctness blocker, and there are no unresolved review threads. The protected Lean job has passed the project build, declaration lint, and style checks but is still running repository quality; its Build project aggregate is therefore pending.

Disposition: approved, integration/checks pending. Once the exact-head Build project check succeeds, re-read the head, main, checks, and review threads, then mark the draft ready and use normal protected merge. The disclosed project-wide timing calibration gap and in-band log-framing limitation remain advisory for this reporting feature; they are not changes to CI gates.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium risk]

The PR appears safe to merge; no new actionable issue or outstanding previous finding remains.

Summary

The PR replaces deprecated-linter heartbeat counts with synchronous Lean command traces and updates parsing and reporting so incomplete measurements cannot appear as valid costs.

• Adds explicit success and complete-timing requirements for heartbeat measurements.
• Excludes invalid timed files while retaining completed siblings’ phase totals.
• Adds regression tests and documents the advisory report.

_{Reviews (5) · Last reviewed commit: "Refactor profile stitching regression fi..."}

[Vilin97]

Reviewed exact head 94d0194a6acc1c55016d0472457fb53a996b2723: approved, integration/checks pending. The five-file profiling change measures synchronous root-command work once, rejects failed/truncated/legacy measurements, and keeps unavailable timings out of totals. I inspected the full diff and measurement/rendering callers, including forged section headers, nested traces, terminal status handling, and base/head comparisons. This changes advisory measurement, not a quality gate.

Integrated current main f0f9b418b in an isolated worktree and extracted the stitching fixture without changing the regression assertions. Ruff lint/format checks pass; 551 pytest tests pass, including both real Lean tests (legacy and module mode) against pinned Mathlib 5ed2965256430c3649e86755f9576b54eca72435. The first optional Lean run encountered an invalid local Mathlib checkout; rerunning with an intact checkout at the same pin passed. The test-length finding is resolved.

This account authored the PR, so this is the approval equivalent. Continuation: inspect fresh protected Build project, Content / non-content separation, Documentation preflight, Python checks and review threads; re-read the head and main; perform a normal protected squash once green and current. Auto-merge is disabled. Saved work: /data/codex/scratch/lean4lean4/daily-review/20260929T141549Z/worktree-543. No maintainer decision is needed.

[Vilin97]

/review

Please reassess exact head 94d0194a6acc1c55016d0472457fb53a996b2723: reviewed profiling behavior and regression coverage; the remaining long-test fixture is now factored, and all 551 local tests, including both real pinned-Lean measurements, pass.

[Vilin97]

🤖 LLM review — refactor (gpt-6-astra)

Reviewed head: 94d0194a6acc1c55016d0472457fb53a996b2723

Verdict: 🛑 request_changes

This refactors profiling from the deprecated heartbeat linter to synchronous command traces and strengthens log validation. No pooled proofs change. However, real Lean 4.34.0 traces contradict the assumption that unindented command traces represent disjoint work, producing double-counted costs and false improvements. Failed base measurements also disappear from the report’s error accounting. The 37 focused Python tests pass, but their synthetic traces miss these cases.

Aspect	Value
Scope	profiling pipeline refactor
Introduces tech debt	🛑 yes
Maintainability	🛑 regressed
Brittleness	🛑 more_brittle
Risk	🟡 medium

The validation improvements do not compensate for overlapping heartbeat counts and hidden base failures; fix both before merging.

Findings (2)

• overlapping-measurements — scripts/proof-profile/render.py:167
  Unindented Elab.command traces are not necessarily disjoint: Lean 4.34.0 prints both the theorem inside set_option … in and its enclosing command’s inclusive trace at column zero. This loop sums both. Using the exact measurement flags, removing only that wrapper from an unchanged proof produced a reported reduction from 4,662 to 2,327 maxHB units (50.1%) and classified it as cheaper. Preserve trace hierarchy through structured output or measure top-level commands directly, and add a real-Lean regression covering scoped commands.
• hidden-measurement-errors — scripts/proof-profile/render.py:345
  Filtering failed measurements out of compared also removes them from all comparison error reporting. When a base measurement fails and its head succeeds, the absolute fallback reads only head errors. With another healthy comparison present, the failed file appears under ‘New files’ with Errors = 0 and no failure warning. Keep failed measurements excluded from performance totals, but report excluded modified files with explicit per-side failure status.

---

Tokens: 1,132,480 in / 7,170 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $23.1873 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.

CI was not green for this commit at review time; this review does not replace CI.