mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-06 09:00:52 +00:00
Code Activity

ci(nightly): remove issue-oracle steps (moved to Z3Prover/bench) (#9712)

Browse source 
## 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>
This commit is contained in:
Lev Nachmanson 2026-06-04 18:01:34 +00:00 • committed by GitHub
parent 98ce7f5d05
commit 87c22204a4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

56
.github/workflows/nightly.yml vendored
View file

@ -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: