ci: Fix benchmarks

.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