feat(rocq): wire mathcomp into the toolchain — Coq-Interval is unusable without it

MODULE.bazel

@@ -59,8 +59,11 @@ rocq.toolchain(
 # hammer_tactics is a separate package from hammer (plugin vs library)
 # flocq/interval/coquelicot/gappa_bin/gappalib enable machine-checked
 # floating-point error-bound proofs (#37); gappalib is built from source
-# against Flocq, same as smpl is built from source against Rocq 9.0
-use_repo(rocq, "rocq_coquelicot", "rocq_coqutil", "rocq_flocq", "rocq_gappa_bin", "rocq_gappalib", "rocq_hammer", "rocq_hammer_tactics", "rocq_interval", "rocq_smpl", "rocq_stdlib", "rocq_toolchains")
+# against Flocq, same as smpl is built from source against Rocq 9.0.
+# rocq_interval_env is a separate coq_9_0.withPackages(...) composition that
+# resolves Coq-Interval's real transitive closure (mathcomp/bignums/HB/elpi)
+# for rocq_interval_proof -- see DD-003 / rules_rocq_rust#43.
+use_repo(rocq, "rocq_coquelicot", "rocq_coqutil", "rocq_flocq", "rocq_gappa_bin", "rocq_gappalib", "rocq_hammer", "rocq_hammer_tactics", "rocq_interval", "rocq_interval_env", "rocq_smpl", "rocq_stdlib", "rocq_toolchains")
 
 # Register Rocq toolchain
 register_toolchains("@rocq_toolchains//:all")

README.md

@@ -174,7 +174,7 @@ Test rule that verifies proofs compile successfully.
 | Hammer | Automated proof tactics |
 | smpl | Simplification tactics |
 | Flocq | Floating-point formalization library |
-| Coq-Interval | Interval arithmetic / approximation-error bounds |
+| Coq-Interval | Interval arithmetic / approximation-error bounds, usable via `rocq_interval_proof` (see `rocq:defs.bzl`) -- Coq-Interval's real dependency closure (mathcomp, bignums, hierarchy-builder, coq-elpi) is resolved by a dedicated `coq_9_0.withPackages(...)` environment, not the primary toolchain |
 | Coquelicot | Real analysis library (Coq-Interval's dependency) |
 | Gappa | Rounding-error prover binary, kernel-checked via `gappa_proof` (see `rocq:defs.bzl`) |
 | gappalib-coq | Gappa's Rocq support library (built from source against Flocq) |
@@ -220,6 +220,13 @@ proof (Gappa + Flocq), kernel-checked by Rocq:
 bazel test //examples/gappa_proof:rounding_bound_test
 ```
 
+See `examples/interval_proof/` for a smoke test proving Coq-Interval is
+actually usable (`Require Import Interval.Tactic`), not just fetched:
+
+```bash
+bazel test //examples/interval_proof:smoke_test
+```
+
 ## License
 
 Apache-2.0 — see [LICENSE](LICENSE).

artifacts/requirements.yaml

@@ -118,25 +118,90 @@ artifacts:
       - type: satisfies
         target: REQ-002
 
+  - id: DD-003
+    type: design-decision
+    title: Use coq_9_0.withPackages to resolve Coq-Interval's transitive closure, instead of hand-wiring each nixpkgs sub-package
+    status: implemented
+    description: >
+      Fix for the Coq-Interval usability gap (#43): `Require Import
+      Interval.Tactic` failed because #41 fetched `coqPackages.interval` but
+      never wired its real dependency closure, and #43's own fix attempt
+      (`coqPackages.mathcomp`) turned out to be a 1-file umbrella re-export,
+      not the real `mathcomp-boot` package the error named.
+    fields:
+      decision: >
+        Coq-Interval's real dependency closure is bignums + coquelicot +
+        flocq + mathcomp-boot + mathcomp-fingroup (per nixpkgs
+        `coqPackages.interval.propagatedBuildInputs`), and mathcomp-boot
+        itself needs hierarchy-builder, which needs coq-elpi (a real OCaml
+        findlib plugin, not a plain .v library) -- whose own OCaml deps
+        (ppx_deriving.runtime, ...) go deeper still. Hand-wiring each as a
+        separate nixpkgs_package + -Q flag (the pattern this toolchain uses
+        for coqutil/Hammer/smpl/Flocq/Interval/Coquelicot) doesn't scale past
+        this point. `@rocq_interval_env` (rocq/extensions.bzl) is a single
+        `coq_9_0.withPackages (p: [p.flocq p.interval p.coquelicot])`
+        composition that resolves the *entire* transitive closure
+        automatically, exposed as its own `coqc` + `user-contrib` tree. A new
+        `rocq_interval_proof` rule (rocq/private/rocq.bzl) compiles against
+        this dedicated environment -- it needs no `-Q` flags at all, since
+        the composed coqc already has its own default load path. Verified:
+        `bazel test //examples/interval_proof:smoke_test` compiles `Require
+        Import Interval.Tactic. Goal (1+1<=3)%R. Proof. interval. Qed.`
+        cleanly -- PASSED.
+      rationale: >
+        withPackages is nixpkgs' own answer to exactly this problem class
+        (deep, OCaml-plugin-laden Coq dependency graphs) -- reinventing its
+        closure resolution by hand is the same mistake #41 already made once
+        (missing bignums) and #43 repeated (wrong mathcomp attribute, still
+        missing bignums/HB/elpi). The primary toolchain (coqutil/Hammer/smpl,
+        rocq-of-rust) is left untouched -- this is a second, dedicated
+        environment scoped to the approximation-layer packages only, since
+        `rocq_toolchain_info` assumes one `coqc` for every compile and
+        unifying the whole toolchain onto `withPackages` is a bigger,
+        separate change not needed to close this gap.
+      alternatives: >
+        Continue hand-wiring mathcomp-boot + mathcomp-fingroup + bignums +
+        hierarchy-builder + coq-elpi + coq-elpi's own OCaml findlib deps
+        individually -- rejected: the OCaml findlib chain for elpi didn't
+        terminate in manual testing (ppx_deriving.runtime was the next
+        missing piece with no guarantee it's the last). Unifying the entire
+        toolchain onto one withPackages-composed coqc (retiring the
+        hand-rolled Hammer OCAMLPATH wiring too) -- rejected for now as
+        larger-blast-radius than this fix needs; worth revisiting later.
+      source-ref: "pulseengine/rules_rocq_rust#43, #41"
+    links:
+      - type: satisfies
+        target: REQ-002
+
   - id: FEAT-001
     type: feature
     title: Machine-checked FP error-bound proofs (Flocq + Gappa + Coq-Interval)
     status: implemented
     description: >
       Toolchain capability requested in #37, enabling a raise-assurance proof
       on top of relay's existing exhaustive-enumeration empirical bound.
-      Verified via `bazel test //examples/gappa_proof:rounding_bound_test`,
-      which exercises the full chain: a `.gappa` rounding-bound statement,
-      Gappa's `-Bcoq` codegen, and a real Rocq kernel check of the emitted
-      proof term against gappalib-coq/Flocq — PASSED.
+
+      Rounding layer (Gappa + Flocq): verified via `bazel test
+      //examples/gappa_proof:rounding_bound_test` -- a `.gappa`
+      rounding-bound statement, Gappa's `-Bcoq` codegen, and a real Rocq
+      kernel check of the emitted proof term against gappalib-coq/Flocq --
+      PASSED.
+
+      Approximation layer (Coq-Interval): initially fetched but not usable
+      (#43); fixed via DD-003 (`coq_9_0.withPackages`) and verified via
+      `bazel test //examples/interval_proof:smoke_test` -- a real `Require
+      Import Interval.Tactic` proof compiles end-to-end -- PASSED.
     fields:
       phase: phase-1
       acceptance-criteria:
         - "Toolchain flake provides flocq, gappa (binary), gappalib-coq, interval, coquelicot, pinned against the bundled Rocq version -- DONE (rocq/extensions.bzl, rocq/private/gappalib_repository.bzl)"
         - "rocq_library (or a new gappa_proof rule) can depend on the new packages' .vo/include paths -- DONE (gappa_proof macro, rocq/defs.bzl)"
+        - "Coq-Interval is actually usable (Require Import Interval.Tactic resolves and a smoke proof compiles) -- DONE (rocq_interval_proof + @rocq_interval_env, DD-003, examples/interval_proof, bazel test PASSED)"
         - "A minimal example proves one f32 rounding bound end-to-end, kernel-checked by Rocq, as the template for relay's kernels -- DONE (examples/gappa_proof, bazel test PASSED)"
     links:
       - type: satisfies
         target: REQ-002
       - type: implements
         target: DD-001
+      - type: implements
+        target: DD-003

claims.yaml

@@ -67,3 +67,24 @@ claims:
         path: examples/gappa_proof/BUILD.bazel
       - kind: file-exists
         path: examples/gappa_proof/rounding_bound.gappa
+
+  # #43/DD-003: Coq-Interval claimed "usable" must mean a real Interval.Tactic
+  # proof compiles, not just that the package is fetched (the #41/#43 mistake).
+  # Structural evidence: the dedicated environment + rule this depends on must
+  # exist, and the example's own pointer must resolve to a real target.
+  - id: EXAMPLES-INTERVAL-PROOF
+    doc: README.md
+    text: "bazel test //examples/interval_proof:smoke_test"
+    evidence:
+      - kind: file-exists
+        path: examples/interval_proof/BUILD.bazel
+      - kind: file-exists
+        path: examples/interval_proof/smoke.v
+      - kind: count-min
+        pattern: 'rocq_interval_env'
+        glob: ['rocq/extensions.bzl']
+        min: 1
+      - kind: count-min
+        pattern: 'rocq_interval_proof'
+        glob: ['rocq/private/rocq.bzl']
+        min: 1

examples/interval_proof/BUILD.bazel

@@ -0,0 +1,16 @@
+# Smoke test for the Coq-Interval environment (DD-003, #43): proves
+# Require Import Interval.Tactic actually resolves and a proof compiles --
+# not just that the coq-interval package is fetched.
+
+load("@rules_rocq_rust//rocq:defs.bzl", "rocq_interval_proof", "rocq_proof_test")
+
+rocq_interval_proof(
+    name = "smoke",
+    srcs = ["smoke.v"],
+)
+
+rocq_proof_test(
+    name = "smoke_test",
+    srcs = [],
+    deps = [":smoke"],
+)

examples/interval_proof/smoke.v

@@ -0,0 +1,11 @@
+(* Minimal smoke test for the Coq-Interval environment (DD-003, #43).
+   Proves this toolchain can actually load and use Interval.Tactic, not just
+   fetch the coq-interval package -- FEAT-001's approximation-error layer. *)
+
+Require Import Reals.
+Require Import Interval.Tactic.
+
+Goal (1 + 1 <= 3)%R.
+Proof.
+  interval.
+Qed.

rocq/defs.bzl

@@ -1,9 +1,10 @@
 """Public API for Rocq compilation rules."""
 
-load("//rocq/private:rocq.bzl", _rocq_library = "rocq_library", _rocq_proof_test = "rocq_proof_test")
+load("//rocq/private:rocq.bzl", _rocq_interval_proof = "rocq_interval_proof", _rocq_library = "rocq_library", _rocq_proof_test = "rocq_proof_test")
 
 rocq_library = _rocq_library
 rocq_proof_test = _rocq_proof_test
+rocq_interval_proof = _rocq_interval_proof
 
 def gappa_proof(name, src, deps = [], extra_flags = [], visibility = None):
     """Runs `gappa -Bcoq` on a `.gappa` source and kernel-checks the result.

rocq/extensions.bzl

@@ -224,6 +224,12 @@ filegroup(
 '''
 
 # BUILD file for Coq-Interval (interval arithmetic / approximation-error bounds)
+# NOTE: this filegroup alone is NOT enough to `Require Import Interval.Tactic`
+# -- Interval's real dependency closure (per nixpkgs
+# coqPackages.interval.propagatedBuildInputs) is bignums + coquelicot + flocq +
+# mathcomp-boot + mathcomp-fingroup, and mathcomp-boot transitively needs
+# hierarchy-builder + the coq-elpi OCaml plugin. See @rocq_interval_env below
+# (DD-003) for the environment that actually resolves the whole closure.
 _INTERVAL_BUILD_FILE = '''
 package(default_visibility = ["//visibility:public"])
 
@@ -249,6 +255,32 @@ filegroup(
 )
 '''
 
+# BUILD file for the Coq-Interval environment (DD-003). Interval's real
+# dependency closure includes mathcomp-boot/mathcomp-fingroup (which need
+# hierarchy-builder, which needs the coq-elpi OCaml plugin, which needs its
+# own OCaml findlib closure) -- hand-wiring each as a separate nixpkgs_package
+# doesn't scale past this point (see rules_rocq_rust#43's review). This is a
+# single `coq_9_0.withPackages(...)`-composed coqc that resolves the whole
+# closure the way nixpkgs is designed to. Its own subdirs are already named
+# Flocq/Interval/Coquelicot/mathcomp/Bignums/HB/elpi -- exposing user-contrib
+# with an empty logical root maps each to its correct name in one -Q.
+_INTERVAL_ENV_BUILD_FILE = '''
+package(default_visibility = ["//visibility:public"])
+
+filegroup(
+    name = "coqc",
+    srcs = ["bin/coqc"],
+)
+
+filegroup(
+    name = "user_contrib",
+    srcs = glob([
+        "lib/coq/**/*.vo",
+        "lib/coq/**/*.glob",
+    ], allow_empty = True),
+)
+'''
+
 # BUILD file for the standalone gappa binary (external rounding/approximation prover)
 # Gappa is not a Coq plugin -- it's an external CLI whose `-Bcoq` mode emits a
 # Rocq proof script (see gappa_proof in coq_of_rust:defs.bzl / rocq:defs.bzl,
@@ -391,6 +423,18 @@ import (builtins.fetchTarball {{
             build_file_content = _INTERVAL_BUILD_FILE,
         )
 
+        # Coq-Interval environment (DD-003) -- a coq_9_0.withPackages(...)
+        # composition that resolves Interval's whole transitive closure
+        # (bignums, mathcomp-boot/fingroup, hierarchy-builder, coq-elpi and
+        # its own OCaml deps) the way nixpkgs is designed to, instead of
+        # hand-wiring each nixpkgs sub-package (see rules_rocq_rust#43).
+        nixpkgs_package(
+            name = "rocq_interval_env",
+            repository = nixpkgs_repo,
+            nix_file_content = "(import <nixpkgs> { config = {}; overlays = []; }).coq_9_0.withPackages (p: [ p.flocq p.interval p.coquelicot ])",
+            build_file_content = _INTERVAL_ENV_BUILD_FILE,
+        )
+
         # Coquelicot - real analysis library, Coq-Interval's dependency (#37)
         nixpkgs_package(
             name = "rocq_coquelicot",

rocq/private/rocq.bzl

@@ -22,6 +22,7 @@ def _rocq_library_impl(ctx):
 
     Uses the Rocq toolchain from nixpkgs to compile proofs.
     """
+
     # Validate source files
     sources = ctx.files.srcs
     if not sources:
@@ -72,10 +73,12 @@ def _rocq_library_impl(ctx):
         # Get the relative path from the source file
         # E.g., "RocqOfRust/RocqOfRust.v" should become "RocqOfRust/RocqOfRust.vo"
         rel_path = src.short_path
+
         # Remove package prefix if present (for external sources)
         if rel_path.startswith("../"):
             # External source - extract relevant part after last known directory
             parts = rel_path.split("/")
+
             # Find the logical path component
             if logical_path in rel_path:
                 idx = rel_path.find(logical_path)
@@ -371,3 +374,92 @@ rocq_proof_test = rule(
     test = True,
     doc = "Verifies Rocq proof files compile successfully",
 )
+
+def _rocq_interval_proof_impl(ctx):
+    """Compile a .v file against the Coq-Interval environment (DD-003).
+
+    Coq-Interval's real dependency closure (mathcomp-boot/fingroup, bignums,
+    hierarchy-builder, the coq-elpi OCaml plugin) is resolved by a dedicated
+    coq_9_0.withPackages(...) environment (@rocq_interval_env) rather than by
+    the primary toolchain's hand-wired extra_libs -- see rules_rocq_rust#43.
+    That composed coqc already has its own default load path (Stdlib,
+    Flocq, Interval, Coquelicot, mathcomp, Bignums, HB, elpi), so no -Q
+    flags are needed here.
+    """
+    sources = ctx.files.srcs
+    if not sources:
+        fail("rocq_interval_proof requires at least one source file")
+    for src in sources:
+        if not src.path.endswith(".v"):
+            fail("rocq_interval_proof only accepts .v files, got: " + src.path)
+
+    coqc = ctx.executable._interval_coqc
+    env_files = ctx.files._interval_env_files
+
+    compiled_files = []
+    for src in sources:
+        vo_file = ctx.actions.declare_file(src.basename[:-len(".v")] + ".vo")
+        glob_file = ctx.actions.declare_file(src.basename[:-len(".v")] + ".glob")
+
+        args = ctx.actions.args()
+        args.add("-q")
+        for flag in ctx.attr.extra_flags:
+            args.add(flag)
+        args.add("-o", vo_file)
+        args.add(src)
+
+        ctx.actions.run(
+            executable = coqc,
+            arguments = [args],
+            # The composed coqc's own transitive closure (mathcomp, elpi's
+            # OCaml plugin, ...) lives at its own nix store paths outside
+            # this action's declared inputs; same rationale as rocq_library's
+            # extra_libs no-sandbox case -- hermeticity comes from nix's
+            # immutable store, not the Bazel sandbox, for this action.
+            inputs = [src] + env_files,
+            outputs = [vo_file, glob_file],
+            mnemonic = "CoqCompileInterval",
+            progress_message = "Compiling Coq-Interval proof %{input}",
+            execution_requirements = {"no-sandbox": "1"},
+        )
+        compiled_files.append(vo_file)
+
+    compiled_depset = depset(compiled_files)
+    return [
+        DefaultInfo(
+            files = compiled_depset,
+            runfiles = ctx.runfiles(files = sources + compiled_files),
+        ),
+        RocqInfo(
+            sources = depset(sources),
+            compiled = compiled_depset,
+            include_paths = [],
+            output_dir = "",
+            transitive_deps = depset(sources),
+        ),
+    ]
+
+rocq_interval_proof = rule(
+    implementation = _rocq_interval_proof_impl,
+    attrs = {
+        "srcs": attr.label_list(
+            allow_files = [".v"],
+            doc = "Rocq source files needing Coq-Interval (e.g. Require Import Interval.Tactic)",
+        ),
+        "extra_flags": attr.string_list(
+            doc = "Extra flags to pass to coqc",
+            default = [],
+        ),
+        "_interval_coqc": attr.label(
+            default = Label("@rocq_interval_env//:coqc"),
+            allow_single_file = True,
+            executable = True,
+            cfg = "exec",
+        ),
+        "_interval_env_files": attr.label(
+            default = Label("@rocq_interval_env//:user_contrib"),
+            allow_files = True,
+        ),
+    },
+    doc = "Compiles a Rocq proof using Coq-Interval's composed environment (DD-003); the target fails like any other Rocq proof if the kernel rejects it.",
+)