From 4963c2170c300a80b60f0b4102c2fa8b5870f4ca Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Aug 2026 01:52:26 +0000 Subject: [PATCH] Run the remaining dev package installs in opam's install phase Nine extra-dev recipes still call `make install` from `build:` and carry no `install:` field, so the install runs under opam's build sandbox rather than its install sandbox. Under a sandboxed opam the build phase has no write access to the switch prefix, so these rows cannot install: `make install` fails, or worse, silently installs nothing while the build reports success. This is the same defect and the same mechanical fix as #3793, which cleared 14 of the 23 extra-dev rows that had it. These nine are the residue; after this commit the class is empty under extra-dev/. The edit is identical in every file: drop `[make "install"]` from the tail of `build:` and add `install: [make "install"]` immediately after. Nothing else changes -- no dependency, bound, url or remove: field is touched. coq-algebra.dev coq-distributed-reference-counting.dev coq-fermat4.dev coq-hoare-tut.dev coq-jordan-curve-theorem.dev coq-maths.dev coq-orb-stab.dev coq-tree-automata.dev coq-universe-comparator.1.0.1 Tested: coq-tree-automata.dev installs on a Rocq dev switch with exactly this split and does not without it. The other eight are not individually build-tested against a dev prover -- several have other, unrelated reasons not to build there -- so this commit is a fix to the recipes' install phase, not a claim that the nine packages build. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- extra-dev/packages/coq-algebra/coq-algebra.dev/opam | 2 +- .../coq-distributed-reference-counting.dev/opam | 2 +- extra-dev/packages/coq-fermat4/coq-fermat4.dev/opam | 2 +- extra-dev/packages/coq-hoare-tut/coq-hoare-tut.dev/opam | 2 +- .../coq-jordan-curve-theorem/coq-jordan-curve-theorem.dev/opam | 2 +- extra-dev/packages/coq-maths/coq-maths.dev/opam | 2 +- extra-dev/packages/coq-orb-stab/coq-orb-stab.dev/opam | 2 +- extra-dev/packages/coq-tree-automata/coq-tree-automata.dev/opam | 2 +- .../coq-universe-comparator/coq-universe-comparator.1.0.1/opam | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/extra-dev/packages/coq-algebra/coq-algebra.dev/opam b/extra-dev/packages/coq-algebra/coq-algebra.dev/opam index aa3473243e..503437ef4d 100644 --- a/extra-dev/packages/coq-algebra/coq-algebra.dev/opam +++ b/extra-dev/packages/coq-algebra/coq-algebra.dev/opam @@ -5,8 +5,8 @@ license: "LGPL 2" build: [ ["coq_makefile" "-f" "Make" "-o" "Makefile"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Algebra"] depends: [ "ocaml" diff --git a/extra-dev/packages/coq-distributed-reference-counting/coq-distributed-reference-counting.dev/opam b/extra-dev/packages/coq-distributed-reference-counting/coq-distributed-reference-counting.dev/opam index f6f88640d0..67857b09a3 100644 --- a/extra-dev/packages/coq-distributed-reference-counting/coq-distributed-reference-counting.dev/opam +++ b/extra-dev/packages/coq-distributed-reference-counting/coq-distributed-reference-counting.dev/opam @@ -5,8 +5,8 @@ license: "LGPL 2" build: [ ["coq_makefile" "-f" "Make" "-o" "Makefile"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/DistributedReferenceCounting"] depends: [ "ocaml" diff --git a/extra-dev/packages/coq-fermat4/coq-fermat4.dev/opam b/extra-dev/packages/coq-fermat4/coq-fermat4.dev/opam index c9556378b8..9f2bb88109 100644 --- a/extra-dev/packages/coq-fermat4/coq-fermat4.dev/opam +++ b/extra-dev/packages/coq-fermat4/coq-fermat4.dev/opam @@ -5,8 +5,8 @@ license: "Proprietary" build: [ ["coq_makefile" "-f" "Make" "-o" "Makefile"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Fermat4"] depends: [ "ocaml" diff --git a/extra-dev/packages/coq-hoare-tut/coq-hoare-tut.dev/opam b/extra-dev/packages/coq-hoare-tut/coq-hoare-tut.dev/opam index 163c8bbd93..e6860c0374 100644 --- a/extra-dev/packages/coq-hoare-tut/coq-hoare-tut.dev/opam +++ b/extra-dev/packages/coq-hoare-tut/coq-hoare-tut.dev/opam @@ -5,8 +5,8 @@ license: "GNU LGPL" build: [ ["coq_makefile" "-f" "_CoqProject" "-o" "Makefile"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/HoareTut"] depends: [ "ocaml" diff --git a/extra-dev/packages/coq-jordan-curve-theorem/coq-jordan-curve-theorem.dev/opam b/extra-dev/packages/coq-jordan-curve-theorem/coq-jordan-curve-theorem.dev/opam index 48b43357ea..5e06bc02eb 100644 --- a/extra-dev/packages/coq-jordan-curve-theorem/coq-jordan-curve-theorem.dev/opam +++ b/extra-dev/packages/coq-jordan-curve-theorem/coq-jordan-curve-theorem.dev/opam @@ -5,8 +5,8 @@ license: "unknown" build: [ ["coq_makefile" "-f" "Make" "-o" "Makefile"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/JordanCurveTheorem"] depends: [ "ocaml" diff --git a/extra-dev/packages/coq-maths/coq-maths.dev/opam b/extra-dev/packages/coq-maths/coq-maths.dev/opam index f68bbc22a6..29e028cc49 100644 --- a/extra-dev/packages/coq-maths/coq-maths.dev/opam +++ b/extra-dev/packages/coq-maths/coq-maths.dev/opam @@ -5,8 +5,8 @@ license: "LGPL 2" build: [ ["coq_makefile" "-f" "Make" "-o" "Makefile"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Maths"] depends: [ "ocaml" diff --git a/extra-dev/packages/coq-orb-stab/coq-orb-stab.dev/opam b/extra-dev/packages/coq-orb-stab/coq-orb-stab.dev/opam index ef1f8a3cf6..0e1813ed1f 100644 --- a/extra-dev/packages/coq-orb-stab/coq-orb-stab.dev/opam +++ b/extra-dev/packages/coq-orb-stab/coq-orb-stab.dev/opam @@ -5,8 +5,8 @@ license: "GNU Lesser Public License" build: [ ["coq_makefile" "-f" "Make" "-o" "Makefile"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/OrbStab"] depends: [ "ocaml" diff --git a/extra-dev/packages/coq-tree-automata/coq-tree-automata.dev/opam b/extra-dev/packages/coq-tree-automata/coq-tree-automata.dev/opam index d70c1421eb..bf81d2280b 100644 --- a/extra-dev/packages/coq-tree-automata/coq-tree-automata.dev/opam +++ b/extra-dev/packages/coq-tree-automata/coq-tree-automata.dev/opam @@ -5,8 +5,8 @@ license: "LGPL 2" build: [ ["coq_makefile" "-f" "Make" "-o" "Makefile"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/TreeAutomata"] depends: [ "ocaml" diff --git a/extra-dev/packages/coq-universe-comparator/coq-universe-comparator.1.0.1/opam b/extra-dev/packages/coq-universe-comparator/coq-universe-comparator.1.0.1/opam index 5c2131fcec..9ad0ca2162 100644 --- a/extra-dev/packages/coq-universe-comparator/coq-universe-comparator.1.0.1/opam +++ b/extra-dev/packages/coq-universe-comparator/coq-universe-comparator.1.0.1/opam @@ -7,8 +7,8 @@ license: "MIT" build: [ ["./configure.sh"] [make "-j%{jobs}%"] - [make "install"] ] +install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/UniverseComparator"] depends: [ "ocaml"