diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index 391a8ffe7..a5089f05f 100644 --- a/.github/workflows/update.yml +++ b/.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 }} diff --git a/Ix/Cli/BenchPlots.lean b/Ix/Cli/BenchPlots.lean index c1c8037ab..2aa97bfff 100644 --- a/Ix/Cli/BenchPlots.lean +++ b/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 diff --git a/Ix/Cli/BenchReport.lean b/Ix/Cli/BenchReport.lean index 13f4df2bc..f9a2aa3dd 100644 --- a/Ix/Cli/BenchReport.lean +++ b/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