chore(wave3): bump Poly/ML 5.9.1→5.9.2, OR-Tools 9.12→9.15, ACL2 8.6→8.7#156
Merged
Merged
Conversation
Verification pass on the Wave-3 brittle pins tracked in #75. Five upstreams checked against latest GitHub releases (or git tags for ACL2, which doesn't use GitHub Releases): | Backend | Was | Latest | Action | |---|---|---|---| | Poly/ML | 5.9.1 | 5.9.2 (2025-08-11) | bumped | | OR-Tools | 9.12.4544 | 9.15.6755 (2026-01-12) | bumped (BUILD also) | | SCIP | 10.0.2 | 10.0.2 (2026-04-02) | current ✓ | | ACL2 | 8.6 | 8.7 (git tag) | bumped | | Tamarin | 1.12.0 | 1.12.0 (2026-03-07) | current ✓ | Additional checks: HOL4 trindemossen-2 (current — latest is also trindemossen-2 from 2025-08-12). All five existing-pin asset URLs HEAD-resolved before bumping, so no dead-URL stub-degradation was masking a download failure at this snapshot. OR-Tools BUILD number for v9.15 (6755) verified via the GitHub releases API for that tag — matches the actual asset name `or-tools_amd64_debian-12_cpp_v9.15.6755.tar.gz`. Comment block updated to reflect the new example in case the bump becomes the new reference. Risk: OR-Tools jumped 3 minor versions (9.12 → 9.15) which carries the most ABI surface for downstream Rust callers via the C++ FFI. The other two are patch (Poly/ML) and minor (ACL2) bumps and are low-risk. Container build + the existing Wave-3 smoke jobs will exercise the upgrades. Refs #75. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 30, 2026
Wave-3: brittle upstream version pins need periodic verification (graceful stubs now hide drift)
#75
Open
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
## Summary Second half of #75 — the per-prover smoke-check step in the weekly Tier-3 container build uses \`|| true\` for backends whose CLIs exit non-zero on quit (metamath/hol4/acl2/etc.). That was correct for the per-backend version-check intent, but it also silently swallowed the case where a **graceful stub fallback** (defined in \`Containerfile.wave3\` for tamarin/proverif/scip/metamath) printed its sentinel and exited 1. Result: a broken upstream pin masquerading as a passing weekly build — exactly the regression #75 was filed to surface. This adds a new step (\`Stub-sentinel detection (#75)\`) that re-runs each matrix cell's \`version_check\`, captures stdout+stderr verbatim, and fails LOUDLY with a \`::error::\` annotation on any of: | Pattern | Source backend | |---|---| | \`not available (bundle install failed\` | tamarin, scip | | \`not available (build failed\` | metamath | | \`not available (source build failed\` | proverif | | \`bundle install failed at image build time\` | generic | | \`build failed at image build time\` | generic | | \`source build failed at image build\` | generic | ## Out of scope (by design) - **Imandra** is not matched — its stub says \"proprietary licence required\" rather than the build-time sentinels, and it's excluded from the matrix anyway (not licensable in public CI). - **Hard-fail backends** without a graceful stub (or-tools, hol4, acl2, poly/ml) — these crash the build step itself if their upstream is dead, so they're already covered. ## Gate semantics \`continue-on-error: true\` on the job is preserved. These weekly images are **informational, not merge gates** — so a stub detection shows as red ❌ inside an amber/yellow job, visible in the Actions UI without blocking. That matches the rest of the \`tier3-container\` contract. ## Companion Bumps for the stale pins (Poly/ML / OR-Tools / ACL2) shipped in #156. With both this PR and #156 merged, #75's two asks are addressed: 1. ✓ Bump stale pins. 2. ✓ Catch silent stub-degradation in CI before it lingers another month. ## Test plan - [ ] Workflow lint / actionlint passes. - [ ] Next weekly Tier-3 cron run shows the new step appearing in each matrix cell. - [ ] Manual probe: if a future pin breaks (or someone simulates it by replacing an upstream URL with a 404 in a fork), the stub-sentinel step fires red. Refs #75. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Verification pass on the Wave-3 brittle upstream pins tracked in #75.
Five upstreams checked against latest GitHub releases (or git tags for
ACL2, which doesn't ship GitHub Releases):
Also checked: HOL4
trindemossen-2(latest as of 2025-08-12, current ✓).URL hygiene
All five existing-pin asset URLs HEAD-resolved before the bump, so no
dead-URL stub-degradation (the original #75 concern about graceful
fallbacks hiding drift) was masking a download failure at this
snapshot. After this PR lands, the same set of URLs has been
HEAD-checked for the new tags. The smoke that #75 also asks for
(weekly assertion that
--versionreturns the real prover, not thestub sentinel) is a separate piece of work — not in this PR.
OR-Tools BUILD coupling
The OR-Tools archive name embeds both VERSION and BUILD:
or-tools_amd64_debian-12_cpp_v9.15.6755.tar.gz. Both ARGs must movetogether on any version bump. The inline comment has been updated to
reflect the new example so the next reader has the current reference
point.
Test plan
.github/workflows/cargo-audit.yml/ any Wave-3 smoke that exercises Containerfile.wave3).saved_acl2.corebuilds with the SBCL recipe in the next stage.configure && make && make installrecipe unchanged.Refs #75.
🤖 Generated with Claude Code