From 621d8080f6aefe0e066c45bef6eec566a1508075 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 30 May 2026 23:10:19 +0100
Subject: [PATCH] ci(wave3): stub-sentinel detection step in tier3-container
 matrix
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 .github/workflows/container-ci.yml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/.github/workflows/container-ci.yml b/.github/workflows/container-ci.yml
index 1b1121ee..44cd26fc 100644
--- a/.github/workflows/container-ci.yml
+++ b/.github/workflows/container-ci.yml
@@ -179,6 +179,28 @@ jobs:
           podman run --rm --entrypoint /bin/sh "${{ matrix.image }}" \
             -c '${{ matrix.version_check }}'
 
+      # #75: the per-prover version_check above uses `|| true` for several
+      # backends because tools like metamath / hol4 / acl2 exit non-zero on
+      # quit. Side effect: a stub fallback (graceful-degrade on a dead
+      # upstream pin, see Containerfile.wave3 :: tamarin/proverif/scip/metamath)
+      # prints "<prover> not available (... failed at image build time)" and
+      # `|| true` swallows it. This step re-runs the check, captures the
+      # output verbatim, and fails LOUDLY on any stub sentinel — turning the
+      # silent degradation into a visible weekly red.
+      - name: Stub-sentinel detection (#75)
+        run: |
+          set +e
+          OUTPUT=$(podman run --rm --entrypoint /bin/sh "${{ matrix.image }}" \
+            -c '${{ matrix.version_check }}' 2>&1)
+          echo "--- version_check output ---"
+          echo "$OUTPUT"
+          echo "--- end ---"
+          if echo "$OUTPUT" | grep -qiE 'not available \(bundle install failed|not available \(build failed|not available \(source build failed|bundle install failed at image build time|build failed at image build time|source build failed at image build'; then
+            echo "::error file=.containerization/Containerfile.wave3::Stub sentinel detected in ${{ matrix.prover }} image. The upstream pin is broken and was masked by graceful fallback — bump the pin (#75)."
+            exit 1
+          fi
+          echo "OK: no stub sentinel for ${{ matrix.prover }}"
+
       - name: Verify image metadata
         run: |
           podman inspect "${{ matrix.image }}" \