Pin CI sibling checkouts; add rules_rocq_rust (e4660cc)#17
Merged
Conversation
Makes the CI merge gate deterministic by pinning the relay and rivet
sibling repos to specific commit SHAs, instead of taking whatever main
is at workflow-run time. Adds rules_rocq_rust to wohl's MODULE.bazel
pinned to the same commit other PulseEngine repos (rivet) use, ahead
of any rocq proofs landing in proofs/rocq/.
CI pins (.github/workflows/ci.yml)
- RELAY_REF = 4d42acf (current relay main at pin time)
- RIVET_REF = 335bb84 (current rivet main at pin time)
- ref: ${{ env.RELAY_REF }} on every relay checkout (lint, test,
kani, fuzz-smoke jobs — 4 occurrences)
- ref: ${{ env.RIVET_REF }} on the rivet checkout (rivet-validate)
- Comment in env block points at #8 for the motivating incident
(PR #15 failed non-deterministically because rivet main advanced
0.10 -> 0.12 mid-PR and gained a new check).
- Bumping these refs is now an explicit PR, not a silent CI behavior
change.
rules_rocq_rust (MODULE.bazel)
- bazel_dep + git_override pinned to e4660cc (the rocq-of-rust
hermetic-toolchain commit; matches rivet's pin).
- Toolchain extension intentionally NOT wired yet — wohl has no
proofs/rocq/ to verify. When rocq proofs land, follow rivet's
pattern (rocq.toolchain + nixpkgs + register_toolchains).
- `bazel mod show_repo @rules_rocq_rust` confirms the override
resolves to e4660cc1b06fc4c0aefb49401fa2e2184cf804e3.
No code or artifact changes. CI behavior on this PR validates against
the pinned refs.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 23, 2026
avrabe
added a commit
that referenced
this pull request
May 23, 2026
PR #19's first CI run failed because rules_rocq_rust (added in #17) unconditionally creates a nixpkgs-backed `rocq_toolchains` repo at Bazel module-resolution time — that needs `nix-build` on PATH, even though no rocq rule is actually loaded by //proofs/verus. Per the architect's direction ("install Nix in CI, but pin"): - MODULE.bazel: add rules_nixpkgs_core (0.13.0) + nix_repo.github pinned to NixOS/nixpkgs commit aca4d95 (matches rivet's pin exactly — keep wohl and rivet in lock-step on the nixpkgs ref until there is a reason to diverge). Without nix_repo, rules_ rocq_rust falls back to behavior that varies by tool version. - ci.yml (verus job): add cachix/install-nix-action pinned to SHA 8aa03977 (v31.10.6) BEFORE the setup-bazel step. Pinning by SHA, not tag — tags can move; SHAs cannot. Local devs need nix installed for `bazel test //proofs/verus:...` too (a side-effect of #17's rules_rocq_rust addition). Mac: `brew install nix`; Linux: official installer or distro package. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 23, 2026
avrabe
added a commit
that referenced
this pull request
May 23, 2026
rules_rocq_rust (added in #17) calls rust_toolchain with `channel`, `iso_date`, and `version` attributes — newer-rules_rust APIs that wohl's pinned rules_rust commit (6281d27 via git_override) does not have. This blocks PR #19's Verus CI job at toolchain resolution. Match relay's pin: - bazel_dep rules_rust 0.61.0 -> 0.70.0 (from BCR) - drop the git_override to 6281d27 — that commit is now an ancestor of 0.70.0; the override was the old workaround for a Bazel API break that 0.61.0 had inherited (relay's MODULE.bazel comment documents this). - bazel_dep rules_wasm_component 0.1.0 -> 1.0.0 — rules_wasm_ component 1.0.0 also targets rules_rust 0.70.0; keep the local_ path_override so active rules_wasm_component dev still works. Validation - `bazel mod show_repo @rules_rust` resolves 0.70.0 from BCR cleanly. - `bazel mod show_repo @rules_wasm_component` resolves via the local override. - Existing CI (lint/test/kani/fuzz/rivet-validate) is cargo-based and does not exercise the bazel rules — so this PR's CI passes "trivially". The real bazel-side validation comes via PR #19's Verus job once rebased onto this. A future bazel build //:all CI job (tracked in #14 / #8) will be the standing gate for any rules_wasm_component API ripple through wohl's WASM components. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
May 24, 2026
Wires the Verus deductive-proof gate into CI. The bazel target was landed in Phase 2 Track D (#12 / SWARCH-WOHL-006's verification chain); this PR adds the corresponding workflow job, completing the Verus CI loop and closing issue #7. What the job does - Checks out wohl (path: wohl). - Checks out pulseengine/rules_wasm_component at a pinned SHA (new env var RULES_WASM_COMPONENT_REF). wohl's MODULE.bazel uses local_path_override for rules_wasm_component so local dev iterates against a sibling checkout; CI provides the same sibling layout from a pinned commit so module resolution succeeds without breaking the local-dev pattern. - Sets up Bazelisk via bazel-contrib/setup-bazel@0.15.0 with bazelisk-cache, disk-cache, and repository-cache enabled — keeps the Verus toolchain (~26 MB) and Bazel state cached across runs. - Runs `bazel test //proofs/verus:alert_dedup_verify`. rules_verus's hermetic toolchain handles the Verus binary download via the pinned 0.2026.02.15 toolchain in MODULE.bazel — no manual install. Closes #7. Pairs with #17 (sibling pinning) — this is the first CI job that actually runs Bazel; the pinning makes its behavior deterministic. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
May 24, 2026
PR #19's first CI run failed because rules_rocq_rust (added in #17) unconditionally creates a nixpkgs-backed `rocq_toolchains` repo at Bazel module-resolution time — that needs `nix-build` on PATH, even though no rocq rule is actually loaded by //proofs/verus. Per the architect's direction ("install Nix in CI, but pin"): - MODULE.bazel: add rules_nixpkgs_core (0.13.0) + nix_repo.github pinned to NixOS/nixpkgs commit aca4d95 (matches rivet's pin exactly — keep wohl and rivet in lock-step on the nixpkgs ref until there is a reason to diverge). Without nix_repo, rules_ rocq_rust falls back to behavior that varies by tool version. - ci.yml (verus job): add cachix/install-nix-action pinned to SHA 8aa03977 (v31.10.6) BEFORE the setup-bazel step. Pinning by SHA, not tag — tags can move; SHAs cannot. Local devs need nix installed for `bazel test //proofs/verus:...` too (a side-effect of #17's rules_rocq_rust addition). Mac: `brew install nix`; Linux: official installer or distro package. 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
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.
Summary
Makes the CI merge gate deterministic by pinning the
relayandrivetsibling-repo checkouts to specific commit SHAs, and addsrules_rocq_rustto wohl'sMODULE.bazelpinned to the same commit other PulseEngine repos use — ahead of any rocq proofs landing inproofs/rocq/.Closes the unpinned-sibling fragility item from #8.
What changed
.github/workflows/ci.ymlRELAY_REF/RIVET_REFenv vars pinning sibling commits.ref: ${{ env.RELAY_REF }}on every relay checkout (4 jobs: lint, test, kani, fuzz-smoke).ref: ${{ env.RIVET_REF }}on the rivet checkout (rivet-validate).rivet-validatefailed non-deterministically whenrivetmain advanced 0.10 → 0.12 mid-PR and gained a new check).MODULE.bazelbazel_dep(name = "rules_rocq_rust", version = "0.1.0")+git_overridepinned toe4660cc— matches rivet's pin exactly.proofs/rocq/yet. When rocq proofs land, follow rivet's pattern (rocq.toolchain+rules_nixpkgs_core+register_toolchains).bazel mod show_repo @rules_rocq_rustlocally confirms the override resolves toe4660cc1b06fc4c0aefb49401fa2e2184cf804e3.Verification
python3 -c "import yaml; yaml.safe_load(open('.github/workflows/ci.yml'))"→ OKbazel mod show_repo @rules_rocq_rust→ resolves to e4660cc ✓🤖 Generated with Claude Code