From b96fc4c6d07bda9a8898b4aeeee92f6d4723bd4f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 22 Jul 2026 16:30:26 +0200 Subject: [PATCH 1/2] feat(rocq): wire mathcomp into the toolchain (Coq-Interval dep) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Coq-Interval (added in #41) is present but UNUSABLE: `Require Import Interval.Tactic` fails with "Cannot load mathcomp.boot.seq: no physical path bound to mathcomp.boot" — Interval depends on Mathematical Components, which the toolchain does not expose on the coqc load path. This mirrors the Interval/Coquelicot wiring for mathcomp: a rocq_mathcomp nixpkgs_package (coqPackages.mathcomp), a filegroup BUILD, the toolchain `mathcomp` attr, and the extra_libs -Q binding (logical name `mathcomp`). NOT YET VALIDATED end-to-end: on a consumer (relay) with a pinned MODULE.bazel.lock, the module extension did not re-evaluate, so rocq_mathcomp was not materialised and the smoke proof still failed with the same error. Needs: (a) confirm `coqPackages.mathcomp` is the right nix attribute (modern mathcomp is split into boot/ssreflect/algebra — a meta vs component question), (b) confirm the `/mathcomp/` path pattern + lib/coq glob match the nix output layout, (c) a lock refresh so the extension re-runs. Filed so the approximation-layer FP proofs (relay MATHF32-P04/P05) can proceed once green. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- rocq/extensions.bzl | 24 ++++++++++++++++++++++++ rocq/toolchain.bzl | 10 ++++++++++ 2 files changed, 34 insertions(+) diff --git a/rocq/extensions.bzl b/rocq/extensions.bzl index e04bb03..77cff2e 100644 --- a/rocq/extensions.bzl +++ b/rocq/extensions.bzl @@ -105,6 +105,7 @@ rocq_toolchain_info( smpl_ocaml_plugins = "@rocq_smpl//:ocaml_plugins", flocq = "@rocq_flocq//:flocq", interval = "@rocq_interval//:interval", + mathcomp = "@rocq_mathcomp//:mathcomp", coquelicot = "@rocq_coquelicot//:coquelicot", gappalib = "@rocq_gappalib//:gappalib", ) @@ -236,6 +237,19 @@ filegroup( ) ''' +# BUILD file for Mathematical Components (Coq-Interval's dependency) +_MATHCOMP_BUILD_FILE = ''' +package(default_visibility = ["//visibility:public"]) + +filegroup( + name = "mathcomp", + srcs = glob([ + "lib/coq/**/*.vo", + "lib/coq/**/*.glob", + ], allow_empty = True), +) +''' + # BUILD file for Coquelicot (real analysis library, Coq-Interval's dependency) _COQUELICOT_BUILD_FILE = ''' package(default_visibility = ["//visibility:public"]) @@ -391,6 +405,16 @@ import (builtins.fetchTarball {{ build_file_content = _INTERVAL_BUILD_FILE, ) + # Mathematical Components - Coq-Interval's runtime dependency; without + # its .vo on the load path `Require Import Interval.Tactic` fails with + # "Cannot load mathcomp.boot.seq". (relay#... FP approximation track) + nixpkgs_package( + name = "rocq_mathcomp", + repository = nixpkgs_repo, + attribute_path = "coqPackages.mathcomp", + build_file_content = _MATHCOMP_BUILD_FILE, + ) + # Coquelicot - real analysis library, Coq-Interval's dependency (#37) nixpkgs_package( name = "rocq_coquelicot", diff --git a/rocq/toolchain.bzl b/rocq/toolchain.bzl index be814ab..2ebb09e 100644 --- a/rocq/toolchain.bzl +++ b/rocq/toolchain.bzl @@ -79,6 +79,12 @@ def _rocq_toolchain_info_impl(ctx): if path: extra_libs.append((ctx.files.interval, "Interval", path)) + # Mathematical Components - Coq-Interval's dependency (mathcomp.boot / .ssreflect). + if ctx.files.mathcomp: + path = _find_lib_path(ctx.files.mathcomp, "/mathcomp/", "mathcomp") + if path: + extra_libs.append((ctx.files.mathcomp, "mathcomp", path)) + # Coquelicot - real analysis library (Coq-Interval's dependency) if ctx.files.coquelicot: path = _find_lib_path(ctx.files.coquelicot, "/Coquelicot/", "Coquelicot") @@ -186,6 +192,10 @@ rocq_toolchain_info = rule( allow_files = True, doc = "Coq-Interval library .vo files (optional)", ), + "mathcomp": attr.label( + allow_files = True, + doc = "Mathematical Components library .vo files (Coq-Interval dep; optional)", + ), "coquelicot": attr.label( allow_files = True, doc = "Coquelicot library .vo files (optional)", From 4d47001290037731d55339a4eeaf947c271a0ee4 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 22 Jul 2026 19:35:31 +0200 Subject: [PATCH 2/2] fix(rocq): make Coq-Interval actually usable via coq_9_0.withPackages (DD-003) Replaces the previous commit's coqPackages.mathcomp wiring, which doesn't fix the bug: `nix build coqPackages.mathcomp` produces only a 1-file umbrella re-export (lib/coq/9.0/user-contrib/mathcomp/all/all.vo), not the mathcomp-boot package the original error names ("Cannot load mathcomp.boot.seq"). The real dependency closure, read off nixpkgs directly (not guessed): `coqPackages.interval.propagatedBuildInputs` = bignums, coquelicot, flocq, mathcomp-boot, mathcomp-fingroup. mathcomp-boot itself needs hierarchy-builder, which needs the coq-elpi OCaml plugin, whose own OCaml findlib deps (ppx_deriving.runtime, ...) go deeper still -- hand-wiring each as a separate nixpkgs_package + -Q flag doesn't scale past this point. - rocq/extensions.bzl: @rocq_interval_env is a single `coq_9_0.withPackages (p: [p.flocq p.interval p.coquelicot])` composition that resolves the entire transitive closure automatically (mathcomp-boot/fingroup, bignums, hierarchy-builder, coq-elpi and its OCaml deps) -- exactly the way nixpkgs is designed to solve this. Its own subdirs are already named Flocq/Interval/mathcomp/Bignums/HB/elpi, so exposing the tree needs no manual -Q reconstruction at all. - rocq/private/rocq.bzl: new rocq_interval_proof rule compiles against this dedicated environment's own coqc (no -Q flags needed -- it has its own default load path baked in). The primary toolchain (coqutil/Hammer/smpl, rocq-of-rust) is untouched. - examples/interval_proof/: a real smoke test -- Require Import Interval.Tactic, `interval` tactic discharges a goal. Verified: `bazel test //examples/interval_proof:smoke_test` -- PASSED. Nothing exercised this before (#41/#43 both went green on CI without proving the capability worked). - artifacts/requirements.yaml: FEAT-001/REQ-002 back to implemented (genuinely this time); DD-003 records the verified decision and why hand-wiring the closure was rejected. - README.md / claims.yaml: document the new capability and gate the claim the same way as the rest of this repo's doc claims. Closes #43 Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_011MptgyfLZuHYCbfpq1zDey --- MODULE.bazel | 7 ++- README.md | 9 ++- artifacts/requirements.yaml | 73 +++++++++++++++++++++-- claims.yaml | 21 +++++++ examples/interval_proof/BUILD.bazel | 16 +++++ examples/interval_proof/smoke.v | 11 ++++ rocq/defs.bzl | 3 +- rocq/extensions.bzl | 46 +++++++++++---- rocq/private/rocq.bzl | 92 +++++++++++++++++++++++++++++ rocq/toolchain.bzl | 10 ---- 10 files changed, 257 insertions(+), 31 deletions(-) create mode 100644 examples/interval_proof/BUILD.bazel create mode 100644 examples/interval_proof/smoke.v diff --git a/MODULE.bazel b/MODULE.bazel index de613b8..c98f8e8 100644 --- a/MODULE.bazel +++ b/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") diff --git a/README.md b/README.md index 6c89a29..5e96a7b 100644 --- a/README.md +++ b/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). diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index fa8c173..720a736 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -118,6 +118,61 @@ 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) @@ -125,18 +180,28 @@ artifacts: 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 diff --git a/claims.yaml b/claims.yaml index ecf98f4..5642c59 100644 --- a/claims.yaml +++ b/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 diff --git a/examples/interval_proof/BUILD.bazel b/examples/interval_proof/BUILD.bazel new file mode 100644 index 0000000..381196f --- /dev/null +++ b/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"], +) diff --git a/examples/interval_proof/smoke.v b/examples/interval_proof/smoke.v new file mode 100644 index 0000000..394ee5a --- /dev/null +++ b/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. diff --git a/rocq/defs.bzl b/rocq/defs.bzl index 6ed2982..20227a6 100644 --- a/rocq/defs.bzl +++ b/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. diff --git a/rocq/extensions.bzl b/rocq/extensions.bzl index 77cff2e..d4682fa 100644 --- a/rocq/extensions.bzl +++ b/rocq/extensions.bzl @@ -105,7 +105,6 @@ rocq_toolchain_info( smpl_ocaml_plugins = "@rocq_smpl//:ocaml_plugins", flocq = "@rocq_flocq//:flocq", interval = "@rocq_interval//:interval", - mathcomp = "@rocq_mathcomp//:mathcomp", coquelicot = "@rocq_coquelicot//:coquelicot", gappalib = "@rocq_gappalib//:gappalib", ) @@ -225,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"]) @@ -237,12 +242,12 @@ filegroup( ) ''' -# BUILD file for Mathematical Components (Coq-Interval's dependency) -_MATHCOMP_BUILD_FILE = ''' +# BUILD file for Coquelicot (real analysis library, Coq-Interval's dependency) +_COQUELICOT_BUILD_FILE = ''' package(default_visibility = ["//visibility:public"]) filegroup( - name = "mathcomp", + name = "coquelicot", srcs = glob([ "lib/coq/**/*.vo", "lib/coq/**/*.glob", @@ -250,12 +255,25 @@ filegroup( ) ''' -# BUILD file for Coquelicot (real analysis library, Coq-Interval's dependency) -_COQUELICOT_BUILD_FILE = ''' +# 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 = "coquelicot", + name = "coqc", + srcs = ["bin/coqc"], +) + +filegroup( + name = "user_contrib", srcs = glob([ "lib/coq/**/*.vo", "lib/coq/**/*.glob", @@ -405,14 +423,16 @@ import (builtins.fetchTarball {{ build_file_content = _INTERVAL_BUILD_FILE, ) - # Mathematical Components - Coq-Interval's runtime dependency; without - # its .vo on the load path `Require Import Interval.Tactic` fails with - # "Cannot load mathcomp.boot.seq". (relay#... FP approximation track) + # 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_mathcomp", + name = "rocq_interval_env", repository = nixpkgs_repo, - attribute_path = "coqPackages.mathcomp", - build_file_content = _MATHCOMP_BUILD_FILE, + nix_file_content = "(import { 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) diff --git a/rocq/private/rocq.bzl b/rocq/private/rocq.bzl index 64a50c4..c0c1fff 100644 --- a/rocq/private/rocq.bzl +++ b/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.", +) diff --git a/rocq/toolchain.bzl b/rocq/toolchain.bzl index 2ebb09e..be814ab 100644 --- a/rocq/toolchain.bzl +++ b/rocq/toolchain.bzl @@ -79,12 +79,6 @@ def _rocq_toolchain_info_impl(ctx): if path: extra_libs.append((ctx.files.interval, "Interval", path)) - # Mathematical Components - Coq-Interval's dependency (mathcomp.boot / .ssreflect). - if ctx.files.mathcomp: - path = _find_lib_path(ctx.files.mathcomp, "/mathcomp/", "mathcomp") - if path: - extra_libs.append((ctx.files.mathcomp, "mathcomp", path)) - # Coquelicot - real analysis library (Coq-Interval's dependency) if ctx.files.coquelicot: path = _find_lib_path(ctx.files.coquelicot, "/Coquelicot/", "Coquelicot") @@ -192,10 +186,6 @@ rocq_toolchain_info = rule( allow_files = True, doc = "Coq-Interval library .vo files (optional)", ), - "mathcomp": attr.label( - allow_files = True, - doc = "Mathematical Components library .vo files (Coq-Interval dep; optional)", - ), "coquelicot": attr.label( allow_files = True, doc = "Coquelicot library .vo files (optional)",