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

[avrabe]

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 blocks the FP approximation-layer proofs (relay MATHF32-P04/P05).

Mirrors the Interval/Coquelicot wiring for mathcomp (rocq_mathcomp nixpkgs_package + filegroup + toolchain attr + extra_libs -Q binding).

NOT YET VALIDATED end-to-end — on a consumer with a pinned lock the extension didn't re-evaluate (rocq_mathcomp not materialised, same error). Open: (1) is coqPackages.mathcomp the right attr (modern mathcomp splits into boot/ssreflect/algebra)? (2) do the path pattern + glob match the nix layout? (3) lock refresh needed. Filed as the prerequisite for the approximation-layer proof track.

🤖 Generated with Claude Code

[avrabe]

Verified this empirically before merging (per the operating discipline: reproduce, don't trust a done-flag). Recommend not merging as-is — the diagnosis is right (Coq-Interval genuinely can't load without mathcomp), but this specific fix doesn't resolve it, and the gap is deeper than one missing package.

coqPackages.mathcomp is the wrong attribute. Built it and checked:

$ nix build --expr '(import nixpkgs {}).coqPackages.mathcomp'
→ only lib/coq/9.0/user-contrib/mathcomp/all/all.vo  (1 file — an umbrella re-export)

It does not contain mathcomp/boot/seq.vo — the exact module the original error names. mathcomp.boot.seq lives in the separate coqPackages.mathcomp-boot derivation; modern mathcomp splits into ~20 sub-packages (boot, ssreflect, fingroup, algebra, ...), and mathcomp alone is just a thin re-export shell. Wiring attribute_path = "coqPackages.mathcomp" as this PR does would still fail with the identical error post-merge.

The real dependency list, read directly off nixpkgs (not guessed):

$ nix eval '(import nixpkgs {}).coqPackages.interval.propagatedBuildInputs'
→ bignums, coquelicot, flocq, mathcomp-boot, mathcomp-fingroup, gnuplot

So this is also missing bignums entirely (not wired in #41 either — my miss, not just this PR's).

And it goes one level deeper still. mathcomp-boot itself needs hierarchy-builder (HB), and HB needs coq-elpi — which is a real OCaml plugin (findlib META + .cmxs), not a plain .v library. A smoke test (Require Import Interval.Tactic. Goal (1+1<=3)%R. Proof. interval. Qed.) compiled against every individual package I could enumerate manually still failed on Findlib error: ppx_deriving.runtime not found — the OCaml findlib closure for elpi keeps going, the same category of complexity this repo already had to solve once for Hammer.

What actually works, verified:

nix build --expr '(import nixpkgs {}).coq_9_0.withPackages (p: [p.flocq p.interval p.coquelicot])'

Using that environment's coqc directly on the smoke test above: exit 0, .vo produced, no manual -Q list, no findlib chasing — withPackages has nixpkgs resolve the entire transitive closure (mathcomp-boot/fingroup, bignums, hierarchy-builder, coq-elpi, and elpi's own OCaml deps) the way it's designed to. Confirmed the .vo load path is also reconstructible via a single -Q <that-tree>/lib/coq/9.0/user-contrib "" (the subdirs are already named Flocq/Interval/mathcomp/Bignums/HB/elpi etc., so the empty logical root just works) — but the OCaml plugin/findlib side only resolves through the withPackages-produced coqc binary itself (it has the OCaml env baked in at the binary level, not something I could reproduce by hand as an env var).

Recommendation: the real fix is architectural, not a quick patch — either (a) a second, withPackages-composed coqc scoped to the approximation-layer packages, since rocq_toolchain_info currently assumes one coqc for everything, or (b) unify the whole toolchain (coqutil/Hammer/smpl included) onto coq_9_0.withPackages(...), which would also simplify away the hand-rolled Hammer OCAMLPATH wiring — bigger, but more maintainable long-term. Also worth adding a CI target that actually exercises Interval.Tactic once this lands, since nothing currently does (this PR's own CI went green without proving anything about the bug it claims to fix). Happy to scope the real fix as a follow-up rather than block on it here.

🤖 Generated with Claude Code