ci: CI reliability — Miri timeout headroom + Verus on ubuntu-latest (v0.17.0, #509)#520
Merged
Conversation
…n runs The release-commit CI run went red solely because Miri timed out at 30 min on the self-hosted lean-mem pool while it was contended clearing the #509 outage backlog — every required gate (Format/Clippy/Test/Docs/YAML/Traceability) was green, and Rocq proofs passed. Miri's own comment already anticipated this ("Revisit once we have a few green runs to set the budget closer to actual"; it was previously bumped 15→30 for the same lean-mem slowness). 45 min gives headroom on the lean-mem class without masking a real hang (a genuine UB loop still trips the budget). Does not touch the deliberate self-hosted runner choice. Refs: #509 Trace: skip
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
⚠️ Performance Alert ⚠️
Possible performance regression was detected for benchmark 'Rivet Criterion Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.
| Benchmark suite | Current: b8355f1 | Previous: 23b2495 | Ratio |
|---|---|---|---|
query/10000 |
305834 ns/iter (± 4393) |
232555 ns/iter (± 3605) |
1.32 |
This comment was automatically generated by workflow using github-action-benchmark.
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…rocq job Verus Proofs was perma-red at the "Install Nix" step: the no-sudo daemonless DeterminateSystems installer (crafted for the self-hosted NoNewPrivileges runner) broke on a version bump and escalated to sudo, which fails there. The proofs never even ran. Rocq does the identical Bazel+Nix work on ubuntu-latest with cachix/install-nix-action@v30 and is green. Move Verus to the same config: ubuntu-latest + cachix installer + nix_path. Fixes the install, and removes the job's dependency on the self-hosted pool (also a #509 resilience win). 16 GB hosted RAM is ample for the rivet Verus specs; the lean-mem RAM headroom is no longer needed. Stays continue-on-error (advisory) like rocq. Refs: #509 Trace: skip
avrabe
changed the title
…st, Miri timeout) as v0.17.0 scope Tracks the Miri+Verus CI-reliability fixes in this PR as the first v0.17.0 scope item (baseline v0.17.0-track), traced to REQ-051 (CI-enforced gates) and the #509 resilience theme. Trace: skip
📐 Rivet artifact delta
Graphgraph LR
REQ_215["REQ-215"]:::added
classDef added fill:#d4edda,stroke:#28a745,color:#155724
classDef removed fill:#f8d7da,stroke:#dc3545,color:#721c24
classDef modified fill:#fff3cd,stroke:#ffc107,color:#856404
classDef overflow fill:#e2e3e5,stroke:#6c757d,color:#495057,stroke-dasharray: 3 3
Added
Posted by |
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.
First v0.17.0 work: CI reliability (#509 theme). Two fixes so a fully-green-on-the-required-gates run stops showing red from infra flakiness on the self-hosted pool.
1. Miri timeout 30 → 45
The post-release main run went red solely because Miri timed out at 30 min on the
lean-memself-hosted runner while it was contended clearing the #509 backlog — every required gate was green and Rocq passed. Miri's own comment already called for this ("Revisit once we have a few green runs"). 45 min gives headroom without masking a real hang. Keeps the deliberate self-hosted runner.2. Verus → ubuntu-latest + cachix (mirrors the green Rocq job)
Verus Proofs was perma-red at "Install Nix": the no-sudo daemonless DeterminateSystems installer (crafted for the self-hosted
NoNewPrivilegesrunner) broke on a version bump and escalated tosudo, which fails there — the proofs never ran. Rocq does the identical Bazel+Nix work onubuntu-latestwithcachix/install-nix-action@v30and is green. Verus now mirrors that exactly. Also removes the job's dependency on the self-hosted pool (a #509 resilience win). Stayscontinue-on-error(advisory) like Rocq.Verification
actionlintclean (modulo pre-existing custom runner-label false positives); YAML valid.ubuntu-latest.Refs #509. Part of the v0.17.0 CI-reliability scope (REQ-215).
🤖 Generated with Claude Code