From adcd33f6fced4a9760167cd72f862a6173857362 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Mon, 9 Mar 2026 19:40:08 +0100
Subject: [PATCH] fix: BCR presubmit with Nix + Rust nightly install (Pattern
 1)

- 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>
---
 .bcr/presubmit.yml                 | 15 +++++++--
 examples/rust_to_rocq/MODULE.bazel | 52 ++++++++++++++++++++++++++++++
 2 files changed, 64 insertions(+), 3 deletions(-)
 create mode 100644 examples/rust_to_rocq/MODULE.bazel

diff --git a/.bcr/presubmit.yml b/.bcr/presubmit.yml
index 837e942..a1ac32a 100644
--- a/.bcr/presubmit.yml
+++ b/.bcr/presubmit.yml
@@ -1,12 +1,21 @@
 bcr_test_module:
   module_path: "examples/rust_to_rocq"
   matrix:
-    platform: ["debian11", "macos", "ubuntu2204"]
-    bazel: ["7.x", "8.x"]
+    platform: ["ubuntu2204"]
+    bazel: ["8.x"]
   tasks:
     run_tests:
       name: "Build rust_to_rocq example"
       platform: ${{ platform }}
       bazel: ${{ bazel }}
+      environment:
+        # Nix installer updates ~/.profile but Buildkite CI disregards it.
+        # Cargo/rustup installed to ~/.cargo/bin.
+        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
+        # Rust nightly sysroot lib needed for linking rustc_private crates
+        LIBRARY_PATH: /var/lib/buildkite-agent/.rustup/toolchains/nightly-2024-12-07-x86_64-unknown-linux-gnu/lib
+      shell_commands:
+        - curl -L https://nixos.org/nix/install | sh -s -- --no-daemon
+        - 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
       build_targets:
-        - "//:all"
+        - "//:point_proofs"
diff --git a/examples/rust_to_rocq/MODULE.bazel b/examples/rust_to_rocq/MODULE.bazel
new file mode 100644
index 0000000..a25da9e
--- /dev/null
+++ b/examples/rust_to_rocq/MODULE.bazel
@@ -0,0 +1,52 @@
+"""BCR test module for rules_rocq_rust.
+
+This standalone module exercises the full Rust-to-Rocq verification pipeline:
+translate Rust to Rocq, compile the Rocq code, and verify proofs.
+"""
+
+module(
+    name = "rules_rocq_rust_example",
+    version = "0.1.0",
+)
+
+# Depend on rules_rocq_rust (local_path_override for dev, BCR resolves it in presubmit)
+bazel_dep(name = "rules_rocq_rust")
+local_path_override(
+    module_name = "rules_rocq_rust",
+    path = "../..",
+)
+
+# Nix integration (transitive dep from rules_rocq_rust, but root module must configure repo)
+bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0")
+
+nix_repo = use_extension(
+    "@rules_nixpkgs_core//extensions:repository.bzl",
+    "nix_repo",
+)
+nix_repo.github(
+    name = "nixpkgs",
+    org = "NixOS",
+    repo = "nixpkgs",
+    # nixos-unstable with Rocq 9.0.1
+    commit = "aca4d95fce4914b3892661bcb80b8087293536c6",
+    sha256 = "",
+)
+use_repo(nix_repo, "nixpkgs")
+
+# Rocq toolchain
+rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
+rocq.toolchain(
+    version = "9.0",
+    strategy = "nix",
+    with_rocq_of_rust_deps = True,
+)
+use_repo(rocq, "rocq_toolchains", "rocq_stdlib", "rocq_coqutil", "rocq_hammer", "rocq_hammer_tactics", "rocq_smpl")
+register_toolchains("@rocq_toolchains//:all")
+
+# rocq-of-rust toolchain
+rocq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "rocq_of_rust")
+rocq_of_rust.toolchain(
+    use_real_library = True,
+)
+use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_source")
+register_toolchains("@rocq_of_rust_toolchains//:toolchain")