6.2. Why the timing AND repeat-doubling are in the child
A parent-side timer would include process spawn cost in the
measurement. Lean's startup includes module init, FFI library
load, and the runtime's own bookkeeping; that's tens of ms on a
non-trivial project. Including those in total_nanos would
corrupt every sub-millisecond measurement.
So the child does:
-
Run the function once. Time it.
-
While elapsed <
targetInnerNanos / 2, double the inner repeat count and re-run from scratch. -
Emit one JSONL row with
(inner_repeats, total_nanos, hash).
per_call_nanos = total_nanos / inner_repeats. The clock starts
after startup and stops before JSONL emission, so all the
parent-side / startup / IPC overhead is excluded.