From 222d720cecbaf5ac2722a0ae107cae8ecc75075e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 22 Jul 2026 19:14:28 +0200 Subject: [PATCH] fix(rivet): correct FEAT-001 -- Coq-Interval is not actually usable PR #43 reported (and I independently reproduced/deepened) that Require Import Interval.Tactic fails: #41 fetched coqPackages.interval but never wired its real dependency closure (bignums, mathcomp-boot, mathcomp-fingroup, and transitively hierarchy-builder + the coq-elpi OCaml plugin). FEAT-001 and REQ-002 previously claimed this was done; demoting both back to draft/approved until it's genuinely fixed and covered by a CI target that exercises Interval.Tactic, not just fetches the package. Adds DD-003: the verified fix is coq_9_0.withPackages(...), which resolves the whole transitive closure (confirmed: its coqc compiles a Require Import Interval.Tactic smoke proof cleanly, which no amount of manual nixpkgs_package + -Q wiring reached). Left as a draft design decision for the follow-up PR, not implemented here. Refs #43 Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_011MptgyfLZuHYCbfpq1zDey --- artifacts/requirements.yaml | 77 +++++++++++++++++++++++++++++++++---- 1 file changed, 70 insertions(+), 7 deletions(-) diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index fa8c173..6828db9 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -19,7 +19,7 @@ artifacts: - id: REQ-002 type: requirement title: The toolchain shall support machine-checked floating-point error-bound proofs, kernel-replaying every Gappa certificate - status: implemented + status: approved priority: must description: > Add Flocq (fp model), the `gappa` binary (rounding-error layer), @@ -118,22 +118,85 @@ 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: draft + description: > + Proposed fix for the Coq-Interval usability gap (the approximation-layer + feature, PR #43). Not yet implemented -- a design decision awaiting a + follow-up PR. + 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: PR #43 tried the next package in the chain and still + didn't reach a working state after enumerating 5 packages by hand. + `coq_9_0.withPackages (p: [p.flocq p.interval p.coquelicot])` resolves + the *entire* transitive closure automatically -- verified: its coqc + compiles `Require Import Interval.Tactic. Goal (1+1<=3)%R. Proof. + interval. Qed.` cleanly (exit 0), including the coq-elpi OCaml plugin + load, which no manual -Q/OCAMLPATH assembly reached. Two ways to land + it: (a) a second, withPackages-composed coqc scoped to the + approximation-layer packages only (rocq_toolchain_info currently + assumes one coqc for every compile), or (b) unify the whole toolchain + (coqutil/Hammer/smpl included) onto withPackages, which would also + retire the hand-rolled Hammer OCAMLPATH/ocaml_plugins wiring. + 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 PR #43 repeated (wrong mathcomp attribute, + still missing bignums/HB/elpi). Verified empirically, not assumed: + the .vo load path is also just a single `-Q /user-contrib ""` + once the subdirs are already named Flocq/Interval/mathcomp/etc. + 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), and every new + approximation-layer dependency added later would repeat this same + multi-hour chase. + source-ref: "pulseengine/rules_rocq_rust#43 (review comment), #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 + status: draft 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) is implemented and verified via `bazel + test //examples/gappa_proof:rounding_bound_test` -- exercises the full + chain (a `.gappa` rounding-bound statement, Gappa's `-Bcoq` codegen, a + real Rocq kernel check of the emitted proof term against + gappalib-coq/Flocq) -- PASSED. + + Approximation layer (Coq-Interval) is NOT usable yet, despite #41 + fetching the package: `Require Import Interval.Tactic` fails (Coq-Interval + needs mathcomp-boot/mathcomp-fingroup + bignums + hierarchy-builder + + the coq-elpi OCaml plugin, none of which #41 wired in -- caught by + PR #43's own report and independently re-verified against nixpkgs + `propagatedBuildInputs`, see PR #43 review comment). Demoted back to + draft until this is genuinely fixed and covered by a CI target that + exercises `Interval.Tactic` -- not just fetches the package. 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)" + - "Toolchain flake provides flocq, gappa (binary), gappalib-coq, 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) -- NOT DONE; needs mathcomp-boot/fingroup + bignums + hierarchy-builder + coq-elpi OCaml plugin wiring, verified working via coq_9_0.withPackages but not yet wired into Bazel (see PR #43)" - "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