[hyperpolymath]

Summary

Stacked on #455, which rewrites the same lines of live-provers.yml and carries the repair for main's current startup failures. Merge #455 first; GitHub then retargets this PR to main.

The T1 provision step ran apt-get update before every backend, including vampire, cvc5, alt-ergo and (with #455) chuffed, which install from GitHub release assets and never touch apt. On #446 the runner image's packages.microsoft.com source answered 403 twice, so T1 / vampire failed before any test ran (job 118637174820). The re-run passed, so it was the mirror and not the prover.

Changes

• live-provers.yml, T1 provision step: apt-get update moves into an apt_install helper. Only the apt-installed backends call it (z3, eprover, spass, glpk, minizinc). The release-asset backends no longer depend on the image's apt sources being reachable.

An earlier version of this branch also pinned the T1 Guix job to ubuntu-24.04. I dropped that, because #455 makes the same fix with a pinned guix version and a running daemon.

RSR Quality Checklist

Required

• Tests pass: workflow-only change; the checks below ran on audit: routing/rule-engine recon, Logtalk quarantine; Agda proofs re-checked under PROOF-POLICY §2.1 #455's tree plus this commit
• Code is formatted
• Linter is clean: actionlint with shellcheck, exit 0
• No banned language patterns
• No unsafe blocks without // SAFETY: comments: n/a
• No banned functions: n/a
• SPDX license headers present on all new/modified source files
• No secrets, credentials, or .env files included

As Applicable

• Docs, deed, roadmap, changelog: n/a (CI provisioning only)

Testing

Run locally on this tree:

• actionlint (with shellcheck) on live-provers.yml: clean.
• scripts/ci/test-issue-regressions.sh (with mikefarah yq v4): passed.
• scripts/ci/check-allow-fail-expiry.sh: 10 units, passed.
• In the provision step, sudo apt-get now appears only inside the helper.
• No uses: changed, so actions.lock is unaffected.

This PR's own CI is the live test of the T1 matrix on the new step.

---

Generated by Claude Code

[coderabbitai]

Important

Review skipped

Auto reviews are disabled on base/target branches other than the default branch.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: 300ab112-3b48-46de-8b5f-86ff8e917b39

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• Trigger review

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn

[hyperpolymath]

@coderabbitai review

This PR is stacked on #455, so its base isn't the default branch and auto-review skipped it. Requesting a review now so findings land before it retargets to main.

---

Generated by Claude Code

[coderabbitai]

Action not completed

Review rate limited.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[hyperpolymath]

Static Analysis Gate / panic-attack assail is red here, but this PR didn't cause it.

• The scanner exits 2 with assail: incomplete coverage (partial), and the receipt gate then rejects the missing completion receipt (job 126913664100).
• The same job fails the same way on this PR's base, audit: routing/rule-engine recon, Logtalk quarantine; Agda proofs re-checked under PROOF-POLICY §2.1 #455 at 346a31d (job 126908698977). That gate is one of the workflows audit: routing/rule-engine recon, Logtalk quarantine; Agda proofs re-checked under PROOF-POLICY §2.1 #455 rewrites.
• This PR changes only the T1 provision step in live-provers.yml, which the scanner job doesn't run.
• There's no fix to port yet. audit: routing/rule-engine recon, Logtalk quarantine; Agda proofs re-checked under PROOF-POLICY §2.1 #455 has pushed a newer head (3f47512) whose gate run is still in progress. Once audit: routing/rule-engine recon, Logtalk quarantine; Agda proofs re-checked under PROOF-POLICY §2.1 #455 is green I'll merge its head into this branch so CI re-runs. Not re-running now: the failure reproduces on the base.

---

Generated by Claude Code

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-11-04T23:03:20.678576Z	60f7ac4	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud