Repository navigation
Wave-3: brittle upstream version pins need periodic verification (graceful stubs now hide drift) #75
Description
Tracked follow-up split out of PR #73. PR #73 made every Wave-3 target build
gracefully (stub/empty-export on a failed download instead of hard-failing
the image). Side effect: a dead upstream URL/version now silently degrades
the backend instead of loudly failing — so these pins need periodic
verification (ideally a CI smoke that asserts the real binary, not the stub).
Targets — exact location where each upstream is addressed
All in .containerization/Containerfile.wave3:
| Backend | ARG | Upstream resource | Observed |
|---|---|---|---|
| Poly/ML (hol4) | POLYML_VERSION=5.9.1 |
github.com/polyml/polyml tag tarball | release-asset URL 404'd → #73 switched to tag archive + fallback |
| OR-Tools | ORTOOLS_VERSION=9.12 |
github.com/google/or-tools release or-tools_amd64_debian-12_cpp_v9.12.tar.gz |
download failed in test → needs version/URL re-validation |
| SCIP | SCIP_VERSION=9.2.2 |
scipopt.org SCIPOptSuite-9.2.2-Linux-debian.bookworm.deb |
PASSED in test (valid as of now) — verify on drift |
| ACL2 | ACL2_VERSION=8.6 |
github.com/acl2/acl2 tag | PASSED — verify on drift |
| Tamarin | TAMARIN_VERSION=1.8.0 |
tamarin-prover releases linux64 tarball | PASSED — verify on drift |
Action
- Bump each ARG to a currently-valid upstream version when it drifts.
- Consider a weekly CI assertion that
--version/-helpreturns the real
prover, failing if the stub sentinel string is present.
Refs #53.
Activity
fix(wave3): hol4 pin trindemossen-2 (kananaskis-15 never existed → rc…
fix(wave3): pin HOL4 to existing release tag trindemossen-2 (#76)
fix(wave3): scip was a silent STUB — switch to real GitHub portable b…
fix(wave3): repair 4 silent-stub / non-relocatable backends (tamarin …
fix(wave3): repair 3 post-rebuild backend defects (metamath/or-tools/…
fix(wave3): make proverif a REAL backend — source build, not opam stub
fix(wave3): pin HOL4 to existing release tag trindemossen-2
hyperpolymath commentedon May 30, 2026
Verification pass run 2026-05-30. Three pins bumped via #156 (Poly/ML 5.9.1→5.9.2, OR-Tools 9.12→9.15, ACL2 8.6→8.7); SCIP 10.0.2 and Tamarin 1.12.0 are at latest; HOL4 trindemossen-2 is at latest. All five asset URLs HEAD-resolved before bumping — no dead-URL stub-degradation was masking drift at this snapshot.
Remaining ask from this issue: the CI smoke that asserts the real binary (e.g.
--versionparsed for a non-sentinel string) is the bigger lift and is not in #156. That can be filed as a follow-on if you want it tracked separately, or addressed by a second pass on this issue.hyperpolymath commentedon May 30, 2026
Second half shipped in #157 — adds a `Stub-sentinel detection` step to the existing `tier3-container` matrix in `container-ci.yml`. Re-runs each cell's `version_check`, captures output, fails loudly on the known sentinel patterns (`not available (bundle install failed` / `(build failed` / `(source build failed` / generic `*failed at image build time`). `continue-on-error: true` preserved so it stays informational rather than a merge gate, matching the rest of the job.
With #156 (pin bumps) + #157 (stub smoke) both armed, the two asks in this issue are addressed. Suggest leaving open until both land + the next weekly cron run shows the new step appearing across all 8 matrix cells. Then closeable.
chore(wave3): bump Poly/ML 5.9.1→5.9.2, OR-Tools 9.12→9.15, ACL2 8.6→…
ci(wave3): stub-sentinel detection step in tier3-container matrix (#157)
fix(ci): version_check via env var — unblocks acl2/hol4 cron cells (#75…
hyperpolymath commentedon Jun 1, 2026
Closeout
PRs #156 (pin bumps), #157 (stub-sentinel detection step), and #165 (env-var quoting fix) all landed. The shell-quoting bug that was breaking acl2 + hol4 cells on every cron since 2026-04-27 is now resolved at source.
Next weekly cron (Sunday 06:00 UTC) will produce the first run with all 8 matrix cells reaching the new stub-sentinel grep step. If acl2/hol4 still show graceful-stub output, the next pin bump goes through this issue's audit cadence; if they show real binary output, the per-prover roster declared in PR #156 is fully verified.
Closing now — the original ask ("add a CI smoke that asserts the real binary") is shipped end-to-end. Reopen if Sunday's cron exposes a Tier-3 cell that still silently degrades.
Refs #156, refs #157, refs #165.