diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 1df78f94..c95e8f73 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -308,7 +308,7 @@ jobs: # and throughput are phase-scoped by the CELL (execute vs prove # testbed), and prove-time/verify-time/proof-size exist only on the # prove testbed — a threshold naming an absent measure just sits - # empty there. The per-phase `phase:` measures (witness gen, + # empty there. The per-phase `phase-` measures (witness gen, # stage commits, quotient, …) are uploaded for trend visibility but # intentionally left un-thresholded (noisy and dynamically named; # the PR-comment drill-down does the phase-level comparison). diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index c63f1d99..bc53cedd 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -654,18 +654,27 @@ jobs: env: PARSE_ERROR: ${{ needs.build.outputs.parse-error }} run: | - { - echo "## ❌ benchmark run failed" - if [ -n "$PARSE_ERROR" ]; then + if [ -f comment-body.md ]; then + # A report exists: some job failed but results came through. + # Soft note on top; the report's own footer links the logs. + { + echo "> ⚠️ Some benchmark jobs failed — results may be partial." echo - echo "> $PARSE_ERROR" - fi - echo - if [ -f comment-body.md ]; then cat comment-body.md; fi - echo - echo "[Workflow logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})" - } > body-with-header.md - mv body-with-header.md comment-body.md + cat comment-body.md + } > body-with-note.md + mv body-with-note.md comment-body.md + else + # No report at all: the run itself failed. + { + echo "## ❌ benchmark run failed" + if [ -n "$PARSE_ERROR" ]; then + echo + echo "> $PARSE_ERROR" + fi + echo + echo "[Workflow logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})" + } > comment-body.md + fi - name: Generate token to write PR comment id: app-token uses: actions/create-github-app-token@v3 diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index 5ba0e178..7f788b28 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -17,7 +17,7 @@ ONE PROCESS PER CONSTANT: a kill costs exactly that constant (its row is marked `status: oom`, keeping whatever the tool flushed), and each spawn's texray window (`.spans`) belongs wholly to it, folded - into the row as flat `phase:` fields — independent bencher + into the row as flat `phase-` fields — independent bencher measures with no attribution machinery; 4. gates the cell on the row contract (`Ix.Benchmark.Results`): exit 3 when any row is `rejected`, exit 1 when NO rows were produced, else 0. @@ -237,8 +237,20 @@ def readSpans (path : String) : IO (Array (String × Float)) := do | none => acc := acc.push (s, v) return acc +/-- A span name as a bencher-legal measure slug: lowercase alphanumerics + with every other character folded to `-` (`stark/stage1_commit` → + `stark-stage1-commit`). Row keys ARE bencher measure slugs — the slug + is the one identity uploads and `fetch-main` agree on — so they must + be born slug-shaped. -/ +def slugify (s : String) : String := + let dashed := s.toList.map fun c => if c.isAlphanum then c.toLower else '-' + -- Collapse runs so `a__b` and `a_b` can't alias two spellings apart. + let folded := dashed.foldl (init := []) fun acc c => + if c == '-' && acc.head? == some '-' then acc else c :: acc + String.ofList folded.reverse + /-- Fold a spawn's texray window (`.spans`) into its constant's row as - flat `phase:` fields — the aiur prover's tracing spans and the + flat `phase-` fields — the aiur prover's tracing spans and the zkVM hosts' `record_manual` entries alike — then drop the window file. The keys pass straight through `bmf` as independent bencher measures and come back from `fetch-main` in the same shape. No row (the tool @@ -250,7 +262,7 @@ def mergeSpans (out : String) (name : String) : IO Unit := do let rows ← readRows out if let some row := (rows.getObjVal? name).toOption then let row := spans.foldl (init := row) fun r (s, v) => - r.setObjVal! s!"phase:{s}" (jsonRound 6 v) + r.setObjVal! s!"phase-{slugify s}" (jsonRound 6 v) writeEntry out name row if ← FilePath.pathExists spansPath then IO.FS.removeFile spansPath diff --git a/Ix/Cli/BenchReport.lean b/Ix/Cli/BenchReport.lean index 6677f821..ff0f5713 100644 --- a/Ix/Cli/BenchReport.lean +++ b/Ix/Cli/BenchReport.lean @@ -36,7 +36,7 @@ namespace Ix.Cli.BenchReport def metricKind (metric : String) : String := if ["peak-rss", "file-size", "proof-size"].contains metric then "bytes" - else if metric.startsWith "phase:" then "seconds" + else if metric.startsWith "phase-" then "seconds" else if ["execute-time", "prove-time", "verify-time", "check-time", "compile-time"].contains metric then "seconds" else if ["fft-cost", "cycles", "steps", "max-shard-cycles", @@ -135,11 +135,11 @@ def rowNames (rows : Json) : Array String := | .obj kvs => kvs.toArray.map (·.1) | _ => #[] -/-- The `phase:` field names of one row (flat keys — same shape on +/-- The `phase-` field names of one row (flat keys — same shape on the PR side, in local baselines, and coming back from bencher). -/ def rowPhaseKeys (rows : Json) (name : String) : Array String := match (rows.getObjVal? name).toOption with - | some (.obj kvs) => kvs.toArray.map (·.1) |>.filter (·.startsWith "phase:") + | some (.obj kvs) => kvs.toArray.map (·.1) |>.filter (·.startsWith "phase-") | _ => #[] /-! ## compare -/ @@ -253,7 +253,7 @@ def renderCompare (a : CompareArgs) : String := Id.run do out := out.push "" |>.push "_⚠️ no PR-side results (see the workflow logs)._" -- Per-phase drill-down: the main table above carries every constant's - -- high-level row; below it, each constant with `phase:` fields + -- high-level row; below it, each constant with `phase-` fields -- (aiur witness/commit/quotient breakdowns, zkVM coarse phases) gets its -- own collapsed mini-table (`phase | main | PR | Δ%`), opened as -- desired. @@ -370,7 +370,7 @@ def shardMeasure (k : String) : String := /-- Rows JSON → Bencher Metric Format. Rows with `status ≠ ok` are dropped whole — a rejected or OOM'd constant must never become a bencher data - point. Numeric fields (`phase:` included) pass through as + point. Numeric fields (`phase-` included) pass through as measures. Nested per-shard objects (`shard-cycles: {"0": …}`) become per-shard BENCHMARKS (`/shard-0`) sharing the parent's measure slugs — multiplicity belongs in bencher's benchmark dimension, not as @@ -499,12 +499,16 @@ def runFetchMainCmd (p : Cli.Parsed) : IO UInt32 := do let ms := (bench.getObjVal? "measures").toOption.bind (·.getArr?.toOption) |>.getD #[] for m in ms do - let mName := (m.getObjVal? "measure").toOption.bind fun x => - (x.getObjVal? "name").toOption.bind (·.getStr?.toOption) + -- The SLUG is the source of truth: row keys are born + -- slug-shaped (see the registry metric lists and + -- `BenchCmd.slugify`), uploads attach to measures by it, and + -- the console-editable display name is never consulted. + let mSlug := (m.getObjVal? "measure").toOption.bind fun x => + (x.getObjVal? "slug").toOption.bind (·.getStr?.toOption) let mVal := (m.getObjVal? "metric").toOption.bind fun x => (x.getObjVal? "value").toOption - if let (some mn, some mv) := (mName, mVal) then - metrics := metrics.push (mn, mv) + if let (some ms, some mv) := (mSlug, mVal) then + metrics := metrics.push (ms, mv) if metrics.size > 1 then seen := seen.push name rows := rows.push (name, Json.mkObj metrics.toList) diff --git a/docs/benchmarking.md b/docs/benchmarking.md index 7902b931..bf9148c7 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -21,7 +21,7 @@ and one exit-code convention (Rust: `crates/bench`; Lean: `Ix/Benchmark/Results.lean`): ```json -{ "": { "status": "ok", "": 123, "phase:": 1.5 } } +{ "": { "status": "ok", "": 123, "phase-": 1.5 } } ``` - Rows are flushed after every name, so a killed run keeps its completed rows. @@ -100,7 +100,7 @@ With `--texray`, tools write per-phase span timings (`aiur/prove_ixvm`, `aiur/witness`, `stark/*`, `zisk/execute`, …) to `.spans`. The per-constant backends run **one process per constant**, so each spawn's window belongs wholly to its constant: `ix bench run` folds it into the -row as flat `phase:` fields, which flow to bencher as independent +row as flat `phase-` fields, which flow to bencher as independent measures (witness gen, stage commits, quotient, … each get a trend line) and render in the PR comment as a collapsible per-constant drill-down.