lean-bench

5.1. How profile works🔗

$ lake exe bench profile NAME --profiler "PROFILER ARGS --" [--param N]

The harness assembles the argv:

PROFILER ARGS -- /path/to/bench _child --bench NAME --param N
                 --target-nanos T --cache-mode warm

… and IO.Process.spawns the result with stdout / stderr inherited. Differences from run:

  • Single param, no ladder. The full doubling/linear sweep would produce N profile artifacts that collide on the same output filename. Pick the param you want to investigate (--param 1024) and re-run for each one.

  • No kill-on-cap. Profilers can take seconds to flush their own output (perf record writes perf.data; samply boots a server). The wallclock cap that's right for benchmark mode would mis-fire.

  • No verdict reduction. The child still emits its single JSONL row with the timing — useful for correlating profile artefacts against an absolute wall time — but no aggregation happens.

  • Profiler command is opaque. The string you pass is whitespace-split into argv tokens; there is no shell-quoting layer. If your profiler invocation needs paths with spaces, wrap it in a one-liner script and pass the script's path.

The harness echoes the assembled command line to stderr before exec'ing so you can see exactly what was run.