ci: Add `ix bench plots` command to set bencher plots by samuelburnham · Pull Request #483 · argumentcomputer/ix

samuelburnham · 2026-07-10T20:17:52Z

ix bench plots command takes the latest metrics and parameters and uses the bencher CLI to recreate the dashboard plots accordingly
Parses env vars on a single line instead of only multiple for the !benchmark workflow
Fixes the compile Mathlib env as a !benchmark input
Prints Aiur prove throughput in the !benchmark comment
Removes phase printing from the !benchmark comment by default, add it back with BENCH_PHASES=1
Prunes Vectors.csv to remove redundant constants, adds Std.Hashmap as a heavy test
Fixes Zisk and SP1 peak-rss measurement by bumping tracing-texray in their workspaces, and now collects/prints shards and total constants correctly

Local aiur prove runs plus per-constant closure profiles (targets, ingress bytes, fft-cost) showed a third of the cheap tier measuring the same thing: - drop the base-cost floor duplicates (3-9 constant closures, <13 kB, prove within noise of each other): Acc.rec, Trans.mk, Sum.elim, Prod.map, Option.bind, Array.toList — Eq.rec stays as the recursor representative, Except.bind for monadic bind, WellFounded.fix for recursion combinators; - drop Nat.toDigits (strictly inside Nat.repr's closure), Array.filter and Array.foldlM (within 1.5x of Array.map, which stays), Int.add (scale twin of primary Nat.add_comm; Int is covered by emod/gcd); - drop the Int8/Int16/Int32 instRxcHasSize_eq triplets (byte-identical siblings of the kept Int64) and the trivials Nat, HEq, HEq.rec, Nat.add; - add Std.HashMap as HEAVY: 1,982-constant closure, 2.28 MB ingress, 84.6 s / 49 GiB / 18.4B FFTs proved locally — 6-40x every cheap constant on every axis. The prove-feasible full set is now 20 constants spanning recursors, WF recursion, monadic bind, List/Array, Nat/Int/BitVec/USize arithmetic, decidability, bytes/strings, hashing, and (via the heavy tier) big structures.

The zisk and sp1 hosts pinned tracing-texray at an older rev than the root workspace (bumped in #467), so cargo linked TWO instances of the crate into each host: main() started one instance's RSS sampler while ix_bench::peak_rss_bytes() read the other's never-started one — always None — and the resulting null was dropped by `ix bench bmf`'s numeric-fields filter. Net effect: every zisk upload silently lost peak-rss (parent and per-shard rows alike) since the pin diverged. Align both hosts on the root rev and re-lock; cargo tree confirms a single shared instance, so the sampler the host starts is the one the row emission reads.

constants = the named constants certified over the checked closure — the pre-shard input set, the same universe the aiur rows count via closureFrom. The cheap paths emit the cover size; the shard-plan path emits `needed` (targets this run answers for), computed before shard partitioning and store-reuse filtering, so neither sharding overhead nor covered-shard skips distort it. Anon-work dedup shrinks the WORK item count, never this number; sharding's extra work stays visible in cycles/execute-time where it belongs. shards was already emitted on shard-plan rows; a non-sharded execute now reports 1 (a single leaf IS one shard) instead of omitting the field and rendering n/a in the compare table. bench-main pins constants 0/0 on the zkvm testbeds like the other cells: it is deterministic, and a drop means lost coverage, not a win.

- aiur prove cells report throughput (constants/prove-time was already uploaded and thresholded; the registry column list just omitted it — every other cell follows the time/throughput/peak-rss convention). - zisk compare tables gain constants and shards columns, next to cycles. - The per-constant phase drill-downs are now opt-in via BENCH_PHASES=1 (a passthrough config key): the spans are noisy and dynamically named, so the default comment stays at the headline measures. - KEY=VALUE config parses inline on the command line too, whitespace- separated — the single-line form for bench-pr.yml's manual workflow_dispatch, whose input box cannot hold newlines. Inline keys are strict (an unknown key rejects, like a typo'd backend); config lines stay lenient since comment prose contains `=`.

One plot per (testbed, measure) bench-main tracks, one line per benchmark row the cell uploads, plus the cross-kernel input-constants overlay (aiur and zisk report the same pre-shard closure count, so the paired lines must coincide — separation is a coverage-drift tripwire). Titles, dashboard ordering, redundancy skips, and canonical measure units live here as typed data; the spec derives from the registry + Vectors.csv, so nothing is hand-listed. Idempotent, keyed by title: matching plots are kept (index re-asserted), stale ones deleted and recreated (the plot PATCH endpoint only takes index/title/window), hand-pinned ones untouched. The sync also asserts measure units — bencher auto-creates measures with placeholder units on first upload, leaving plots unitless. All bencher.dev traffic goes through the bencher CLI; --dry-run previews with no key. bencher-plots.yml dispatches it manually (like bencher-thresholds-reset) off the freshest bench-bins cache: run it after a registry change has merged AND bench-main has built it — the registry is compiled into the binary, and a new constant only gets its plot line once its first rows upload.

…le subpackage BENCH_ENVS=Mathlib died at 'Get Mathlib Cache' with 'unknown executable cache': use-mathlib-cache runs `lake exe cache get`, and mathlib is a dependency of the Benchmarks/Compile subpackage, not the root workspace lean-action was pointed at. bench-main had this right; bench-pr now mirrors it: - compile job: provision from Benchmarks/Compile (same toolchain as root) and `lake build Compile<env>` before the measured compile; - benchmark cells: no mathlib cache at all — the .ixe comes from the compile job, and the lazy Mathlib fallback fails loudly rather than fetching oleans it still couldn't build; - base side: the build action stays on the base root (it builds ix); a separate step fetches/builds base mathlib oleans in the subpackage when a Mathlib cell must re-run the base.

The benchmark cells carried two lazy fallbacks for artifacts the compile job publishes in the same run: a missing compile row made the compile cell re-measure the compile in-cell, and a missing `.ixe` made `ix bench run` recompile the env fresh. Neither could ever work for the Mathlib env (its oleans live only in the compile job's subpackage provisioning), so the fallbacks meant InitStd and Mathlib failed differently for the same infrastructure problem. Both restores are now fail-on-cache-miss and the run step always passes `--ixe`: the artifacts were published moments earlier, so a miss is an infrastructure failure and every env fails the same way, loudly, at the restore step. The in-cell "Save PR .ixe" step goes with the fallback that produced it.

The zkVM hosts uploaded cycles/second under the same `throughput` slug every other cell used for constants/second, so the shared measure had no honest unit (and the dashboard showed a generic "per second"). The hosts now report constants/second like everyone else — cheap zisk rows over the certified cover, shard-plan rows over the pre-shard `needed` set, sp1 over its checked count (its stdout already printed this number; the row disagreed) — via one shared `ix_bench::throughput` calculator. A zkVM's cycle rate stays derivable from its `cycles` and `execute-time` fields. The bencher measure's canonical units become "constants / second". NB: the first post-merge zisk upload drops throughput by orders of magnitude (meaning change, not a regression) — reset the zisk-check-execute baseline (!bencher-thresholds-reset) right after, or the 10% lower bound alerts.

samuelburnham · 2026-07-10T20:17:52Z

ix bench plots command takes the latest metrics and parameters and uses the bencher CLI to recreate the dashboard plots accordingly
Parses env vars on a single line instead of only multiple for the !benchmark workflow
Fixes the compile Mathlib env as a !benchmark input
Prints Aiur prove throughput in the !benchmark comment
Removes phase printing from the !benchmark comment by default, add it back with BENCH_PHASES=1
Prunes Vectors.csv to remove redundant constants, adds Std.Hashmap as a heavy test
Fixes Zisk and SP1 peak-rss measurement by bumping tracing-texray in their workspaces, and now collects/prints shards and total constants correctly