Skip to content

ci: decouple playwright/kani/rocq from needs:[test] (#299)#300

Open
avrabe wants to merge 1 commit into
mainfrom
fix/issue-299-decouple-playwright-kani-rocq
Open

ci: decouple playwright/kani/rocq from needs:[test] (#299)#300
avrabe wants to merge 1 commit into
mainfrom
fix/issue-299-decouple-playwright-kani-rocq

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented May 17, 2026

Closes #299.

Summary

Phase 1 of the CI fan-out de-coupling proposed in #299. When the self-hosted rust-cpu pool saturates (rivet-core mutation testing held it for ~4 hours on 2026-05-17, smithy commit 70401cd), the entire downstream CI tree blocks because eight jobs chain off test. Three of those — playwright, kani, rocq — have their own ubuntu-latest runner capacity available and are independent of cargo-test status.

Acceptance criteria from #299

  • Remove needs: [test] from playwright. .github/workflows/ci.yml line ~117. Replaced with a 4-line comment explaining the decoupling and back-referencing ci: decouple playwright/kani/rocq from needs:[test] to reduce blast radius of rust-cpu queue saturation #299. Playwright runs the release binary end-to-end via npx; cargo-test status is not a precondition.
  • Remove needs: [test] from kani. Line ~511. Kani harnesses are bounded model checks against rivet-core source; they do not read cargo-test status.
  • Remove needs: [test] from rocq. Line ~594. Rocq theorem proving runs against vendored .v files; it does not read cargo-test status.
  • Keep needs: [test] on coverage. Verified at the remaining grep line — coverage re-runs the same suite under llvm-cov so the dependency is legitimate.
  • Keep needs: [test] on mutants. Verified at the remaining grep line — mutants (lean-mem) mutation testing intentionally gates on a clean test baseline.
  • verus deferred to Phase 2. Verus still gates on test; no change in this PR per the issue's "Defer verus to Phase 2" line.

After the change, only five needs: [test] references remain in ci.yml: vscode-extension (Phase 2 audit), coverage (kept), mutants (kept), verus (deferred), release-results (Phase 2 fan-in concern).

Out of scope (Phase 2, not in this PR)

  • Auditing vscode-extension's dep on test.
  • Reconsidering the 5-way release-results fan-in.
  • Lowering cargo-mutants --jobs or sharding the rivet-core mutation suite.

Test plan

  • grep -n "needs:" .github/workflows/ci.yml — only the five expected references remain (vscode-extension, coverage, mutants, verus, release-results).
  • python3 -c "import yaml; yaml.safe_load(open('.github/workflows/ci.yml'))" — workflow is still valid YAML.
  • yamllint config (default + project overrides at .yamllint.yml): comment lines ≤120 chars, 4-space comment indentation matching surrounding context, no flow-style maps.
  • First post-merge CI run on main shows playwright, kani, rocq starting in parallel with test rather than queuing behind it. (Validated only after merge — that's the gate the issue describes.)

Commit traceability

ci type is exempt from artifact trailers per CLAUDE.md ("Exempt types (no trailer needed): chore, style, ci, docs, build."). No Implements: / Refs: lines required.


Generated by Claude Code

When the self-hosted rust-cpu pool saturates (rivet-core mutation
testing held it for ~4 hours on 2026-05-17), the entire downstream CI
tree blocks because eight jobs chain off `test`. Three of those jobs
— playwright (ubuntu-latest), kani (ubuntu-latest), rocq
(ubuntu-latest) — have their own runner capacity available and are
independent of cargo-test passing:

- Playwright runs the release binary end-to-end via npx.
- Kani harnesses are bounded model checks against rivet-core source.
- Rocq theorem proving runs against vendored .v files.

Remove `needs: [test]` from these three jobs (Phase 1 per #299).

Untouched (Phase 1 boundary):
- coverage / mutants — legitimately re-run the same suite, keep gate.
- verus — deferred to Phase 2.
- vscode-extension / release-results — Phase 2 audit items.

Closes #299.
@codecov
Copy link
Copy Markdown

codecov Bot commented May 18, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

ci: decouple playwright/kani/rocq from needs:[test] to reduce blast radius of rust-cpu queue saturation

2 participants