Skip to content

Commit 6a8da0b

Browse files
avrabeclaude
andauthored
fix: BCR presubmit with Nix + Rust nightly install (Pattern 1) (#23)
- Add standalone MODULE.bazel for examples/rust_to_rocq test module so BCR presubmit can build it as an independent Bazel module - Update .bcr/presubmit.yml to install Nix (--no-daemon) and Rust nightly-2024-12-07 with rustc-dev via shell_commands, matching the pattern used by rules_nixpkgs_core and rules_elm - Restrict to ubuntu2204 + Bazel 8.x (Nix single-user install is most reliable on Linux) - Set PATH and LIBRARY_PATH for Buildkite CI agent environment Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
1 parent ea3211f commit 6a8da0b

2 files changed

Lines changed: 64 additions & 3 deletions

File tree

.bcr/presubmit.yml

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,21 @@
11
bcr_test_module:
22
module_path: "examples/rust_to_rocq"
33
matrix:
4-
platform: ["debian11", "macos", "ubuntu2204"]
5-
bazel: ["7.x", "8.x"]
4+
platform: ["ubuntu2204"]
5+
bazel: ["8.x"]
66
tasks:
77
run_tests:
88
name: "Build rust_to_rocq example"
99
platform: ${{ platform }}
1010
bazel: ${{ bazel }}
11+
environment:
12+
# Nix installer updates ~/.profile but Buildkite CI disregards it.
13+
# Cargo/rustup installed to ~/.cargo/bin.
14+
PATH: /var/lib/buildkite-agent/.nix-profile/bin:/var/lib/buildkite-agent/.cargo/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
15+
# Rust nightly sysroot lib needed for linking rustc_private crates
16+
LIBRARY_PATH: /var/lib/buildkite-agent/.rustup/toolchains/nightly-2024-12-07-x86_64-unknown-linux-gnu/lib
17+
shell_commands:
18+
- curl -L https://nixos.org/nix/install | sh -s -- --no-daemon
19+
- curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain nightly-2024-12-07 -c rustc-dev,rust-src,llvm-tools-preview
1120
build_targets:
12-
- "//:all"
21+
- "//:point_proofs"

examples/rust_to_rocq/MODULE.bazel

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
"""BCR test module for rules_rocq_rust.
2+
3+
This standalone module exercises the full Rust-to-Rocq verification pipeline:
4+
translate Rust to Rocq, compile the Rocq code, and verify proofs.
5+
"""
6+
7+
module(
8+
name = "rules_rocq_rust_example",
9+
version = "0.1.0",
10+
)
11+
12+
# Depend on rules_rocq_rust (local_path_override for dev, BCR resolves it in presubmit)
13+
bazel_dep(name = "rules_rocq_rust")
14+
local_path_override(
15+
module_name = "rules_rocq_rust",
16+
path = "../..",
17+
)
18+
19+
# Nix integration (transitive dep from rules_rocq_rust, but root module must configure repo)
20+
bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0")
21+
22+
nix_repo = use_extension(
23+
"@rules_nixpkgs_core//extensions:repository.bzl",
24+
"nix_repo",
25+
)
26+
nix_repo.github(
27+
name = "nixpkgs",
28+
org = "NixOS",
29+
repo = "nixpkgs",
30+
# nixos-unstable with Rocq 9.0.1
31+
commit = "aca4d95fce4914b3892661bcb80b8087293536c6",
32+
sha256 = "",
33+
)
34+
use_repo(nix_repo, "nixpkgs")
35+
36+
# Rocq toolchain
37+
rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
38+
rocq.toolchain(
39+
version = "9.0",
40+
strategy = "nix",
41+
with_rocq_of_rust_deps = True,
42+
)
43+
use_repo(rocq, "rocq_toolchains", "rocq_stdlib", "rocq_coqutil", "rocq_hammer", "rocq_hammer_tactics", "rocq_smpl")
44+
register_toolchains("@rocq_toolchains//:all")
45+
46+
# rocq-of-rust toolchain
47+
rocq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "rocq_of_rust")
48+
rocq_of_rust.toolchain(
49+
use_real_library = True,
50+
)
51+
use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_source")
52+
register_toolchains("@rocq_of_rust_toolchains//:toolchain")

0 commit comments

Comments
 (0)