extra-dev: run the remaining dev package installs in opam's install phase (9 recipes)

[JasonGross]

This is a mechanical fix to the install phase of nine recipes. It is not a claim that nine packages build. The tested/untested split is spelled out below, because the file count here does not imply coverage.

The defect

Nine recipes under extra-dev/ run make install as the last command of build: and declare no install: field, so the install executes during opam's build phase instead of its install phase.

This is the same defect and the same one-line mechanical fix as #3793, which cleared 14 recipes of exactly this shape. These nine are the residue that PR left behind.

Every hunk is identical:

   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]

9 files, +9/-9. No dependency, version bound, url, or remove: field is touched anywhere in the diff. install: is the ordinary spelling in this repository already: 3563 of the 4157 opam files in the tree carry one.

The nine recipes

recipe
extra-dev/packages/coq-algebra/coq-algebra.dev
extra-dev/packages/coq-distributed-reference-counting/coq-distributed-reference-counting.dev
extra-dev/packages/coq-fermat4/coq-fermat4.dev
extra-dev/packages/coq-hoare-tut/coq-hoare-tut.dev
extra-dev/packages/coq-jordan-curve-theorem/coq-jordan-curve-theorem.dev
extra-dev/packages/coq-maths/coq-maths.dev
extra-dev/packages/coq-orb-stab/coq-orb-stab.dev
extra-dev/packages/coq-tree-automata/coq-tree-automata.dev
extra-dev/packages/coq-universe-comparator/coq-universe-comparator.1.0.1

Eight are .dev recipes; coq-universe-comparator.1.0.1 is a numeric version carrying the same defect, and it lives under extra-dev/ like the rest.

Independent confirmation: opam lint warning 26

opam lint implements a slightly narrower form of this predicate itself:

warning 26: No field 'install', but a field 'remove': install instructions probably part of 'build'. Use the 'install' field or a .install file

I walked all 4157 opam files in the tree with opam lint and grepped for that warning:

• at the base commit — warning 26 fires on exactly 9 files, and they are exactly the nine listed above;
• at this branch's head — 0 files, across the whole repository.

A per-file comparison of the warning sets before and after shows the change removes warning 26 and introduces no new warning. All nine lint at rc=0 (with --warn=-21); the remaining warnings on them (36, 37, 47, 62) are pre-existing and untouched.

Scope: why this stops at nine

A broader scan of the same 4157 files — "build: performs the install (make install / dune install / a copy into %{lib}%) and the recipe has no install: field" — finds 24 at the base commit: these 9 under extra-dev/, 15 under core-dev/, and 0 under released/. After this change extra-dev/ is at 0 and the archive-wide figure is 15.

The 15 core-dev/ recipes are deliberately left alone here — they are the historical coq.8.0.dev … coq.8.5~rc1 and coqide.8.5~beta* recipes. They are also why warning 26 alone undercounts: W26 additionally requires a remove: field, and those recipes have none, so opam's linter is silent about them. One concern per PR; extra-dev/ going to 0 is a complete story on its own.

Tested / untested

Tested: 1 of 9. coq-tree-automata installs on a Rocq dev switch with exactly this build/install split, and does not install without it — that is the observation this whole PR came from.

Two further recipes of the same shape, coq-bdds and coq-smc, were verified the same way before #3793 landed. They are not part of this PR, but they are the same mechanism working.

Two things about the coq-tree-automata result that should not be blurred together. That install test was run against a fork whose sources have been fixed for a current prover. Upstream coq-contribs/tree-automata, which is what this recipe's url actually names, is red today at coq_makefile: Unknown option -full and would not reach the install step at all.

Untested: 8 of 9 — and none of the eight can be end-to-end tested today. I built each of the eight git-sourced upstreams in an isolated prefix (clone, coq_makefile, make, then make install DESTDIR=…) against a current dev prover. All eight are red, all eight install zero files, and in every case the first failure is upstream source rot with nothing to do with the install phase:

recipe	first failure
coq-tree-automata	coq_makefile rc=1, Unknown option -full
coq-distributed-reference-counting	coq_makefile rc=1, Unknown option -opt
coq-hoare-tut	constructor Iset … applied to 3 arguments
coq-fermat4	infinite_descent: Attempt to save an incomplete proof
coq-jordan-curve-theorem	library Omega … not found
coq-algebra	build error in the sources
coq-maths	build error in the sources
coq-orb-stab	build error in the sources

The ninth, coq-universe-comparator.1.0.1, constrains coq {>= "8.5~beta2" & < "8.5~beta3"}, so it cannot be resolved on any current switch and is untestable by construction.

So the claim being made is precisely: these nine recipes now run their install in opam's install phase. Whether the underlying packages build is a separate question, and for eight of them the answer today is no.

Caveat on the opam version

The lint results above were produced with opam 2.5.1. CI here runs opam 2.1.2, which is the version #3793 was checked against. The edit is plain opam 2.0 syntax used by most of the repository already, so I do not expect a difference, but I have not reproduced the lint run under 2.1.2 locally.