Turn require Coq depr warnings as error by default - #21851
Closed
proux01 wants to merge 2 commits into
Closed
coqbot-app / GitLab CI job library:ci-riscv_coq (pull request)
failed
Apr 3, 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.
This job ran on the Docker image registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2026-03-19-ac6c1c9705 with OCaml 4.14.2+flambda and depended on jobs build:edge+flambda library:ci-coqutil library:ci-stdlib+flambda. It built targets riscv_coq.
We show below an excerpt from the trace from GitLab starting around the last detected "Error" (the complete trace is available here).
Details
File "/builds/coq/coq/_build_ci/riscv_coq/src/riscv/Utility/Monads.v", line 1, characters 15-49:
Error: "From Coq" has been replaced by "From Stdlib".
Running after_script
Running after script...
$ if { [ "$SAVE_BUILD_CI" ] || [ "$CI_COMMIT_REF_NAME" = master ] || ! [ -e ci-success ]; } && [ -d _build_ci ]; then mv _build_ci saved_build_ci; fi
$ dev/tools/list-potential-artifacts.sh > available_artifacts.txt
$ dev/tools/cleanup-artifacts.sh downloaded_artifacts.txt available_artifacts.txt
Uploading artifacts for failed job
Uploading artifacts...
WARNING: _install_ci: no matching files. Ensure that the artifact path is relative to the working directory (/builds/coq/coq)
saved_build_ci: found 4421 matching artifact files and directories
saved_build_ci/**/.git: excluded 11 files
saved_build_ci/**/.git/**/*: excluded 492 files
Uploading artifacts as "archive" to coordinator... 201 Created correlation_id=01KN9TV309XT1VE7EJKX3MJF1H id=7139065 responseStatus=201 Created token=64_x8uXoZ
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
Loading