rules_rocq_rust/examples/rust_to_rocq/MODULE.bazel at 16f6ff2ca7d326423e6fcb280ee508006db47b22 · pulseengine/rules_rocq_rust · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
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.1.1 (2026-04-01)
    commit = "6201e203d09599479a3b3450ed24fa81537ebc4e",
    sha256 = "",
)
use_repo(nix_repo, "nixpkgs")

# Rocq toolchain
rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
rocq.toolchain(
    version = "9.1",
    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")