Bound dune < 3.24 on extra-dev packages still using the coq extension - #3802
Merged
coqbot-app / GitLab CI job opam-build:4.14.2 (pull request)
failed
Jul 31, 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 ###
# [...]
# File "./theories/ZornsLemma/Proj1SigInjective.v", line 1, characters 24-40:
# Error: Cannot find a physical path bound to logical path
# ProofIrrelevance with prefix Stdlib.
#
# (cd _build/default && /builds/coq/opam-repositories/opam-root-4.14.2-2.1.2-sandbox/4.14.2/bin/coqc -q -w -deprecated-hint-rewrite-without-locality -w -deprecated-instance-without-locality -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /builds/coq/opam-repositories/opam-root-4.14.2-2.1.2-sandbox/4.14.2/lib/coq/../rocq-runtime/plugins/btaut[...]
# File "./theories/ZornsLemma/Relation_Definitions_Implicit.v", line 1, characters 5-8:
# Warning: "From Coq" has been replaced by "From Stdlib".
# [deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
# File "./theories/ZornsLemma/Relation_Definitions_Implicit.v", line 1, characters 24-44:
# Error: Cannot find a physical path bound to logical path
# Relation_Definitions with prefix Stdlib.
#
The former state can be restored with:
/usr/local/bin/opam switch import "/builds/coq/opam-repositories/opam-root-4.14.2-2.1.2-sandbox/4.14.2/.opam-switch/backup/state-20260731020305.export"
'opam install coq-zorns-lemma.dev -y -v -v --with-test' failed.
Installed files:
[WARNING] Running as root is not recommended
[WARNING] Running as root is not recommended
Removing coq-zorns-lemma
[WARNING] Running as root is not recommended
[NOTE] coq-zorns-lemma is not installed.
Packages that succeeded to install: coq-ceres.dev coq-coqffi.dev coq-disel-examples.dev coq-disel.dev coq-gaia-numbers.dev coq-gaia-ordinals.dev coq-gaia-schutte.dev coq-gaia-stern.dev coq-gaia-theory-of-sets.dev coq-itree-extra.dev coq-itree.dev coq-quickchick.dev coq-simple-io.dev coq-tactician-dummy.8.6.dev
Packages that failed to install: coq-addition-chains.dev coq-gaia-hydras.dev coq-goedel.dev coq-huffman.dev coq-hydra-battles.dev coq-pocklington.dev coq-tactician-dummy.8.17.dev coq-tactician.8.13.dev coq-tactician.8.14.dev coq-tactician.8.15.dev coq-tactician.8.16.dev coq-tactician.8.17.dev coq-tactician.8.18.dev coq-tactician.8.19.dev coq-tactician.8.20.dev coq-tactician.dev coq-topology.dev coq-vlsm.dev coq-zorns-lemma.dev
Packages that were not compatible with the current compiler: coq-freespec-exec.dev coq-freespec-ffi.dev coq-tactician.8.11.dev coq-tactician.8.12.dev
Packages that can never be installed: coq-tactician.8.10.dev
Uploading artifacts for failed job
Uploading artifacts...
log/: found 39 matching artifact files and directories
Uploading artifacts as "archive" to coordinator... 201 Created correlation_id=01KYTYZTFNY60FAY4FHNQHS9FT id=7686663 responseStatus=201 Created token=64_de6CGi
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
Loading