loom/MODULE.bazel at main · pulseengine/loom · 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
###############################################################################
# LOOM Bazel Module Configuration
#
# Uses Bzlmod for modern dependency management.
# See: https://bazel.build/external/overview#bzlmod
###############################################################################

module(
    name = "loom",
    version = "0.3.0",
)

# Rocq/Coq formal verification support
# See: https://github.com/pulseengine/rules_rocq_rust
# Requires nix to be installed: sh <(curl -L https://nixos.org/nix/install)
bazel_dep(name = "rules_rocq_rust", version = "0.1.0")

# Override to fetch from GitHub (not yet in BCR)
git_override(
    module_name = "rules_rocq_rust",
    remote = "https://github.com/pulseengine/rules_rocq_rust.git",
    commit = "307b65f",
)

# Rocq toolchain extension (creates internal nixpkgs for bzlmod compatibility)
rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
rocq.toolchain(
    version = "9.0",    # Rocq 9.0 for rocq-of-rust compatibility
    strategy = "nix",   # Hermetic nix-based installation
)
use_repo(
    rocq,
    "rocq_coqutil",
    "rocq_hammer",
    "rocq_hammer_tactics",
    "rocq_nixpkgs",
    "rocq_smpl",
    "rocq_stdlib",
    "rocq_toolchains",
)

register_toolchains("@rocq_toolchains//:all")

# rocq-of-rust toolchain for translating Rust to Rocq
rocq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "rocq_of_rust")
rocq_of_rust.toolchain(
    commit = "858907dbee116c51d7c6e87511bf5f92d6432ba4",  # Pinned for reproducibility
    use_real_library = True,  # Full library with coqutil/hammer/smpl
)
use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_source")

register_toolchains("@rocq_of_rust_toolchains//:toolchain")