feat: production-ready improvements

1. Pin rocq-of-rust to specific commit with sha256:
   - Commit: 858907dbee116c51d7c6e87511bf5f92d6432ba4
   - SHA256: 2fcfb09c3d14091f021b3aa7876ada55a29708c7f27f6646d3ebee162975bf61

2. Fail loudly when rocq-of-rust build fails:
   - New fail_on_error option (default: True)
   - Clear error message with troubleshooting steps
   - Set to False for placeholder mode

3. Comprehensive documentation:
   - Prerequisites section with Linux Rust requirements
   - API reference for all rules
   - Configuration options
   - Troubleshooting guide

4. Added integration test for advanced example

Author: avrabe

README.md

@@ -10,25 +10,42 @@ Bazel rules for Rocq/Coq theorem proving and Rust formal verification with herme
 - **Cross-Platform**: Linux, macOS (Intel & Apple Silicon)
 - **Bazel 8 bzlmod**: Modern module system support
 
-## Prerequisites: Installing Nix
+## Prerequisites
 
-**Nix is required** for the Rocq toolchain.
+### Nix (Required)
 
-### macOS
+Nix is required for the Rocq toolchain.
 
+**macOS:**
 ```bash
 sh <(curl -L https://nixos.org/nix/install)
 . /nix/var/nix/profiles/default/etc/profile.d/nix-daemon.sh
 nix --version
 ```
 
-### Linux
-
+**Linux:**
 ```bash
 sh <(curl -L https://nixos.org/nix/install) --daemon
 nix --version
 ```
 
+### Rust Nightly (Linux only)
+
+On Linux, rocq-of-rust requires Rust nightly with rustc internals:
+
+```bash
+# Install nightly toolchain
+rustup toolchain install nightly-2024-12-01
+
+# Add required components
+rustup component add rustc-dev rust-src --toolchain nightly-2024-12-01
+
+# Set library path for LLVM (add to ~/.bashrc or ~/.zshrc)
+export LIBRARY_PATH="$(rustc +nightly-2024-12-01 --print sysroot)/lib:$LIBRARY_PATH"
+```
+
+On macOS, Nix provides the complete Rust toolchain automatically.
+
 ## Quick Start
 
 ### 1. Add to MODULE.bazel
@@ -71,53 +88,174 @@ impl Point {
 ### 3. Add BUILD.bazel
 
 ```starlark
-load("@rules_rocq_rust//coq_of_rust:defs.bzl", "coq_of_rust_library")
+load("@rules_rocq_rust//coq_of_rust:defs.bzl", "rocq_rust_verified_library")
 load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library")
 
-# Translate Rust to Rocq
-coq_of_rust_library(
-    name = "point_translated",
+# One-liner: translate and compile
+rocq_rust_verified_library(
+    name = "point_verified",
     rust_sources = ["point.rs"],
-    edition = "2021",
-)
-
-# Compile translated Rocq code
-rocq_library(
-    name = "point_compiled",
-    srcs = [":point_translated"],
-    deps = ["@rocq_of_rust_source//:rocq_of_rust_main"],
     extra_flags = ["-impredicative-set"],
 )
 
 # Write proofs about the Rust code
 rocq_library(
     name = "point_proofs",
     srcs = ["point_proofs.v"],
-    deps = [":point_compiled", "@rocq_of_rust_source//:rocq_of_rust_main"],
+    deps = [":point_verified"],
     extra_flags = ["-impredicative-set"],
 )
 ```
 
 ### 4. Build and verify
 
 ```bash
-# Translate and compile
-bazel build //:point_compiled
-
-# Verify proofs
 bazel build //:point_proofs
 ```
 
+## API Reference
+
+### rocq_library
+
+Compiles Rocq `.v` files to `.vo`.
+
+```starlark
+rocq_library(
+    name = "my_proofs",
+    srcs = ["proof.v"],
+    deps = [":other_library"],
+    include_path = "MyProject",      # Logical path prefix
+    extra_flags = ["-impredicative-set"],
+)
+```
+
+| Attribute | Description |
+|-----------|-------------|
+| `srcs` | Rocq source files (`.v`) |
+| `deps` | Dependencies on other `rocq_library` targets |
+| `include_path` | Logical path for this library (default: package path) |
+| `extra_flags` | Extra flags passed to coqc |
+
+### coq_of_rust_library
+
+Translates Rust source files to Rocq.
+
+```starlark
+coq_of_rust_library(
+    name = "translated",
+    rust_sources = ["lib.rs"],
+    edition = "2021",
+)
+```
+
+| Attribute | Description |
+|-----------|-------------|
+| `rust_sources` | Rust source files to translate |
+| `edition` | Rust edition (default: "2021") |
+
+### rocq_rust_verified_library
+
+Convenience macro: translates Rust to Rocq and compiles.
+
+```starlark
+rocq_rust_verified_library(
+    name = "verified",
+    rust_sources = ["lib.rs"],
+    edition = "2021",
+    deps = [],                       # Additional Rocq dependencies
+    extra_flags = ["-impredicative-set"],
+)
+```
+
+### rocq_proof_test
+
+Test rule that verifies proofs compile successfully.
+
+```starlark
+rocq_proof_test(
+    name = "proofs_test",
+    srcs = ["proofs.v"],
+    deps = [":proofs"],
+)
+```
+
+## Configuration Options
+
+### rocq_of_rust.toolchain()
+
+```starlark
+rocq_of_rust.toolchain(
+    use_real_library = True,         # Use full RocqOfRust library (recommended)
+    fail_on_error = True,            # Fail if rocq-of-rust build fails (default: True)
+    rust_nightly = "nightly-2024-12-01",  # Rust nightly version
+)
+```
+
+| Option | Description |
+|--------|-------------|
+| `use_real_library` | Use full RocqOfRust library with coqutil/hammer/smpl |
+| `fail_on_error` | Fail build if rocq-of-rust cannot be built |
+| `rust_nightly` | Rust nightly version for building rocq-of-rust |
+
+## Troubleshooting
+
+### "unable to find library -lLLVM-19-rust-*" (Linux)
+
+The Rust nightly compiler bundles its own LLVM. Set `LIBRARY_PATH`:
+
+```bash
+export LIBRARY_PATH="$(rustc +nightly-2024-12-01 --print sysroot)/lib:$LIBRARY_PATH"
+```
+
+### "cargo not found"
+
+Install Rust via rustup:
+
+```bash
+curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
+```
+
+### "rustc-dev component not found"
+
+Install the required nightly components:
+
+```bash
+rustup component add rustc-dev rust-src --toolchain nightly-2024-12-01
+```
+
+### Build fails silently with placeholder
+
+By default, builds fail loudly. If you see placeholder output, check the build logs for the actual error. To debug, run:
+
+```bash
+bazel build @rocq_of_rust_source//:rocq_of_rust_main --verbose_failures
+```
+
+### Proofs fail with "reference not found"
+
+Ensure the translated code compiled successfully first:
+
+```bash
+bazel build //:point_compiled
+```
+
+Then check that your proof imports match the generated module names.
+
 ## Example
 
-See `examples/rust_to_rocq/` for a complete working example with:
-- `point.rs` - Rust source code
-- Translated `point.v` (auto-generated)
-- `point_proofs.v` - Formal proofs about the Rust code
+See `examples/rust_to_rocq/` for a complete working example:
+
+- `point.rs` - Rust source with Point and Rectangle structs
+- `advanced.rs` - Generics, traits, lifetimes, enums
+- `point_proofs.v` - Formal proofs about the translated code
 
 ```bash
-# Build the example
+# Build all examples
 bazel build //examples/rust_to_rocq:point_proofs
+bazel build //examples/rust_to_rocq:advanced_verified
+
+# Run proof tests
+bazel test //examples/rust_to_rocq:point_proofs_test
 ```
 
 ## How It Works
@@ -129,15 +267,13 @@ bazel build //examples/rust_to_rocq:point_proofs
 
 ## Toolchain Contents
 
-The nixpkgs-based toolchain provides:
-
 | Component | Description |
 |-----------|-------------|
 | Rocq 9.0 | Core theorem prover |
 | coqutil | Utility library |
 | Hammer | Automated proof tactics |
 | smpl | Simplification tactics |
-| rocq-of-rust | Rust-to-Rocq translator |
+| rocq-of-rust | Rust-to-Rocq translator (pinned version) |
 
 ## Supported Platforms
 

coq_of_rust/extensions.bzl

@@ -8,7 +8,7 @@ _RocqOfRustToolchainTag = tag_class(
     attrs = {
         "commit": attr.string(
             doc = "Git commit hash or branch of rocq-of-rust",
-            default = "main",
+            default = "",  # Empty means use pinned default
         ),
         "sha256": attr.string(
             doc = "SHA256 of the source archive",
@@ -22,6 +22,10 @@ _RocqOfRustToolchainTag = tag_class(
             doc = "Use real RocqOfRust library (requires nixpkgs deps: coqutil, hammer, smpl)",
             default = False,
         ),
+        "fail_on_error": attr.bool(
+            doc = "Fail build if rocq-of-rust cannot be built (recommended for production)",
+            default = True,
+        ),
     },
 )
 
@@ -37,24 +41,31 @@ def _rocq_of_rust_impl(module_ctx):
     # Use first configuration or defaults
     if configs:
         config = configs[0]
-        commit = config.commit
+        commit = config.commit if config.commit else ""  # Empty uses pinned default
         sha256 = config.sha256
         rust_nightly = config.rust_nightly
         use_real_library = config.use_real_library
+        fail_on_error = config.fail_on_error
     else:
-        commit = "main"
+        commit = ""  # Uses pinned default in repository.bzl
         sha256 = ""
         rust_nightly = "nightly-2024-12-01"
         use_real_library = False
+        fail_on_error = True
 
     # Create source repository that downloads and builds rocq-of-rust
-    rocq_of_rust_source(
-        name = "rocq_of_rust_source",
-        commit = commit,
-        sha256 = sha256,
-        rust_nightly = rust_nightly,
-        use_real_library = use_real_library,
-    )
+    repo_kwargs = {
+        "name": "rocq_of_rust_source",
+        "rust_nightly": rust_nightly,
+        "use_real_library": use_real_library,
+        "fail_on_error": fail_on_error,
+    }
+    if commit:
+        repo_kwargs["commit"] = commit
+    if sha256:
+        repo_kwargs["sha256"] = sha256
+
+    rocq_of_rust_source(**repo_kwargs)
 
     # Create toolchain repository
     _create_toolchain_repo(name = "rocq_of_rust_toolchains")