extra-dev: add 46 dev recipes and update 5 more, for packages that do not yet install (on top of #3809)

[JasonGross]

Stacked on #3809 — merge that one first.

#3809 keeps the 45 recipes whose packages install; this PR carries the 43 that do not. Its diff also includes #3809 because several recipes here depend on recipes there, including coq-mathcomp-cad on the mathcomp-analysis family, rocq-sims on coq-ctree, and rocq-marble on rocq-listz.

These red .dev recipes are useful because most affected packages have a live release capped below Rocq master. Without a recipe tracking the default branch, breakage is not found until someone attempts a release against 9.3. The recipes identify the first failure for each package on every archive run.

The results are a lower bound: a compiler stops at the first error, and only 14 of these 43 packages have had their own sources compiled. The other 29 stopped in a dependency or sibling first. A source census for one known 9.3 break found 183 sites in 10 repositories behind these recipes, but only one repository reports that break as its first error. Seven of the other nine are behind elpi, interval, finmap, or deriving blockers; one is behind an earlier error in its own package; and one is in a green package behind a depopts: gate that CI never enables.

Failure ledger

The driver records what changed, rather than merely where the error surfaced. For Rocq-driven rows, Rocq version is the first tag containing the responsible commit (git tag --contains <sha> | sort -V | head -1). visible-now means the reported error is in the package's own sources; latent means its sources have not been measured because a dependency or sibling failed first. A blocked row therefore remains unknown (blocked) rather than inheriting its blocker's driver.

package	driver	Rocq version	visibility
coq-vst-lib	unknown (blocked)	—	latent — stops at rocq-elpi
rocq-categories	unknown (blocked)	—	latent — stops at rocq-elpi; 1 of site unreached
rocq-elpi-json	unknown (blocked)	—	latent — stops at rocq-elpi
rocq-elpi-xml	unknown (blocked)	—	latent — stops at rocq-elpi
rocq-navi	unknown (blocked)	—	latent — stops at rocq-elpi; 4 of sites, all in examples/ behind {with-test}
rocq-partial-orders	unknown (blocked)	—	latent — stops at rocq-elpi; 147 of sites unreached
coq-infotheo	unknown (blocked)	—	latent — stops at coq-interval; 20 of sites unreached
rocq-infotheo	unknown (blocked)	—	latent — stops at coq-interval; the same 20 sites
rocq-laproof	unknown (blocked)	—	latent — stops at coq-interval
rocq-num-analysis ‡	unknown (blocked)	—	latent — stops at rocq-mathcomp-finite-group, and capped at < 9.2~
rocq-num-analysis-algebra ‡	unknown (blocked)	—	latent — same
rocq-num-analysis-fem ‡	unknown (blocked)	—	latent — same
rocq-num-analysis-lax-milgram ‡	unknown (blocked)	—	latent — same
rocq-num-analysis-lebesgue ‡	unknown (blocked)	—	latent — same
rocq-num-analysis-subset ‡	unknown (blocked)	—	latent — same
coq-mathcomp-cad	unknown (blocked)	—	latent — stops at rocq-mathcomp-finmap; 2 of sites unreached
rocq-rouche-capelli §	unknown (blocked)	—	latent — stops at rocq-mathcomp-finmap; latent content since measured: 1 of site and a goal-order break behind it
coq-ssprove	unknown (blocked)	—	latent — stops at coq-deriving; 2 of sites unreached
rocq-ssprove	unknown (blocked)	—	latent — stops at coq-deriving; the same 2 sites
rocq-hollight-logic	unknown (blocked)	—	latent — stops at coq-mathcomp-classical
rocq-hollight-logic-unif	unknown (blocked)	—	latent — stops at coq-mathcomp-classical
coq-coinduction	inherited — shim	see rocq-coinduction	n/a — no sources of its own
coq-color	inherited — shim	see rocq-color	n/a — no sources of its own
coq-trocq-hott-examples	unknown (blocked)	—	latent — stops at coq-trocq-hott
coq-trocq-std-examples	unknown (blocked)	—	latent — stops at coq-trocq-std
rocq-concert-examples	unknown (blocked)	—	latent — stops at rocq-concert
rocq-sims	unknown (blocked)	—	latent — stops at coq-ctree, and after the rename at rocq-ctree
rocq-typed-extraction	none found	—	was unsatisfiable, so latent in CI; built clean locally against 9.4+alpha, 13/13 .v
rocq-typed-extraction-plugin	Rocq	V9.3+rc1 — #21955, ba476414d4	was unsatisfiable; fix verified locally by building past it
coq-pprint	toolchain	— (dune 3.24)	visible-now
coq-sflib	toolchain	— (dune 3.24)	visible-now
rocq-ceres-bytestring	toolchain	— (dune 3.24)	visible-now
coq-ctree → rocq-ctree	packaging	—	visible-now — renamed in this PR; three further drivers sit behind the rename, none reached
coq-hol-light	dependency	—	visible-now
rocq-concert	dependency	— (plan resolved rocq-core 9.1.dev)	visible-now
rocq-mathcomp-hollight-real-with-N	Rocq	V9.3+rc1 — #21611, e6a2fb9b2f	visible-now — the only of break the archive has actually seen
rocq-robot-rocq	dependency	— (mathcomp 2.6)	visible-now — 1 of site still latent behind angle.v:126
coq-trocq-hott	Rocq (presumed) — no PR identified	undetermined	visible-now
coq-trocq-std	Rocq	V9.3+rc1 — #21947, 1fc7ef04ed	visible-now
rocq-marble †	Rocq + dependency	V9.3+rc1 — #21987, eebacb3bb1 — Rocq half only	visible-now
rocq-coinduction	recipe	n/a (recipe)	visible-now (4.09.0 only) — fixed in this PR
rocq-color	recipe	n/a (recipe)	visible-now (4.09.0 only) — fixed in this PR
coq-vcfloat	recipe	n/a (recipe)	visible-now (4.09.0 only) — not fixed; see below

† rocq-marble has two independent drivers. The version covers only its Rocq driver.

§ rocq-rouche-capelli was built past its blocker locally. It has two independent breaks: the of site and a rewrite goal-order break that appears only after fixing of. Other latent rows remain unmeasured.

‡ Five of the six rocq-num-analysis* recipes cap rocq-core at < "9.2~"; the sixth inherits that through {= version}. Clearing their blocker still would not put them on master.

Blocked and unsatisfiable packages

Twenty-one packages never reached their own build. Their blockers were:

blocker	fails at	blocker's driver	blocker's version	packages it hides
rocq-elpi.3.4.0 — dune-project says (using coq 0.8), deleted in dune 3.24	dune build -p rocq-elpi	toolchain	dune 3.24	coq-vst-lib, rocq-categories, rocq-elpi-json, rocq-elpi-xml, rocq-navi, rocq-partial-orders
coq-interval.dev † — ocamlfind: Package 'coq-core.engine' not found	./configure	Rocq, twice	V9.3+rc1 — #21955 ba476414d4; 9b1424650d (also V9.3+rc1) is the second driver behind it	coq-infotheo, rocq-infotheo, rocq-laproof
rocq-mathcomp-finite-group.dev — morphism.v:3, Required library ssreflect matches several files in path	make -C finite_group	packaging	mathcomp 2.5.0 (#1415)	the six rocq-num-analysis* packages
rocq-mathcomp-finmap.dev — finperm.v:160, The reference index_inj was not found	make -j2	dependency	mathcomp 2.5.0 (#1430)	coq-mathcomp-cad, rocq-rouche-capelli
coq-deriving.0.2.3 — theories/base.v:3, same matches several files	make	packaging	mathcomp 2.5.0 (#1415)	coq-ssprove, rocq-ssprove
coq-mathcomp-classical.1.15.0	make -C classical	undetermined	undetermined	rocq-hollight-logic, rocq-hollight-logic-unif

rocq-elpi.3.4.0, coq-deriving.0.2.3, and coq-mathcomp-classical.1.15.0 are released packages from the main archive, so this PR cannot fix them.

The mathcomp 2.5.0 split of mathcomp-ssreflect into mathcomp-boot and mathcomp-order (math-comp#1415) permits old and new layouts to be co-installed. For example:

rocq-num-analysis-algebra.dev:  rocq-mathcomp-boot dev  +  rocq-mathcomp-ssreflect 2.4.0
coq-ssprove.dev:                rocq-mathcomp-boot dev  +  coq-mathcomp-ssreflect  2.3.0

This makes Require ssreflect ambiguous. rocq-mathcomp-finite-group.dev itself is not broken: math-comp d5507be, finite_group/ built against a dev stack, 10/10 .v → .vo, with no source changes. A conflicts: on rocq-mathcomp-boot against {coq,rocq}-mathcomp-ssreflect {< "2.5~"} would turn these into solver errors, but the six rocq-num-analysis* packages behind it would remain capped below master and unmeasured.

rocq-mathcomp-finmap.dev also permits ("coq-mathcomp-ssreflect" {>= "2.2" & < "2.4~"} | "rocq-mathcomp-ssreflect" {>= "2.4"}); under coq-mathcomp-cad.dev, the solver chose coq-mathcomp-ssreflect 2.2.0. Its source uses index_inj, absent at 2.4.0 and present at 2.5.0 (boot/seq.v:1453) and dev (boot/seq.v:1484). Raising the floor to 2.5.0 clears this error, but the result was not built and may reveal another.

coq-mathcomp-classical.1.15.0 could not be attributed because the trace omits the failing line. Its plan includes rocq-core dev, while coq-mathcomp-classical.dev and rocq-mathcomp-classical.dev both pass on the same job, so the two blocked packages need a version-bound change rather than a source port. The later Hollight commits move the relevant constraint to coq-mathcomp-ssreflect.

Six more packages are blocked by recipes in this PR: coq-coinduction, coq-color, coq-trocq-hott-examples, coq-trocq-std-examples, rocq-concert-examples, and rocq-sims.

rocq-typed-extraction.dev and rocq-typed-extraction-plugin.dev were unsatisfiable because they require rocq-elm-extraction {= version} and rocq-rust-extraction {= version}, but neither dependency had a .dev recipe:

[ERROR] Package conflict!
  * Missing dependency:
    - rocq-elm-extraction >= dev
    no matching version

The final commit adds both missing recipes. This turns an unsatisfiable dependency into an ordinary build result; it does not make the whole stack green.

Packages that reached their own build

package	first error
coq-pprint	dune-project:3 (using coq 0.8) — dune 3.24 deleted the Coq Build Language
coq-sflib	dune-project:4 (using coq 0.8) — same
rocq-ceres-bytestring	dune-project:2 (using coq 0.2) — same
coq-ctree	I don't know about package coq-ctree (passed through --only-packages) / Hint: did you mean rocq-ctree?
coq-hol-light	mappings.v — Unable to unify "forall x : ?A, ?f x = ?g x" with ...
rocq-concert	execution/test/TestUtils.v:175 — No derive declared for Show, against rocq-core 9.1.dev
rocq-mathcomp-hollight-real-with-N	type.v:24 — Usage: HB.builders Context A (f : F1 A).
rocq-robot-rocq	angle.v:126 — The LHS of ltcR (_%:C%C < _%:C%C) does not match any subterm of the goal
coq-trocq-hott	hott/Param_lemmas.v — The LHS of equiv_invK (_ (_^-1%equiv _)) does not match any subterm of the goal
coq-trocq-std	generic/Param_vector.v:38 — The constructor cons (in type t) is expected to be applied to 2 arguments while it is actually applied to 3 arguments
rocq-marble	fails at dune build -p rocq-marble; CI output is truncated
rocq-coinduction	4.09.0 only — theories/lattice.v:40, Syntax error: illegal begin of vernac
rocq-color	4.09.0 only — Util/Logic/EpsilonUtil.v:16, same error
coq-vcfloat	4.09.0 only — IEEE754_extra.v:434, The reference eq_IZR_contrapositive was not found in the current environment

The first three failures occur before any .v is read: dune 3.24 removed (using coq X.Y) and requires (using rocq 0.11) with (lang dune 3.21) or later.

The remaining driver evidence is package-specific:

• coq-ctree is a package rename, not a source port. Its new recipe preserves upstream's dune {>= "3.8" & < "3.24"}, which avoids the deleted (using coq 0.7) extension without migrating it. The expected next result is therefore a different red rather than a green.

• rocq-mathcomp-hollight-real-with-N uses HB.builders Context T of HOL_isPointed T.. HB's a12d7cc57 adaptation to #21611 changes no grammar, confirming that the syntax came from Rocq's parser rather than HB.

• rocq-robot-rocq's pinned source has angle.v:126 as rewrite normrM gtr0_norm; last by rewrite ltcR.; at 4e8bedb43 this becomes a single by rewrite normrM gtr0_norm ?ltcR// …. Its new floors are HB 1.10.0, mathcomp 2.6.0, analysis 1.17.0, and real-closed 2.0.6.

• rocq-coinduction uses Abbreviation 34 times and rocq-color 675 times. The 9.0 parser failure is not fixed by changing those sources; pinning rocq-core {= "dev"} causes the 4.09 job to skip them, while both already pass on 4.14.2 and 5.3.0.

vellvm/ctrees 29a153df8 renamed (name coq-ctree) to (name rocq-ctree). This PR adds rocq-ctree.dev from upstream's in-tree opam and reduces coq-ctree.dev to depends: [ "rocq-ctree" {= version} ]. This clears the package-name failure but leaves three unreached issues: (using coq 0.7), intuition auto with * (#21129), and _ ° → _ ^° from relation-algebra 1.9.0. rocq-sims therefore remains blocked.

rocq-concert is dependency-driven. QuickChick removed bare Derive after v2.1.1 in favor of QCDerive; v2.2.0 is the first release without it, and CI selected coq-quickchick.dev = v2.2.0-1-g3d4d6c0. ConCert also needs the now-nullary MetaRocq universes_entry constructor. With those two source fixes and a fully-dev dependency stack, dune build @all passes for 188/189 .v, and the two opam packages install with 72 and 116 .vo. examples/AllTests.v is not built because it has no examples/dune, matching upstream. examples/dexter2/extract/ExtractCPMMLIGO.v:19 requires ulimit -s unlimited; with the default ulimit -s 8192 it fails with Error: Stack overflow.

rocq-mathcomp-hollight-real-with-N is broken by #21611, which reserves of; type.v:24 contains HB.builders Context T of HOL_isPointed T.. The responsible commit is first tagged V9.3+rc1.

rocq-robot-rocq was tested outside upstream's declared support: its pinned cf7add1cb declares "coq" { (>= "9.0" & < "9.2~") } and coq-mathcomp-ssreflect {>= "2.5.0"}, while this run used mathcomp 2.6. Upstream later adapted in d08cd27fc and 4e8bedb43; the archive also lacks a .dev recipe satisfying its new rocq-mathcomp-analysis 1.17.0 floor.

coq-trocq-hott is attributed to Rocq based on upstream's ## Trocq is broken on Rocq-master configuration and its 9.0/9.1-only CI, but no responsible PR or version was identified. Two minimal probes produced byte-identical goals under 9.1, 9.2, and dev, so the ledger leaves its version undetermined.

coq-trocq-std was reproduced locally at a36529e66 against Rocq dev:

File "./generic/Param_vector.v", line 38, characters 6-16:
Error: The constructor cons (in type t) is expected to be applied to
2 arguments while it is actually applied to 3 arguments.

#21947 changed asymmetric patterns so they no longer suppress implicit arguments. Five @-patterns fix the shared generic/ code. coq-trocq-hott and coq-trocq-std also install 36 identically named .vo files under Trocq without declaring a conflict. This PR does not add conflicts: because the isolated archive jobs cannot expose the overlap.

rocq-marble has independent dependency and Rocq failures. theories/traverse.v:217, The variable list_elem_of_init was not found, reflects a mismatch between marble HEAD and listz 597ad1e6; no 9.2 build was run, so that attribution is structural rather than measured. theories/pqueue.v:765, wp_move_up depends on the section variable H2 but H2 in the current context does not refer to the section variable of the same name, is caused by #21987, first tagged V9.3+rc1.

The dependency mismatch is also visible in marble's history: f378d8a (Remove listz_buffer. (Now depending on an up-to-date listz.)) precedes 7563cc8 (New file listz_buffer.v.), leaving marble HEAD dependent on a listz change newer than listz HEAD. The Rocq half comes from the proof engine tracking section-variable status after d52593d7e8; listz's tactic reverts and reintroduces variables, yielding a convertible variable that no longer carries the original marker.

coq-hol-light is dependency-driven by Deducteam/coq-hol-light-real-with-N 95e5c1050 (2025-08-01), 18 commits after tag 2.0.0 at fce5a880… (2025-07-11). Its change to align_ε leaves P a as a premise, and the failure appears downstream in coq-hol-light's mappings.v.

All identified Rocq changes driving rows are first tagged V9.3+rc1. There is no V9.3.0; the latest final release is V9.2.0. These are therefore committed 9.3 release-stream breaks rather than speculative master churn. coq-trocq-hott is excluded from that claim because its responsible change remains unidentified.

Packages not tested against master

Resolved versions from each per-package section show that 14 of the 43 never had Rocq master in their install plan on any compiler:

resolved rocq-core	packages	where the cap is written
9.1.dev on all three jobs	the six rocq-num-analysis*	their own depends:
9.1.dev on all three jobs	rocq-concert, rocq-concert-examples, rocq-rouche-capelli	a sibling's
9.0.dev on all three	coq-ssprove, rocq-ssprove	a sibling's
8.20.dev on all three	coq-ctree, rocq-sims	a sibling's
8.18.dev / 8.20.dev	coq-mathcomp-cad	a sibling's

Five rocq-num-analysis* recipes directly use:

(("coq-core" {>= "8.20" & < "8.21~"} & "coq-stdlib") |
  ("rocq-core" {>= "9.0" & < "9.2~"} & "rocq-stdlib"))

The sixth inherits the cap through {= version} dependencies. Their state is not evidence about master and cannot become evidence until the cap changes.

rocq-concert instead has rocq-core {>= "9.1"} but was dragged to 9.1 by four sibling constraints, all removed by the last commit:

"rocq-metarocq-erasure" {>= "1.5.1" & < "1.6~"}
"rocq-rust-extraction"  {= "0.2.1"}
"rocq-elm-extraction"   {= "0.2.1"}
"rocq-stdpp"            {= "1.13.0"}

The typed-extraction chain was built from eaf194e5 against rocq --version 9.4+alpha: common, elm, and rust pass unchanged, 13/13 .v → .vo. git diff v0.2.1..eaf194e5 -- '*/theories' '*/src' '*.opam' is empty, so the released 0.2.1 sources are covered. The plugin then fails at ocamlfind: Package 'coq-core.plugins.extraction' not found; changing it to rocq-runtime.plugins.extraction builds through .cmxs and Loader.v.

rocq-rouche-capelli.dev has the same sideways-cap pattern: it declares rocq-core {>= "9.0.0"} without a ceiling, but five rocq-mathcomp-* {= "2.4.0"} pins and coq-mathcomp-classical {= "1.13.0"} pull the plan to 9.1. Its released 0.2.0 recipe does have rocq-core {>= "9.0.0" & < "9.1~"}, but that is not the .dev constraint responsible for this run.

Relaxing rocq-{rust,elm}-extraction {= "0.2.1"} to {>= "0.2.1"} is a forward allowance: the build used sources byte-identical to v0.2.1, so it shows that 0.2.1 need not be the ceiling, not that every future version works. The relaxation and the new .dev recipes are both required; either alone still resolves the old chain.

The coq-core findlib rename

Commit ba476414d4 (#21955) removed the compatibility coq-core.* findlib packages except coq-core.kernel. Counting ^package in lib/coq-core/META gives 24 subpackages on 9.1 and 9.2, but only kernel on dev. The commit is first tagged V9.3+rc1.

The replacement is rocq-runtime.*, available since V9.0+rc1. It affects two rows here:

• rocq-typed-extraction-plugin.dev: plugin/RocqMakefile.plugin.local:2 names coq-core.plugins.extraction. Renaming it to rocq-runtime.plugins.extraction is the whole fix, verified through .cmxs and Loader.v.

• coq-interval.dev: configure.in:44 sets COQROOT=coq-core, and configure.in:160/170 query $COQROOT.engine; src/Plot/META.coq-interval:4 also requires coq-core.plugins.ltac. Renaming those clears configuration but reveals a separate V9.3+rc1 break at src/Plot/plot.c:236, caused by 9b1424650d changing Constrexpr.CGenarg and Ltac_plugin.Tacarg.wit_ltac_in_term.

A census of 77 repositories behind 109 recipes in #3809–#3812 found four literal coq-core. lines. Besides the two real cases above, coq-belgames has an unused FINDLIBPKGS entry but no .ml, .mlg, or .mli, while rocq-elpi-json / rocq-elpi-xml contain a comment next to a script that already creates the compatibility shim from rocq-runtime.kernel. Five repositories' seven code-bearing submodules were also screened and had no hits. Dynamically assembled names and pre-fix dependency revisions remain outside that grep's coverage.

The new name itself comes from 3d60180c53 (rename package coq-core -> rocq-runtime). HB's corresponding adaptation for the reserved-of change is a12d7cc57 (also cited upstream as a12d7cc), released in v1.10.3; it changes comments, documentation, error strings, and examples rather than owning the removed grammar.

Hidden of breakage

The source census for #21611 (e6a2fb9b2f, first tag V9.3+rc1) covered 29 pristine repositories at their pinned refs and 3060 .v files. After stripping comments and strings, it counted of only at delimiter depth 0 before the first top-level : or :=, excluding constructors, HB.structure Definition bodies, and quoted term notations. Those exclusions account for 189 + 67 + 17 = 273 legal sites. Mathcomp is the negative control: 0 broken / 530 legal across 139 files at both 2.6.0 and dev.

The result is 183 sites in 10 repositories: 83 HB.builders Context, 53 HB.factory Record, 41 HB.mixin Record, and 6 plain Definition/Lemma binders.

repository (recipes)	sites	status
rocq-partial-orders	147	latent behind rocq-elpi
coq-infotheo, rocq-infotheo	20	latent behind coq-interval
rocq-navi	4	latent behind rocq-elpi; sites are in examples/ and HB is {with-test}
coq-ssprove, rocq-ssprove	2	latent behind coq-deriving
coq-mathcomp-cad	2	latent behind rocq-mathcomp-finmap
rocq-rouche-capelli	1	latent behind rocq-mathcomp-finmap; built past locally
rocq-categories	1	latent behind rocq-elpi
rocq-robot-rocq	1	behind its own earlier error, angle.v:126
rocq-mathcomp-hollight-real-with-N	1	visible now
rocq-relation-algebra	4	green, but all sites are in fhrel.v behind --enable-ssr and a depopts: gate

The backward-compatible fix is token substitution: replace of with &, preserving any existing &. This passed on Rocq 9.2 with HB 1.10.2 and Rocq dev with HB dev. Fifteen sites have multiple binders; dropping an existing & can preserve parsing while changing arity.

Of those 15 multi-binder sites, 13 have two binders and 2 have three. Twelve remain live, all in unported packages: rocq-partial-orders has 8, including the three-binder heads at theories/lattice.v:179 and :215; coq-infotheo / rocq-infotheo have 3; and rocq-rouche-capelli has 1. The census tracks sentences and delimiter depth rather than line starts, because an anchored regex misses multiline heads such as the rocq-rouche-capelli example.

rocq-rouche-capelli demonstrates both the fix and the lower-bound claim:

HB.mixin Record isFinVector
  (R : nzRingType) (V : Type) of Vector R V & Finite V := {}.

The correct replacement is (V : Type) & Vector R V & Finite V. After that change, the build reaches rouche_capelli.v:57, Cannot apply lemma v2r_inj. math-comp 2.6 removed Global Set SsrOldRewriteGoalsOrder, reversing side-goal order; Set SsrOldRewriteGoalsOrder. fixes the second failure. Thus the census finds the first source error, not every error behind it.

OCaml 4.09 and recipe bounds

rocq-runtime.9.0.dev permits ocaml >= 4.09.0; 9.1 and later require >= 4.14.0. Consequently, the 4.09.0 job cannot use rocq-core.dev and falls back to older provers. In #3809's 45-recipe job, 28 skipped, 17 built, and 0 of those 17 used dev. The resolved versions included coq 8.16+rc1, coq 8.16.dev, coq 8.20.dev, coq-core 8.20.dev, coq 9.0.dev, and rocq-core 9.0.dev.

rocq-color.dev and rocq-coinduction.dev used a numeric floor on rocq-prover, but rocq-prover.meta.1 sorts above every numeric version and has only unconstrained dependencies on rocq-core and rocq-stdlib. Thus {>= "9.2"} admits meta.1 and does not transfer the floor to rocq-core. The 4.09.0 job selected rocq-core 9.0.dev, whose parser predates Abbreviation (#20855, 436dca3b11, first tag V9.2+rc1), producing Syntax error: illegal begin of vernac.

Commit d65d1fddc replaces all eight numeric rocq-prover dependencies under extra-dev and core-dev with "rocq-core" {= "dev"}. git grep -l '"rocq-prover"' d65d1fddc^ -- extra-dev core-dev finds 8 files and the same grep at HEAD finds 0. The affected recipes are rocq-color, rocq-coinduction, coq-hol-light, coq-hol-light-real-with-N, coq-hol-light-real-with-nat, rocq-hollight-logic, rocq-hollight-logic-unif, and rocq-mathcomp-hollight-real-with-N.

rocq-color also allowed old rocq-bignums; rocq-coinduction allowed unconstrained rocq-stdlib. This PR pins all necessary paths:

- "rocq-prover"  {>= "9.0"}/{>= "9.2"}  + "rocq-core"    {= "dev"}   # all eight
- "rocq-bignums" {>= "9.0"}             + "rocq-bignums" {= "dev"}   # rocq-color only
- "rocq-stdlib"                         + "rocq-stdlib"  {= "dev"}   # rocq-coinduction only

coq-vcfloat is different. Its constraint is:

"coq" {(>= "8.16" & < "8.19~") | = "dev"}

On OCaml 4.09, the dev branch is unavailable and the solver validly falls back to Coq 8.16. The recipe therefore remains red; changing it would require a policy decision about whether extra-dev recipes may retain non-dev fallbacks.

The resolved versions were read from job 7695047: rocq-coinduction.dev and rocq-color.dev received rocq-core 9.0.dev, while coq-vcfloat.dev received coq 8.16.dev. For the vacuous rocq-prover floor, raising the number would not help—not 9.9, 99, or 9999999—because meta.1 sorts above any numeric version. This ordering was checked against opam show -f all-versions for 12 packages and 779 versions with zero disagreements.

Job 7709751 contains 10 install rocq-prover meta.1 plan lines. Six are in plans that were executed, covering four recipes: rocq-coinduction, rocq-color, coq-hol-light-real-with-N, and coq-hol-light-real-with-nat. The other four occur only in --update-invariant re-plans. Thus eight recipes contain the defect, while this job directly executes four of them.

Four failures on the 4.09.0 job are also Failed to get sources of coq.8.16+rc1: Bad checksum. They come from the coq/coq → rocq-prover/rocq rename changing the top-level directory in generated GitHub archive tarballs. The recorded digest is 87ad8e99…; current bytes hash to b0cf2831…. The archive-wide census found 32 recipes across 16 distinct tarballs with mismatches, versus 9 matches and 0 mismatches for 9 distinct URLs from repositories that were not renamed. Released versions using uploaded release assets are unaffected. This PR's changed-file list does not intersect those 32 recipes.

V8.17+rc1 is affected in the same way (7dc99523… recorded, 55b8066f… current). Pipelines 1455710 (2026-08-01) and 1457864 (2026-08-06) date the exposure, likely through source-cache eviction, rather than the defect; four recipes had already been repaired upstream on 2026-02-21. The census fetched and checked all 19 distinct coq/coq archive URLs rather than relying on a sha512-shaped grep, so it also covers md5 recipes and both /archive/refs/tags/<TAG> and /archive/<TAG> spellings.

The source checksum failure is deterministic but does not identify the full affected set from one job: job 7709746 fetched four of the 32 broken recipes, leaving at least 28 unreached in that run. Three URLs and four recipes were already clean after the February repair; V8.8+beta1 is split, with one of its two recipes repaired and the other still stale. The release-asset control was also fetched and matched, supporting the distinction between mutable generated archives and immutable uploaded assets.

Interpreting the pipeline

The archive helper runs feasibility checks and actual installs differently:

echo Check if $PKG is installable
if opam install "$PKG" -y --with-test --show-action $EXTRA_OPAM_OPTION; then
  echo Installing $PKG
  opam install "$PKG" -y -v -v --with-test $EXTRA_OPAM_OPTION >> $LOG
else
  echo Skipping $PKG since not installable with the current compiler
  echo Check if $PKG is installable with another compiler
  opam install "$PKG" -y --show-action --update-invariant
fi

Both branches print a --show-action plan, while only the first performs the install. In job 7709751, 90 packages were attempted: 28 plans were executed and 62 packages skipped. Four skipped packages timed out before printing a plan, leaving 86 visible plans: 28 acted-on and 58 --update-invariant re-plans. The reliable discriminator is an Installing <pkg> line after the plan's ===== N to install ===== trailer and before the next plan. Every one of the 58 re-plan trailers includes to upgrade; none of the 28 executed-plan trailers does.

The counts can be reproduced with:

grep -cE 'Skipping .* since not installable with the current compiler'  # 62
grep -c  'Skipping'                                                     # 63  <- WRONG
grep -oE '=====[^=]*=====' | sed -E 's/[0-9]+/N/g' | sort | uniq -c
#   58  ===== N to install | N to upgrade =====   <- re-plan
#   28  ===== N to install =====                  <- acted on
#   30  ==========                                <- section rule, not a plan

The bare Skipping count includes GitLab's Skipping Git submodules setup. Plan lines must be paired with the following trailer, not the preceding one. The complete log is 1,101,192 bytes; a prior 1,046,155-byte fetch was a byte-identical prefix and produced plausible but incomplete totals. Counts require the job-end marker (Cleaning up project directory, followed by Job succeeded or ERROR: Job failed).

Job 7709746 is the complete 4.09 audit for #3809's 45 recipes: 28 skipped and 17 built, with zero builds on literal dev. The corresponding 4.14.2 and 5.3.0 jobs resolved dev for every reached package but were still running when read, so those are open rather than final counts.

Pipeline 1457865's 4.09.0 job provides the direct rocq-prover.meta.1 example: - install rocq-prover meta.1 [required by rocq-color] is followed by Installing coq-color.dev and a compile failure. This pipeline predates d65d1fddc, so it demonstrates the original defect rather than the current branch state.

Hollight dependency floors

Commits 6fc3d127e, 8e582aa97, and 64198bdf6 add coq-mathcomp-ssreflect {>= "2.5.0"} to the Hollight .dev recipes because a coq-mathcomp-classical floor does not imply a post-boot mathcomp. Their upstream states differ:

row	upstream #main	paths in sources	expected result
rocq-hollight-logic-unif.dev	6005c99	mathcomp.boot.*	green — already migrated upstream
rocq-hollight-logic.dev	881963b	mathcomp.ssreflect.*	red until the migration lands

Only rocq-hollight-logic is expected to become red. Its required migration matches rocq-hollight-logic-unif PR #9 (Mathcomp2.5.0, merged 2025-12-15). This PR does not depend on that upstream change.

The related rocq-mathcomp-real-closed.dev correction is commit 81cfd315f: its mathcomp 2.4 floor predates the boot module paths its source requires. The other corrected rows in that batch are rocq-infotheo, coq-coqeal, and coq-trocq-std-examples; only rocq-mathcomp-real-closed.dev belongs to #3809.

The two Hollight rows were not measured by Deducteam's dev leg: that job fails earlier in coq-mathcomp-classical.1.13.0 at mathcomp_extra.v:154, Cannot apply lemma floor_ge_int. The expected outcomes above instead come from the checked source paths and the dev-switch layout: mathcomp/ssreflect/ contains only all_ssreflect.*, while choice and ssrbool live under mathcomp/boot/.

Changes inherited from the stacked branch

dev-packages-green is an ancestor of this branch, so this PR's diff against master includes 45 package files from #3809 and 93 package files total, with all 45 overlapping. CI tests the union. A red row seen here may therefore belong to #3809 rather than this PR.

Three commits on this branch also tighten recipes introduced by #3809. rocq-mathcomp-classical.dev and coq-mathcomp-word.dev replace {(>= "2.4" & < "2.7~") | (= "dev")} dependency menus with {= "dev"}. They already resolve to dev because opam prefers dev, but the pin prevents a released mathcomp 2.6.0 stack from becoming selectable if dev later becomes unattractive. rocq-mathcomp-real-closed.dev raises its mathcomp floor because its source requires post-boot module paths.

The branch has also been rebased over the relevant bound changes. In particular, rocq-typed-extraction-common.dev now contains rocq-core {= "dev"}, matching the description and rendered diff.

Verification and scope

Every recipe passes opam lint --warn=-21 --check-upstream, matching scripts/opam-coq-lint. Verdicts and resolved versions come from the three opam-build jobs on #3809's pipeline (4.09.0 / 4.14.2 / 5.3.0), using the package whose build command actually failed rather than the package nominally under test.

Local builds cover the cases where CI output was truncated or dependencies made rows unreachable: rocq-marble, coq-trocq-std, rocq-mathcomp-finite-group, typed extraction, ConCert, and rocq-rouche-capelli. Where no commit, bound, comparison, or local build established a cause, the ledger says undetermined or unknown (blocked).

The ConCert dev-stack build included rocq-stdpp dev.2026-07-31.0.45d12a56. QuickChick's syntax boundary was checked at source level: QCDerive exists at v2.0.3, bare Derive remains through v2.1.1, ec6bd8db narrows it to Derive Instance, and 5a6c291 removes the block before v2.2.0.

A package absent from a job's failure list is not counted as passing: the compiler jobs reached different depths. Each row is sourced from a job that visited that package's own section. Likewise, a feasible --show-action plan is not counted as an executed install unless followed by Installing <pkg>; the real install output is redirected by scripts/opam-coq-install-remove.

This branch has been rebased onto the bound updates it quotes. It remains stacked on dev-packages-green: that branch is an ancestor, so the diff against master contains #3809's 45 recipes plus this PR's additions. Failures in the combined pipeline must therefore be partitioned by owning PR.

🤖 Generated with Claude Code

Wordsmithed by Codex.