Add rocq-certirocq.dev

[JasonGross]

Draft; blocked on #3693. This cannot go green or merge until that PR lands. The dependency bounds would also benefit from review.

Adds extra-dev/packages/rocq-certirocq/rocq-certirocq.dev/opam, tracking CertiRocq's main branch. The existing released/packages/rocq-certirocq/rocq-certirocq.0.9.1+9.1 remains unchanged, as does extra-dev/packages/coq-certicoq/coq-certicoq.dev, which tracks the old CertiCoq/certicoq repository for Coq 8.20.

Why #3693 is required

All three opam-build jobs (4.09.0, 4.14.2, 5.3.0) stopped before compilation:

Check if rocq-certirocq.dev is installable
[ERROR] Package conflict!
No solution found, exiting
...
Packages that can never be installed: rocq-certirocq.dev

Both the --show-action probe and --show-action --update-invariant retry in scripts/opam-coq-install-remove returned Package conflict!. rocq-metarocq-{erasure,safechecker}-plugin {= "dev"} pulls in rocq-metarocq-utils.dev, which requires "rocq-core" { = "dev" }, while released/packages/coq-wasm/coq-wasm.2.2.0 requires "coq" {>= "8.20" & < "9.2~"}. No coq-wasm.dev currently exists, and no assignment satisfies both constraints. #3693 adds that package, so this uses "coq-wasm" {= "dev"}; {>= "2.2.0"} could not coexist with dev MetaRocq.

Package and dependencies

CertiRocq has one root opam file, rocq-certirocq.opam. Its make install installs the theories, plugins/plugin as findlib rocq-certirocq, plugins/cplugin as findlib rocq-certirocq-vanilla, the C runtime under runtime/, and the compiler under bootstrap/. Separate META files do not represent separate opam packages.

main (default branch, HEAD 45a1950, 2026-06-25) is the development branch. master and coq-9.1 share commit 59f1103, 2026-05-04, corresponding to the existing 9.1 package.

The package follows upstream's file, dropping its dune-style header and version: and appending the usual url { src: ... } block. These dependency changes are also proposed in CertiRocq/certirocq#159:

upstream	here	reason
"coq" {>= "9.1" & < "9.2~"}	"rocq-core" {>= "9.1"}, "rocq-stdlib" {>= "9.1"}, "coq-core" {>= "9.1"}	main has 220 From Stdlib Require occurrences. coq-core provides the coq_makefile binary invoked by Makefile, libraries/Makefile, and the plugin Makefiles; on a 9.4+alpha switch, bin/coq_makefile belongs to coq-core, not rocq-core. As usual for .dev, there is no upper bound.
"coq-compcert" {= "3.17"}	"coq-compcert" {>= "3.17"}	Avoids making the dev package uninstallable when CompCert advances.
"rocq-equations" {= "1.3.1+9.1"}	"rocq-equations" {>= "1.3.1+9.1"}	Also permits rocq-equations.dev.
"coq-wasm" {= "2.2.0"}	"coq-wasm" {= "dev"}	Required by dev MetaRocq, as described above.
"rocq-metarocq-erasure-plugin" {>= "1.5.1"}, "rocq-metarocq-safechecker-plugin" {>= "1.5.1"}	{= "dev"}	theories/Compiler/metarocq_pipeline.v:19 imports EImplementBox EImplementLazyForce; EImplementLazyForce.v is absent from tag v1.5.1-9.2 and exists only on MetaRocq main.
—	"conf-python-3" {build}	make plugins runs python3 plugins/manifests/generate.py for plugins/*/\_CoqProject and plugins/*/*.mlpack. Although generated files are checked in, their rule depends on the always-rebuilt theories/Extraction/extraction.vo.

Verification limits

opam lint --warn=-21 --check-upstream passes under opam 2.1.2, the version pinned by .gitlab-ci.yml.

There is no successful build evidence for this package from CI or locally. CI reached only the solver failure above. A local Rocq-dev build could not complete without mutating the switch:

• Its MetaRocq commit 9242c14 (2026-07-15) predates EImplementLazyForce; there Monomorphic_entry was nullary. MetaRocq main at e8bb91d (2026-07-29) restores the ContextSet.t argument used by theories/LambdaANF/PrototypeGenFrame.v. Source inspection suggests both errors are resolved on current main, but MetaRocq main was not built to confirm.
• The switch has coq-compcert-64, installed under lib/coq-variant/compcert64/, rather than coq-compcert. coq-wasm.dev installs a partial compcert tree into user-contrib/compcert (Archi, lib/{Coqlib,Floats,IEEE754_extra,Integers,Zbits}, common/Memdata), colliding with a real coq-compcert installation. A conflicts: field may be appropriate, but is out of scope.

Once #3693 lets CI pass the solver, its result will be the first build signal.

Wordsmithed by Codex.

[JasonGross]

How does one get

File "./maps_util.v", line 1, characters 0-33:
Error:
Compiled library compcert.lib.Maps (in file /builds/coq/opam-repositories/opam-root-4.14.2-2.1.2-sandbox/4.14.2/lib/coq/user-contrib/compcert/lib/Maps.vo) makes inconsistent assumptions over library compcert.lib.Coqlib

On CI?