ci: Fix benchmarks (#591)

* bench: fetch-main reads report results via per-uuid GET

Bencher's reports LIST endpoint stopped inlining each report's
`results` (it now carries only a `counts` summary), which fetch-main
read as "report found, zero rows" — every !benchmark base fetch on
every backend then exited 3 and silently fell back to a FULL base-side
rerun (rebuild the base binaries + re-measure), ~5 min of redundant
work per entry despite the rows sitting on bencher.

Fetch each SHA-matched report by uuid (the single-report GET still
returns full results) before row parsing; an inlined results array is
still used directly if the API populates it again. Validated against
live bencher at main@7da4132: the aiur-sharded-env/ISLB fetch that
drove the fallback in run 32749751301 now returns its row (5 measures,
empty missing list, exit 0), and a compile fetch at the same SHA
exercises the multi-report-per-testbed aggregation.

* bench: display titles for the aiur-sharded-env-check plots

The five new plots synced with the slug fallback ("aiur-sharded-env-
check: check-time"); name them in the house style — Aiur Env Check
Time / Throughput / Peak RAM Usage, Aiur Env Constants, Aiur Env
Shards. Verified via `ix bench plots --dry-run`.

* ci: lean-update sweeps every Benchmarks package via the /** glob

`. Benchmarks/**` replaces the hand-listed ". Benchmarks/Compile":
the recursive form reaches all seven packages under Benchmarks/
(Catalog, CatalogReal, CatalogSpine, Compile, CompileFC, and Catalog's
nested RelocFixture workspaces) while skipping dotted directories, so
.lake dependency checkouts stay untouched. CompileFC was previously
left pinned to an old toolchain on purpose; it now updates with the
rest.

Author: samuelburnham

.github/workflows/update.yml

@@ -32,9 +32,12 @@ jobs:
       # pinned to a commit hash is reported and left alone.
       - uses: argumentcomputer/lean-update@dev
         with:
-          # The root package and the compile benchmarks; Benchmarks/CompileFC
-          # is deliberately left on its old toolchain, so no glob here.
-          lake_package_directory: ". Benchmarks/Compile"
+          # The root package plus every package under Benchmarks/ — `/**`
+          # walks the whole tree (catching Catalog's nested fixture
+          # workspaces) and skips dotted directories, so `.lake`
+          # dependency checkouts are never swept up. This includes
+          # Benchmarks/CompileFC, previously pinned to an old toolchain.
+          lake_package_directory: ". Benchmarks/**"
           bump_mode: pinned-tags
           pr: true
           token: ${{ steps.app-token.outputs.token }}

Ix/Cli/BenchPlots.lean

@@ -78,6 +78,11 @@ def plotTitle (workload measure : String) : String :=
   | "ooc-check", "check-time"            => "OOC Check Time"
   | "ooc-check", "throughput"            => "OOC Check Throughput"
   | "ooc-check", "peak-rss"              => "OOC Check Peak RAM Usage"
+  | "aiur-sharded-env-check", "check-time" => "Aiur Env Check Time"
+  | "aiur-sharded-env-check", "throughput" => "Aiur Env Check Throughput"
+  | "aiur-sharded-env-check", "peak-rss"   => "Aiur Env Check Peak RAM Usage"
+  | "aiur-sharded-env-check", "constants"  => "Aiur Env Constants"
+  | "aiur-sharded-env-check", "shards"     => "Aiur Env Shards"
   | w, m => s!"{w}: {m}"
 
 /-- Tracked but not plotted solo. Zisk

Ix/Cli/BenchReport.lean

@@ -822,9 +822,30 @@ def runFetchMainCmd (p : Cli.Parsed) : IO UInt32 := do
     IO.println s!"fetch-main: no reports for {backend}/{mode} @ {sha.take 8}"
     return exitRejected
 
+  -- The LIST endpoint stopped inlining each report's `results` (it now
+  -- carries only a `counts` summary), which read here as "report found,
+  -- zero rows" and sent every caller down the full base-rerun fallback.
+  -- Fetch each matched report by uuid — the single-report GET still
+  -- returns full results; the inline array is used when a future API
+  -- (or cached response) populates it again.
+  let mut detailed : Array Json := #[]
+  for r in atSha do
+    let inline := (r.getObjVal? "results").toOption.bind (·.getArr?.toOption)
+      |>.getD #[]
+    if !inline.isEmpty then
+      detailed := detailed.push r
+    else
+      let some uuid := (r.getObjVal? "uuid").toOption.bind (·.getStr?.toOption)
+        | continue
+      match ← curlJson s!"https://api.bencher.dev/v0/projects/ix/reports/{uuid}" with
+      | .error e =>
+        IO.println s!"fetch-main: bencher API error (report {uuid}): {e}"
+        return exitRejected
+      | .ok full => detailed := detailed.push full
+
   let mut rows : Array (String × Json) := #[]
   let mut seen : Array String := #[]
-  for r in atSha do
+  for r in detailed do
     let iterations := (r.getObjVal? "results").toOption.bind (·.getArr?.toOption)
       |>.getD #[]
     for iteration in iterations do