From 87c22204a4d80977853b3d91e0b86ae34082a4f2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Thu, 4 Jun 2026 18:01:34 +0000 Subject: [PATCH] ci(nightly): remove issue-oracle steps (moved to Z3Prover/bench) (#9712) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Why Removes the three issue-oracle steps from the Ubuntu nightly job. They have been failing every nightly run since they landed in #9688 — see [run 26927938635](https://github.com/Z3Prover/z3/actions/runs/26927938635/job/79441695358): - **`Clone bench (for issue-oracle smoke test)`** → exit 128 with `fatal: could not read Username for 'https://github.com'`, because `Z3Prover/bench` is a private repo and the workflow had no credentials for it. - **`Run issue-oracle smoke test`** → exit 2 because `bench/scripts/issues_check_oracle.py` was never downloaded. - **`Upload issue-oracle report`** → warning because the JSON report was never produced. All three were absorbed by `continue-on-error: true`, so the job stayed green, but every nightly emitted two stale red error annotations and **the smoke test never actually ran**. ## What replaces it The smoke test has been moved to a new workflow in `Z3Prover/bench`: [`.github/workflows/issue-oracle.yml`](https://github.com/Z3Prover/bench/blob/ci/issue-oracle-pull-z3-nightly/.github/workflows/issue-oracle.yml) — see **Z3Prover/bench PR #2504**. The bench-side workflow: - runs at 04:30 UTC daily (this repo's nightly runs at 02:00 UTC + DAG, so ~2.5 h slack); - pulls the `z3-*-x64-glibc-*.zip` asset from **this repo's public `Nightly` release** via `gh release download` — unauthenticated for `Z3Prover/z3` because z3 is public, so **no cross-repo PAT and no `BENCH_REPO_TOKEN` secret** are required; - checks the release's `publishedAt` is < 18 h old, so a skipped/failed upstream nightly reds the workflow instead of silently re-testing yesterday's binary; - runs `issues_check_oracle.py` with the exact same smoke-test budget the deleted step used (`--max 200 --timeout 5 --wallclock 20 --jobs 0`, outer `timeout 90`); - uploads `issue-oracle-report.json` as an artifact (7-day retention). ## Scope of this PR Only the three dead steps are deleted; the downstream `Upload artifact` (`UbuntuBuild`) step and everything that depends on it (`deploy-nightly`, etc.) are unchanged. A short comment replaces the deleted block to direct future readers to the new home. ## Merge order This PR can land **before, after, or simultaneously with** the bench-side PR. There is no functional regression either way: - Today, the deleted steps produce zero useful output (just noisy annotations). Removing them is strictly an improvement to nightly log signal. - The bench-side workflow stands on its own and produces output the moment it lands (since it pulls from the already-existing `Nightly` release). ## Validation - `python -c "import yaml; yaml.safe_load(open('.github/workflows/nightly.yml'))"` → OK. - Search confirms no remaining live references to `bench/`, `BENCH_REPO_TOKEN`, or `issue-oracle-report.json` in `nightly.yml` (only the explanatory comment in the deletion block). - Diff: -56 / +9, single file. --- **Companion PR (do not merge before this one is reviewed):** https://github.com/Z3Prover/bench/pull/2504 --------- Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .github/workflows/nightly.yml | 56 ----------------------------------- 1 file changed, 56 deletions(-) diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml index 180dc6d90..12f063db2 100644 --- a/.github/workflows/nightly.yml +++ b/.github/workflows/nightly.yml @@ -244,63 +244,7 @@ jobs: - name: Test run: python z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2 - - name: Clone bench (for issue-oracle smoke test) - continue-on-error: true - run: | - # Sparse clone: bench is ~12 GB total but only scripts/ and - # inputs/issues/ (~800 MB) are needed by the oracle. The - # smoke-test runs on a sampled subset of iss-* dirs (see - # next step), so even this 800 MB pull is upper-bounded - # at the clone level rather than runtime. - git clone --depth 1 --filter=blob:none --sparse \ - https://github.com/Z3Prover/bench bench - git -C bench sparse-checkout set scripts inputs/issues - - name: Run issue-oracle smoke test - # continue-on-error: true means this step can NEVER red the - # nightly build. Its job is to produce a JSON report artifact, - # not to gate the build. The bounds below (--max 200, --timeout - # 5, --wallclock 20, outer timeout 90) keep the step under ~2 - # minutes regardless of corpus growth. - continue-on-error: true - run: | - # SMOKE-TEST budget (sampled subset of the corpus): - # --max 200 first 200 of ~2,700 iss-* dirs - # (sorted, so the same sample every run - # and easy to diff across nightlies) - # --timeout 5 per-file z3 cap (matches capture-time - # timeout/4, so any bench that escapes - # this cap was already on the edge) - # --wallclock 20 hard global cap INSIDE the script - # --quiet suppress per-issue progress lines - # timeout 90 shell-level belt-and-braces wrapper, - # leaves 30 s headroom for the script - # to flush its JSON report before SIGTERM - # The script ALWAYS exits 0 on normal operation, so the only - # ways this step can non-zero are: missing z3 binary, sparse - # clone failure (the previous step's continue-on-error - # absorbs that), or the outer `timeout` firing. All three - # are absorbed by this step's continue-on-error: true. - timeout 90 python bench/scripts/issues_check_oracle.py \ - --z3 build-dist/z3 \ - --all bench/inputs/issues \ - --max 200 \ - --timeout 5 \ - --wallclock 20 \ - --jobs 0 \ - --quiet \ - --json-report issue-oracle-report.json - - - name: Upload issue-oracle report - if: always() - continue-on-error: true - uses: actions/upload-artifact@v7.0.1 - with: - name: issue-oracle-report - path: issue-oracle-report.json - retention-days: 7 - - - name: Upload artifact uses: actions/upload-artifact@v7.0.1 with: