extra-dev: add 46 dev recipes and update 5 more, for packages that do not yet install (on top of #3809) - #3812
Draft
JasonGross wants to merge 54 commits into
Draft
coqbot-app / GitLab CI job opam-build:5.3.0 (pull request)
failed
Aug 19, 2026 in 0s
Test has failed on GitLab CI
This job has failed. If you need to, you can restart it directly in the GitHub interface using the "Re-run" button.
We show below the last 40 lines of the trace from GitLab (the complete trace is available here).
Details
### output ###
# [...]
# CAMLDEP src/wGraph.mli
# CAMLC -c src/init0.mli
# CAMLC -c src/fin.mli
# ocamlfind: Package `coq-core.plugins.extraction' not found
# ocamlfind: Package `coq-core.plugins.extraction' not found
# make[2]: *** [RocqMakefile.plugin:769: src/init0.cmi] Error 2
# make[2]: *** Waiting for unfinished jobs....
# make[2]: *** [RocqMakefile.plugin:769: src/fin.cmi] Error 2
# make[1]: *** [RocqMakefile.plugin:423: all] Error 2
# make[1]: Leaving directory '/builds/coq/opam-repositories/opam-root-5.3.0-2.1.2-sandbox/5.3.0/.opam-switch/build/rocq-typed-extraction-plugin.dev/plugin'
# make: *** [Makefile:24: plugin] Error 2
# make: Leaving directory '/builds/coq/opam-repositories/opam-root-5.3.0-2.1.2-sandbox/5.3.0/.opam-switch/build/rocq-typed-extraction-plugin.dev/plugin'
The former state can be restored with:
/usr/local/bin/opam switch import "/builds/coq/opam-repositories/opam-root-5.3.0-2.1.2-sandbox/5.3.0/.opam-switch/backup/state-20260819100018.export"
'opam install rocq-typed-extraction.dev -y -v -v --with-test' failed.
Installed files:
[WARNING] Running as root is not recommended
[WARNING] Running as root is not recommended
Removing rocq-typed-extraction
[WARNING] Running as root is not recommended
[NOTE] rocq-typed-extraction is not installed.
Packages that succeeded to install: coq-coinduction.dev coq-color.dev coq-coqeal.dev coq-mathcomp-word.dev coq-record-update.dev coq-riscv.dev coq-ssprove.dev rocq-coinduction.dev rocq-color.dev rocq-elm-extraction.dev rocq-elpi-json.dev rocq-elpi-xml.dev rocq-mathcomp-boot.dev rocq-mathcomp-classical.dev rocq-mathcomp-finmap.dev rocq-mathcomp-multinomials.dev rocq-mathcomp-real-closed.dev rocq-rust-extraction.dev rocq-ssprove.dev rocq-stdpp.dev
Packages that failed to install: coq-ctree.dev coq-hol-light.dev coq-infotheo.dev coq-libvalidsdp.dev coq-mathcomp-cad.dev coq-pil.dev coq-pprint.dev coq-sflib.dev coq-trocq-hott-examples.dev coq-trocq-hott.dev coq-trocq-std-examples.dev coq-trocq-std.dev coq-validsdp.dev coq-vcfloat.dev coq-vst-lib.dev rocq-categories.dev rocq-ceres-bytestring.dev rocq-concert-examples.dev rocq-concert.dev rocq-ctree.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-partial-orders.dev rocq-pil.dev rocq-robot-rocq.dev rocq-rouche-capelli.dev rocq-sims.dev rocq-typed-extraction-plugin.dev rocq-typed-extraction.dev
Packages that were not compatible with the current compiler: rocq-navi.dev
Packages that can never be installed: rocq-num-analysis-algebra.dev rocq-num-analysis-fem.dev rocq-num-analysis-lax-milgram.dev rocq-num-analysis-lebesgue.dev rocq-num-analysis-subset.dev rocq-num-analysis.dev
Uploading artifacts for failed job
Uploading artifacts...
log/: found 61 matching artifact files and directories
Uploading artifacts as "archive" to coordinator... 201 Created correlation_id=01M0CRYASFDB6QGS3XCPGBPXP8 id=7747373 responseStatus=201 Created token=64_8MYbfa
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
Loading