extra-dev: add 32 dev recipes and update 11 more, for packages that install successfully

[JasonGross]

Undrafted, and narrowed to the 45 recipes whose packages actually install
against Rocq master.

This started as one 88-recipe batch. Its pipeline gave a clean per-package,
per-compiler verdict, so it is now split in two: this PR keeps the 45 that
install, and #3812 carries the 43 that do not. #3812 is stacked on this
one. The recipes are the ones from the original batch; four commits on top
tighten prover bounds that were loose enough to resolve a released prover, so
that a green here means what it says. Those edits are described under
How the recipes were written below.

CI evidence

Read off the three opam-build jobs of the pipeline on the original 88-recipe
head (171b3335), per package rather than per job:

outcome	n
installed on all three compilers	15
installed on 4.14.2 and 5.3.0, skipped on 4.09.0	28
coq-pil, rocq-pil	2

Read the first row as "installed", not as "installed against master": the 4.09.0
column carries no information about Rocq master at all, for the reason set out
under Read the 4.14.2 and 5.3.0 jobs below. The 15 is a three-compiler
portability result; the dev result is the 4.14.2 and 5.3.0 columns alone.

The 28 skips are Skipping ... since not installable with the current compiler: rocq-runtime.9.0.dev allows ocaml >= 4.09.0 but 9.1, 9.2, 9.3 and
dev all require >= 4.14.0, so the 4.09.0 job's solver can only reach
rocq-core 9.0.dev, which the mathcomp-analysis family's lower bounds
exclude. A skip is a pass as far as the archive gate is concerned.

The pil pair is the only qualification. coq-pil installed on 4.09.0 and
rocq-pil on 4.09.0 and 5.3.0; their remaining jobs died fetching a
dependency's sources, not building anything:

[ERROR] Failed to get sources of coq-stdpp.1.12.0: curl error code 429

That is GitLab rate-limiting the runner. No other package in this PR appears
in any job's Packages that failed to install: line, and none appears in any
Packages that can never be installed: line — every package that did is in
#3812.

The 4.09.0 job at 3b3d471 was red, for a defect that predates this PR

This section describes pipeline 1457864, which ran on 3b3d471 — before the
four prover-bound commits now at the head of this branch. Those commits were
written to fix exactly what it found, so the pipeline on the current head is the
test of the fix, not a repeat of this. Left in because the diagnosis is what
motivates the commits.

Job 7709746 exits 1 with five names:

Packages that failed to install: coq-kruskal-fan.dev coq-kruskal-finite.dev \
  coq-kruskal-veldman.dev coq-ordinal.dev coq-pil.dev
Packages that can never be installed:

All five are in this PR, and none of them failed on its own sources. There
are zero occurrences of [ERROR] The compilation of in the job's 615 KB log.
Every one died fetching a dependency's tarball — four on coq.8.16+rc1 and
one on the same coq-stdpp rate-limit as above:

4 x [ERROR] Failed to get sources of coq.8.16+rc1: Bad checksum
1 x [ERROR] Failed to get sources of coq-stdpp.1.12.0: curl error code 429

Only the 429 will clear on a retry — but all five failures have the same
cause, and it is not the tarballs. None of the five recipes constrains its
prover toward dev: coq-kruskal-{fan,veldman} and coq-pil declare no
prover dependency at all, and coq-kruskal-finite and coq-ordinal declare
only a bare floor ("coq" {>= "8.14"} and {>= "8.9"}) with no ceiling. On
4.09 that lets the solver walk back far enough to reach a broken artifact —
four of them landed on coq.8.16+rc1 and coq-pil stopped at coq 8.20.dev
and died fetching coq-stdpp instead. Classifying these by error message
scatters one defect across two buckets.

The four checksum failures are also deterministic and will recur on every
pipeline until the archive is fixed, and they are not this PR's doing. GitHub
names the top-level directory inside an auto-generated /archive/ tarball after
the repository's current name, and coq/coq now redirects to
rocq-prover/rocq:

https://github.com/coq/coq/archive/refs/tags/V8.16+rc1.tar.gz
  301 -> https://github.com/rocq-prover/rocq/archive/refs/tags/V8.16+rc1.tar.gz
  302 -> https://codeload.github.com/rocq-prover/rocq/tar.gz/refs/tags/V8.16%2Brc1

Same tag, same commit, same files — but the archive now unpacks to
rocq-8.16-rc1/ where the recorded sha512 was taken over coq-8.16-rc1/.
Both affected tags were measured, byte-identical across two fetches each:

V8.16+rc1  recorded 87ad8e99…  actual b0cf2831…  topdir rocq-8.16-rc1/
V8.17+rc1  recorded 7dc99523…  actual 55b8066f…  topdir rocq-8.17-rc1/

Thirty-two recipes archive-wide are affected, across sixteen distinct
tarballs — every core-dev recipe fetching a generated coq/coq archive, not
only the +rc1 ones. 36 recipes over 19 tarballs are candidates; 32 over 16 were
still stale when measured, and the remaining 4 had already been repaired
upstream. The defect also reaches md5 recipes (the 8.5–8.10 betas), so a
sha512-shaped search undercounts it a second way:

V8.14+rc1.tar.gz  (legacy /archive/<TAG> spelling)  -> topdir rocq-8.14-rc1/
V8.5beta1.tar.gz  (legacy spelling, md5)            -> topdir rocq-8.5beta1/

The /archive/<TAG>.tar.gz and /archive/refs/tags/<TAG>.tar.gz spellings are
the same generated endpoint and break identically; searching only for the latter
is what produces the appealing but wrong answer that seven recipes and two URLs
are involved.

The defect is roughly six months old, not new. Four recipes were already
repaired upstream on 2026-02-21 (db5a6c07e, 5cb9e6e56, c71643346,
325bb876d, each titled fix(coq.8.N+betaM): camlp5 version and MD5). A cheap
no-network tell for that piecemeal repair: coq.8.8+beta1 and coqide.8.8+beta1
share one URL but recorded different md5s, because only the first had been
fixed. So the fact that pipeline 1455710 (2026-08-01) shows zero occurrences and
1457864 shows four dates the exposure — most likely a source-cache eviction —
and not the defect.

Almost all of the 32 are latent, because a recipe has to actually be fetched to
fail: the four observed failures measure which recipes this solver happened to
reach, not the size of the defect. Released versions are structurally immune —
they use release assets, immutable uploads rather than generated archives.
This PR touches none of the 32.

Read the 4.14.2 and 5.3.0 jobs, not the 4.09.0 one

That 4.09.0 job would be weak evidence about Rocq master even if it were green.
rocq-core.dev requires OCaml >= 4.14, so on 4.09 the solver does not skip —
it walks backward to whatever ancient prover a recipe's bounds still admit.
Taking the resolved - install {coq,rocq-core} <version> line out of each
Check if <pkg> is installable section of job 7709746, and pairing every plan
with a check for that section's Skipping … line:

sections seen      : 45
never built (skip) : 28      <- plans in these are hypothetical
built, on dev      :  0
built, NOT on dev  : 17      (12 ok, 5 FAIL)

Not one of the 45 packages was built against Rocq master on this job. The 17
that were built resolved coq 8.16+rc1, 8.16.dev, 8.20.dev or
rocq-core 9.0.dev; the other 28 were never built at all. A green here means
"builds against Coq 8.16", not "builds against Rocq master".

The pairing matters because a skipped section still prints a plan — the
opam install --show-action --update-invariant retry, which is allowed to
change the compiler and so routinely shows rocq-core dev for a package that
was never compiled. Read without that check, this job appears to test 27
packages against master. It tests none.

The same audit on 4.14.2 (7709747) and 5.3.0 (7709748) resolves dev for
every section either job has reached, with none skipped and none walked back
— 15 and 15 as of the latest sample, including the whole Kruskal family. Both
jobs are still running, so the counts are lower bounds and will rise; what does
not change with more sections is the part that matters, that no section on
either job resolved anything other than dev. Final counts go in when the jobs
are terminal. These are the two jobs that carry the evidence for this PR.

Three of them were not actually tested against master

(Also read off the terminal 88-recipe run at 171b3335, not off the live
pipeline audited in the two sections above.)

Worth stating plainly, because it is the thing a .dev recipe is for. I pulled
the resolved rocq-core version out of every per-package section rather than
trusting the job name, and three packages here never had Rocq master in their
install plan on any compiler: coq-pil and rocq-pil resolved
rocq-core 8.20.dev, and rocq-cakeml-extraction resolved 9.2.dev. Seven
more resolved an older line on the 4.09.0 job only and dev on the other two,
which is enough. So the honest count is 42 verified against master, 3
installed against an older Rocq.

None of the three declares an upper bound on rocq-core — the cap is
transitive, and visible in the install plans:

rocq-cakeml-extraction.dev
  - install rocq-core                    9.2.dev   [required by rocq-cakeml-extraction]
  - install rocq-metarocq-erasure-plugin 1.5.1+9.2 [required by rocq-cakeml-extraction]

rocq-pil.dev
  - install coq                          8.20.dev  [required by rocq-pil]
  - install coq-core                     8.20.dev  [required by coq]
  - install coq-equations                1.3.1+8.20 [required by rocq-pil]
  - install coq-stdpp                    1.12.0    [required by rocq-pil]

rocq-cakeml-extraction asks for
rocq-metarocq-erasure-plugin {>= "1.4" & < "1.5.2"}, and the release that
satisfies it is built for the 9.2 line. The pil recipes depend on the legacy
coq package rather than rocq-core, and land on coq 8.20.dev next to
coq-equations 1.3.1+8.20. A .dev recipe whose transitive
closure caps rocq-core is silent about master whether it goes green or red,
so these three are recipes that exist and lint but do not yet produce the
signal they are for.

Two of the three are addressed by the bound commits, one is not:

• coq-pil / rocq-pil reached coq 8.20.dev through their own loose
  coq floor, so the fix is local. Both are edited here (see Renames below);
  rocq-pil needed the rename rather than a tightening, because every archive
  coq-stdpp caps coq below dev. This is a prediction, not a measurement
  — the 42/3 count above was read off 171b3335, which predates these commits,
  and only the next pipeline can confirm the walk-back is gone.
• rocq-cakeml-extraction is not fixed and is deliberately left alone. Its
  cap is transitive, through rocq-metarocq-erasure-plugin {>= "1.4" & < "1.5.2"},
  whose satisfying release is built for the 9.2 line; pinning the prover to dev
  here would make the recipe uninstallable rather than correct. Fixing it means
  moving the dependency's bound, which is upstream of this PR. Its green is
  real, and it is 9.2 evidence.

#3812 has the same section — 14 of the 43 red ones are red against 9.1, 9.0 or
8.20, not against master.

And one of them installs with a feature switched off

rocq-relation-algebra.dev is green against master, but only because CI never
installs a depopt. The recipe declares

depopts: [ "rocq-mathcomp-ssreflect" "rocq-aac-tactics" ]
build: ["sh" "-exc" "./configure --%{rocq-mathcomp-ssreflect:enable}%-ssr --%{rocq-aac-tactics:enable}%-aac"]

and upstream's configure responds to --enable-ssr by appending
theories/fhrel.v to _RocqProject — a file _RocqProject ships commented
out. So the package compiles more code whenever mathcomp happens to be in the
same switch. Its install plan on 5.3.0 is ten packages ending
rocq-core dev / rocq-stdlib dev, with no mathcomp and no aac-tactics, and
across all 88 per-package sections of the pipeline no plan co-installs
relation-algebra with mathcomp — its three consumers here (rocq-sims,
coq-atbr, rocq-ctree) pull neither. Every green it has is a
--disable-ssr --disable-aac green.

In a switch that does have mathcomp installed, --enable-ssr is passed and the
extra file fails on Rocq dev, identically at 1.9.0 and at master (2d2af36):

File "./theories/fhrel.v", line 5, characters 0-110:
Error: Notation "[ ! _ ]" is already defined at level 0 with arguments constr
while it is now required to be at level 0 with arguments constr at level 200.

This is not a Rocq-dev breakage, and fhrel.v has at least three independent
ones. All of the following was executed, not inferred.

The mathcomp hedge is void, not merely narrow. fhrel.v imports only boot/
modules, and boot/'s tree SHA is identical at tag mathcomp-2.6.0 and at
78cb0653 (the commit a dev pin resolves): both
8d9a278e093947a1a496bca0e86012e5bd7cdcd4. (Positive control that the diff is
live: algebra/ differs by 19 files.) So this already was released-mathcomp
evidence. Rebuilding mathcomp 2.6.0 boot/ from source against 9.4+alpha
confirms it — 25/25 .vo, 0 errors, and fhrel.v then fails byte-identically,
with the loadpath verified by probe rather than assumed.

The clashing notation is relation-algebra's own, and it is not new. Rocq's
[ ! _ ] lives in theories/Corelib/ssr/ssreflect_rw.v:628 and has since
312497af6a (2023-12-06). relation-algebra added a conflicting spelling at
kat.v:27 on 2026-01-07 (6b326b9, "Adapt to rocq-prover/rocq#21478")
without a level annotation. Reproduced with the real kat.v and no mathcomp
at all, and on 9.0.0, 9.1.1, 9.2+rc2 and 9.4+alpha alike; reversing the
require order fails symmetrically, so it is not an ordering artefact. Present at
both 1.8.1 and 1.9.0, so no version pin dodges it. One-line fix, verified:
add (at level 0, p at level 200).

Behind it sits a genuine Rocq change — but a released 9.3 one. With the
notation fixed, fhrel.v:39 fails on
Definition fhrel_of of phant A & phant B := fhrel_type. with
Syntax error: [def_body] expected after [ident_decl]. Reserving of
(rocq #21611, e6a2fb9b2f, git tag --contains → V9.3+rc1) removed the
ssr plugin's of/& extension of def_body. Version-bracketed probe on
Definition foo of nat & bool := 0.: rc=0 on 9.0.0 / 9.1.1 / 9.2+rc2, rc=1 on
9.4+alpha. This will hit any contrib using the mathcomp phantom-type idiom,
and it is intentional and changelogged — worth knowing well beyond this package.
A third failure follows at fhrel.v:288 (The LHS of eq_cardT #|_| does not match any subterm of the goal), against released mathcomp 2.6.0, unresolved.

Nobody has ever built this file. Upstream CI (build-relation-algebra.yml,
docker-coq-action with opam_file:) installs depends: but not depopts:, so
upstream builds --disable-ssr too. --enable-ssr has been broken for months
on every supported Rocq, and no CI anywhere exercises it.

--enable-aac remains simply unmeasured: coq-aac-tactics.dev is green in this
same batch, so the combination is installable, and nobody has built it.

I am leaving the package here — its verdict under the closure CI actually solves
is green, and a depopt-off green is an honest result. But the general point is
now sharper than "weaker for this one": a depopt-gated green is silent about
code the recipe compiles only when the optional dependency is present, and that
silence can hide breakage that predates the version under test by months and
belongs to a third party. Same shape as a transitively-capped plan being silent
about master whatever colour it comes out.

How the set was chosen

rocq-dev sees five repositories (iris-dev, coq-released, rocq-core-dev,
rocq-extra-dev, default). Taking the exact set difference between the
released package names and the names that have any dev version in any of
them — iris-dev versions are dev.<date>.<n>.<sha>, so a .dev suffix test
misses all 35 of them — leaves 322 released packages with no dev at all.

Filtering that down:

bucket	n	verdict
dev exists under the other name (coq-/rocq- skew)	17	rename
coq-X whose rocq-X twin is also released	24	superseded, skip
latest release capped below Rocq 9.0	145	dead, skip
no coq/rocq dependency and frozen	~10	skip
worth authoring	75	this PR + #3812, minus 3

The three subtractions: coq-wasm is #3693, rocq-certirocq is #3807, and
coq-sail no longer exists upstream — rems-project/coq-sail main ships only
rocq-sail-stdpp.opam, which is #3800.

How the recipes were written

Each is upstream's own in-tree opam file at the default branch, with
version: dropped and url { src: "git+<repo>#<branch>" } appended. Of the 45
here, only coq-bedrock2-compiler comes from a repository that ships no opam
file (mit-plv/bedrock2); it is derived from the latest released recipe with
the tarball url swapped for a git one.

One deliberate edit, in two steps: each recipe's binding prover constraint is
pinned to {= "dev"}.

The first step was to drop upper bounds on coq / coq-core / coq-stdlib /
rocq-core / rocq-runtime / rocq-stdlib. opam orders the version string
dev above any numeric version, so a recipe carrying < "9.2~" can never be
selected on a dev switch — it would be a .dev package that no dev switch can
install.

That was necessary and not sufficient, and the ocaml-4.09 job showed why:
removing the ceiling leaves the floor, and an unbounded-above floor like
coq {>= "8.14"} lets the solver walk backward to Coq 8.16 — which then
fails on an unrelated defect, the archive's stale core-dev tarball checksums. A recipe that resolves Coq 8.16 is not testing dev at all,
so "no upper bound" is not the safety property; {= "dev"} is. 25 recipes are
now pinned, listed in the commit messages.

Where the prover dependency is spelled coq rather than rocq-core, the bound
is tightened in place rather than renamed: coq-core is still the package
that ships coq_makefile, which those recipes' build: invokes, and the shim
chain coq.dev → coq-core {= version} → rocq-runtime {= version} pins rocq
master exactly as rocq-core {= "dev"} would. Renaming would convert a solver
problem into a build problem.

Three recipes are the exception, and each is renamed for a stated reason:

• rocq-pil.dev — coq → rocq-core, coq-stdpp → rocq-stdpp,
  coq-equations → rocq-equations. Here tightening in place is unsatisfiable:
  every coq-stdpp in the archive caps coq (1.12.0 at < "8.21~", 1.11.0 at
  < "9.1~") and there is no coq-stdpp.dev, so coq {= "dev"} alongside it
  has no solution — it would turn a walk-back into a package that can never be
  installed, which is worse. rocq-stdpp.1.13.0 is the only stdpp admitting a
  dev prover. This recipe builds with dune and never invokes coq_makefile, so
  it does not need the compat binaries. On the 4.09 job it resolved
  coq 8.20.dev, coq-stdpp 1.12.0, coq-equations 1.3.1+8.20.
• coq-hol-light-real-with-N.dev and -with-nat.dev — rocq-prover →
  rocq-core + rocq-stdlib. A bound on the rocq-prover metapackage is
  vacuous and routes around every constraint on rocq-core: its version is
  meta.1, which opam orders above any numeric version. The 4.14 job's plan for
  these two shows the metapackage contributing nothing but indirection —
  rocq-runtime dev, rocq-core dev, rocq-stdlib dev, rocq-prover meta.1,
  with no coq or coq-core anywhere — so the renamed dependency set is
  precisely the set that was already being installed.

One asymmetry is worth stating, since it explains why several recipes pin the
core and leave the stdlib loose: the closure runs core → stdlib and not
stdlib → core. rocq-core {= "dev"} excludes every released rocq-stdlib,
because each caps rocq-core (< "9.1~", < "9.4~") and dev fails both — so
a bare companion rocq-stdlib beside a dev-pinned core is not a hole. The
reverse does not hold: rocq-stdlib.dev constrains the core with a disjunction,
rocq-core {>= "9.2" | = "dev"}, whose numeric branch four core-dev versions
satisfy. Pinning the stdlib alone therefore closes nothing.

13 of these greens are against released mathcomp, not mathcomp master

Worth stating explicitly, because the package names all end in .dev and invite
the opposite reading. Thirteen packages in this PR install under a dev prover
but against released mathcomp 2.6.0: coq- and rocq- × {mathcomp-analysis,
mathcomp-analysis-stdlib, mathcomp-classical, mathcomp-experimental-reals,
mathcomp-reals, mathcomp-reals-stdlib}, plus coq-mathcomp-word.dev.
Identically on 4.14.2 and 5.3.0.

This is not a solver preference — mathcomp dev was never permitted. One
ceiling drives twelve of the thirteen:

rocq-mathcomp-classical.dev:  "rocq-mathcomp-algebra" { (>= "2.6.0" & < "2.7~") }

dev sorts above 2.7~, so the release is the only candidate, and
{= version} locks propagate it across the monorepo split (algebra → order, finite-group → boot; ssreflect.dev needs boot and order at dev, a
contradiction, so it too takes 2.6.0). The whole analysis family then funnels
into classical by {= version}. The thirteenth is independent —
coq-mathcomp-word.dev's own coq-mathcomp-ssreflect {(>= "2.4" & < "2.7~")}.

The control that distinguishes "not permitted" from "not preferred": in the
same plans, every mathcomp package carrying no ceiling — finmap,
bigenough, reals, analysis — resolved dev. And mathcomp 2.6.0 can sit
beside a dev prover at all because it is the first release to drop the cap:
rocq-mathcomp-boot.2.5.0 has rocq-core {>= "9.0" & < "9.2~"}, 2.6.0 has
rocq-core {>= "9.0"}.

These remain real greens for the claim this PR makes — the prover is master.
They are simply silent about mathcomp master. Widening those ceilings is
deliberately not in this PR: permitting dev would make the solver select it
(per the control above), so the next run would test analysis-at-master against
mathcomp-at-master, a configuration nothing in this dataset has ever exercised.
That change belongs in #3812, where an untested configuration is the point.

Six packages here did exercise mathcomp dev: coq-/rocq-mathcomp-multinomials,
coq-/rocq-mathcomp-real-closed, coq-graph-theory, coq-graph-theory-planar.

Lower bounds on non-prover dependencies are untouched. Two recipes are
deliberately left unedited and are still unsafe: coq-record-update.dev
(coq-core {(>= "8.17" & < "9.3") | (= "dev")}, which admits 8.17–9.2 and on
the 4.09 job selected coq-core 8.20.dev) and rocq-mathcomp-multinomials.dev
(rocq-core {>= "9.0"}). Both files carry the header "This file was generated
from meta.yml, please do not edit manually", so the fix belongs upstream in
the generator, not here. Flagging rather than fixing them is the deliberate
choice; a disjunction that merely permits dev is a menu, not a pin, and the
solver is free to take the numeric branch.

Renames and conflicts

Renaming only ever goes coq- → rocq-, never the other way.

Twelve packages here have been renamed upstream — aac-tactics, libhyps,
pil, relation-algebra, and the eight mathcomp-analysis packages — and are
released under rocq-* while extra-dev had only coq-*. Two recipes for the
same logpath cannot coexist, so the last commit gives all twelve the
arrangement this archive already uses for coq-mathcomp-finmap,
coq-mathcomp-bigenough and coq-hierarchy-builder: coq-X.dev becomes a
metadata-only compatibility package whose whole content is
depends: ["rocq-X" {= version}], and rocq-X.dev declares
conflicts: ["coq-X" {!= version}] — which still excludes the released
coq-X builds but admits the shim.

Eight of the shims (the math-comp/analysis family) are upstream's own in-tree
coq-X.opam verbatim, minus the version: line. The other four
(aac-tactics, libhyps, pil, relation-algebra) ship none upstream and are
synthesised from the rocq-X metadata; coq-pil.dev did not exist here at all
and is new. Five blanket conflicts: ["coq-X"] added earlier in the branch are
narrowed to {!= version} by that commit; the seven whose upstream file
already carries a version-scoped conflict ({< "1.16~"}, {<= "2.4.0"}) are
untouched, since those already admit a dev shim.

Also verified

Every recipe passes opam lint --warn=-21 --check-upstream, the exact check
scripts/opam-coq-lint runs. Every git URL and branch was resolved against the
forge.

Three small drive-by fixes, all flagged by lint: dev-repo: filled in for
rocq-induction and strict-order-solver; coq-ordinal's license normalised
from "MIT License" to the SPDX "MIT"; and the mis-cased
name: "Coq-Kruskal-Trees" fields dropped (the directory already names the
package).

One correction to what this PR said before the split: it claimed every
{= version} dependency resolved to a package with a dev recipe. That was
wrong — rocq-typed-extraction{,-plugin}.dev depend on
rocq-elm-extraction {= version} and rocq-rust-extraction {= version},
neither of which had a dev recipe anywhere, so both were unsatisfiable on all
three compilers. All four packages are in #3812, whose last commit adds the two
missing recipes.

🤖 Generated with Claude Code

https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b

[JasonGross]

CI says:

• Packages that succeeded to install: coq-aac-tactics.dev coq-bedrock2-compiler.dev coq-coinduction.dev coq-color.dev coq-graph-theory-planar.dev coq-graph-theory.dev coq-hol-light-real-with-N.dev coq-hol-light-real-with-nat.dev coq-kruskal-almostfull.dev coq-kruskal-fan.dev coq-kruskal-finite.dev coq-kruskal-higman.dev coq-kruskal-theorems.dev coq-kruskal-trees.dev coq-kruskal-veldman.dev coq-libhyps.dev coq-mathcomp-analysis-stdlib.dev coq-mathcomp-analysis.dev coq-mathcomp-classical.dev coq-mathcomp-experimental-reals.dev coq-mathcomp-multinomials.dev coq-mathcomp-real-closed.dev coq-mathcomp-reals-stdlib.dev coq-mathcomp-reals.dev coq-mathcomp-word.dev coq-ordinal.dev coq-record-update.dev coq-relation-algebra.dev coq-tlc.dev rocq-aac-tactics.dev rocq-cakeml-extraction.dev rocq-coinduction.dev rocq-color.dev rocq-induction.dev rocq-libhyps.dev rocq-listz.dev rocq-mathcomp-analysis-stdlib.dev rocq-mathcomp-analysis.dev rocq-mathcomp-classical.dev rocq-mathcomp-experimental-reals.dev rocq-mathcomp-multinomials.dev rocq-mathcomp-real-closed.dev rocq-mathcomp-reals-stdlib.dev rocq-mathcomp-reals.dev rocq-relation-algebra.dev rocq-typed-extraction-common.dev strict-order-solver.dev
• Packages that failed to install: coq-ctree.dev coq-hol-light.dev coq-infotheo.dev coq-mathcomp-cad.dev coq-pil.dev coq-pprint.dev coq-sflib.dev coq-ssprove.dev coq-trocq-hott-examples.dev coq-trocq-hott.dev coq-trocq-std-examples.dev coq-trocq-std.dev coq-vcfloat.dev coq-vst-lib.dev rocq-categories.dev rocq-ceres-bytestring.dev rocq-concert-examples.dev rocq-concert.dev rocq-elpi-json.dev rocq-elpi-xml.dev rocq-hollight-logic-unif.dev rocq-hollight-logic.dev rocq-infotheo.dev rocq-laproof.dev rocq-marble.dev rocq-mathcomp-hollight-real-with-N.dev rocq-num-analysis-lebesgue.dev rocq-num-analysis-subset.dev rocq-num-analysis.dev rocq-partial-orders.dev rocq-pil.dev rocq-robot-rocq.dev rocq-rouche-capelli.dev rocq-sims.dev rocq-ssprove.dev
• Packages that were not compatible with the current compiler: rocq-navi.dev rocq-num-analysis-algebra.dev
• Packages that can never be installed: rocq-num-analysis-fem.dev rocq-num-analysis-lax-milgram.dev rocq-typed-extraction-plugin.dev rocq-typed-extraction.dev