ci(wave3): stub-sentinel detection step in tier3-container matrix#157
Merged
Conversation
Second half of #75: the per-prover smoke-check step uses \`|| true\` for backends whose CLIs exit non-zero on quit (metamath/hol4/acl2/etc.) This was correct for those backends in isolation, but it also swallowed the case where a graceful stub fallback (defined in Containerfile.wave3 for tamarin/proverif/scip/metamath) printed its sentinel line — \"<prover> not available (... failed at image build time)\" — and exited 1. Result: a broken upstream pin masked as a passing weekly container build, exactly the regression #75 was filed to surface. This step re-runs the matrix's \`version_check\`, captures stdout+stderr verbatim, and fails LOUDLY (\`::error::\` annotation + exit 1) on any of the known sentinel patterns: - \"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) Imandra is intentionally NOT pattern-matched here — its stub message includes \"proprietary licence required\" rather than the build-time sentinels, and it is excluded from the matrix anyway (not licensable in public CI). Hard-fail backends without a graceful stub (or-tools, hol4, acl2, poly/ml) are covered by the existing build step failing the cell outright. \`continue-on-error: true\` on the job is preserved — these weekly images are informational, not merge gates — so a stub detection shows as a red ❌ step inside an amber/yellow job, visible in the Actions UI without blocking. That matches the rest of the tier3-container contract. Refs #75 (closes the second half — the bumps shipped in #156). 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
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
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:
Out of scope (by design)
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:
Test plan
Refs #75.
🤖 Generated with Claude Code