Reduce source profiling overhead with cached native compact capture

[Vilin97]

Profiling previously paid for an interpreted driver, pervasive internal tracing, expression/symbol export, and repeated rewrites of the growing query index. CLI and VS Code captures now default to source-focused compact recordings using a cached native driver and a reused Lake environment. Timing bars, semantic declaration/tactic queries and source snapshots remain available; detailed internal/expression tracing is an explicit option.

The driver honors existing module setup options and native Lean async/snapshot/import defaults, retains sub-threshold declaration/async scopes, and waits for kernel completion. Linux compact source scopes and frontend totals use raw-clock endpoints; built-in Lean scopes are calibrated separately. No profiled LeanPool sources, quality gates, CI, installed toolchains, or existing public recordings are changed.

Measured on 21 pinned Mathlib and 3 pinned LeanPool files, with four rotating-order repeats and one discarded warmup per mode: 3.01% aggregate end-to-end overhead, including atomic recording publication/cleanup and query-index export. Complete-repeat overhead ranges from 2.81% to 3.22%; worst individual file is 10.74%. Cold preparation costs another 11.43–15.60 seconds per toolchain. Source/setup and frozen implementation hashes were audited. Full raw measurements and methodology are in docs/LOW-OVERHEAD.md and docs/benchmarks/2026-10-03-linux-compact.json.

Validation: 61 unit/CLI/viewer checks; compact same-run timing/range/thread/declaration/self-time/query parity; independent Python raw stopwatch; native/configured-option and kernel rejection checks in both modes; 30 portable capture, 13 collection and 17 stale-import checks; legacy interpreted declaration capture; actual browser folder/declaration/tactic/source navigation; VSIX and CLI package builds and a real capture from the extracted CLI tarball without development dependencies.

Native compilation is validated on Linux x64 with Lean 4.34.0-rc2, 4.34.0 and 4.35.0-rc3; macOS/Windows native paths still need platform validation. Built-in timer calibration assumes a stable rate within each segment, ancillary phase counters are estimates, custom source/build roots are not automatically resolved, and the selected-file benchmark is not a full-corpus rerun or a universal error bound.

[greptile-apps]

Confidence Score: 4/5

[High risk] Adds compiled native capture backend with new data format.

The PR appears safe to merge, with non-blocking improvements warranted for cancellation isolation, session completion resilience, benchmark comparability and large-recording memory use.

Findings

1.  Shared compilation couples cancellations ▶
2.  Folder append delays completion ▶
3.  Compact benchmark repeats preparation ▶
4.  Compact files can expand heavily ▶

Summary

The PR makes compact, native-driver capture the default while retaining detailed capture, adds compact recording support and clock calibration, and changes session indexing to append query rows.

• The native backend is compiled and cached per toolchain; CLI and VS Code expose the capture-mode choice.
• The recording reader and viewer support source-focused events, and the PR adds validation and overhead measurements.

Diagram

%%{init: {'theme': 'neutral'}}%%
flowchart LR
  A[CLI or VS Code capture] --> B[Prepare cached native backend]
  B --> C[Run Lean frontend]
  C --> D[Write compact or detailed recording]
  D --> E[Append per-file query rows]
  E --> F[Checkpoint session manifest]
  F --> G[Reader filters committed files and recomputes folders]

Loading

_{Reviews (1) · Last reviewed commit: "Make compact native source profiling the..."}

[greptile-apps]

Shared compilation couples cancellations When two callers prepare the same backend at once, they share a compilation tied to the first caller’s abort signal. Cancelling the first caller also fails the other caller; cancelling the second caller does not stop its wait. This makes concurrent use of the exported backend API unreliable.

[greptile-apps]

Folder append delays completion If this final write fails, the session never reaches its final manifest checkpoint and remains marked partial even though every file was captured. Readers discard these stored folder rows and recompute them, so the write adds a failure point without benefiting those readers.

[greptile-apps]

Compact benchmark repeats preparation Every benchmark request prepares the backend, but this branch calls capture(), which prepares it again. Native and baseline requests prepare it only once. The compact end-to-end measurement therefore includes an extra validation step, making the modes less directly comparable than the documented methodology suggests.

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[greptile-apps]

Compact files can expand heavily A recording can pass the disk-size check with up to three million events, then expand into millions of node objects plus the maps and child arrays built during normalization. Opening a large, otherwise valid recording can use substantially more memory than its file size suggests. Bound or stream the expanded data and test the upper limit.