Surfaced by the L2.3 ADR (PR #154).
Problem
L2.3 introduced `exitCode = -5` for preempted losers (distinct from -3 timeout / -4 subprocess error). The `bench_mrr` CSV currently only reports `success / winning_prover` per strategy run; the per-prover preemption-vs-timeout-vs-success breakdown isn't captured. Without it, the wallclock improvement attributable to preemption can't be directly measured.
Acceptance
- `bench_mrr` emits a second CSV (or extra columns) reporting per-prover-per-strategy: completed-success, completed-failure, preempted (exit=-5), timed-out (exit=-3), not-available, subprocess-error.
- `docs/bench/` writeup re-run shows preemption rates next to wallclock.
- Optional: a `--telemetry-only` flag that skips the wallclock measurements when only the categorical breakdown is wanted.
Surfaced by the L2.3 ADR (PR #154).
Problem
L2.3 introduced `exitCode = -5` for preempted losers (distinct from -3 timeout / -4 subprocess error). The `bench_mrr` CSV currently only reports `success / winning_prover` per strategy run; the per-prover preemption-vs-timeout-vs-success breakdown isn't captured. Without it, the wallclock improvement attributable to preemption can't be directly measured.
Acceptance