ci: fix Rocq Formal Proofs — bump rules_rocq_rust to hermetic toolchain

[avrabe]

Problem

The Rocq Formal Proofs CI job (bazel build //proofs/...) has been failing — pre-existing breakage, identical on main. It is not a problem with LOOM's .v proof files.

The failure happens inside the rocq_of_rust_source Bazel repository rule (from rules_rocq_rust), while it builds the rocq-of-rust-rustc binary from source:

rust-lld: error: unable to find library -lLLVM-19-rust-1.85.0-nightly
collect2: error: ld returned 1 exit status
error: could not compile `rocq_of_rust_lib` (bin "rocq-of-rust-rustc")

rocq-of-rust is a rustc driver, so it dynamically links librustc_driver → libLLVM. librustc_driver is passed to the linker by absolute path, but libLLVM is passed as -lLLVM-19-rust-1.85.0-nightly and must be resolved via linker search paths. That .so lives in <rust-sysroot>/lib, which was never placed on LIBRARY_PATH.

Root cause

LOOM pinned rules_rocq_rust at 307b65f (Feb 2). That revision's repository rule only passes through an ambient LIBRARY_PATH and never adds the Rust toolchain's own lib/ directory. LOOM's CI does not export LIBRARY_PATH, so the link step cannot find libLLVM.

rules_rocq_rust PR #25 fixed this: the repository rule now downloads a hermetic Rust nightly sysroot and prepends <sysroot>/lib to LIBRARY_PATH / LD_LIBRARY_PATH itself. LOOM's pin simply predated that fix.

Fix

Bump the git_override pin 307b65f → 424e6a6 (current rules_rocq_rust main). No LOOM CI changes are needed — the hermetic toolchain is self-contained.

Rocq versions are unaffected: rules_rocq_rust main is still Rocq 9.0 (the 9.1 upgrade is an unmerged draft), matching rocq.toolchain(version = "9.0") here.

Verification

CI on this PR will exercise the Rocq Formal Proofs job. The rocq-of-rust toolchain build is confirmed working on rules_rocq_rust's own green main CI, where libLLVM-19-rust-1.85.0-nightly.so is present in <sysroot>/lib.

🤖 Generated with Claude Code