fix(rivet): correct FEAT-001 -- Coq-Interval is not actually usable

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 <tree>/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