2.5. Memory metrics
Two optional fields on every row record per-child memory behaviour
(issue #6). They
sit alongside total_nanos so a regression that preserves
wall-clock time but allocates more memory or balloons RSS is still
visible.
field | unit | source | available on |
|---|---|---|---|
| bytes | not yet captured — Lean 4 has no portable in-process API | nowhere today |
| kibibytes |
| Linux |
Interpretation:
-
The values describe the child process for one batch (one
runOneBatch/runFixedOneBatchinvocation), not the parent. Incache_mode == "warm", the child runsinner_repeatsiterations of the function in a single process, sopeak_rss_kbis the peak RSS observed across that whole batch (which is what you usually want — a function whose RSS spikes once per call shows up inpeak_rss_kb). Incache_mode == "cold", each rung is its own child, sopeak_rss_kbis the per-call peak RSS. -
peak_rss_kbincludes the Lean runtime's own footprint (bytecode, static GC roots, the harness itself), not just the function under test. It is most useful as a delta across runs of the same benchmark, not as an absolute "this function uses N kB" reading. -
alloc_bytesis currently alwaysnull. It is reserved in the schema so downstream tooling can opt in to reading it once a Lean release exposes allocation counters in-process; until then, consumers should treat it as "not measured" rather than "zero".
Platform support:
-
Linux:
peak_rss_kbpopulated from the kernel's/proc/self/statusVmHWM:field. The kernel updatesVmHWMcontinuously as the process's RSS grows, so reading it once at the end of a batch gives the true peak across the whole run. -
macOS / Windows / Emscripten:
peak_rss_kbisnull. Reading peak RSS portably on those platforms requires either FFI (getrusageon macOS,GetProcessMemoryInfoon Windows) or a per-batch subprocess shell-out (e.g.ps), and a per-batch shell would itself dominate the metric for fast benchmarks. Adding a platform-specific probe is tracked as future work.
Reading them:
-
Both keys are documented as optional and may be
null. Readers must toleratenulland treat it as "no measurement" — never as zero. -
Both are emitted on every row by current writers (the writers stamp
nullwhen the platform can't supply a value), but readers must also tolerate the keys being absent entirely, in line with the general "tolerate missing optional keys" rule.