coqdep warnings default AsError#22253
Draft
SkySkimmer wants to merge 1 commit into
Draft
coqbot-app / GitLab CI job library:ci-vst (pull request)
failed
Jul 10, 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-07-06-62b9804f8c with OCaml 4.14.2+flambda and depended on jobs library:ci-compcert build:edge+flambda library:ci-stdlib+flambda library:ci-flocq library:ci-menhir. It built targets vst.
We show below an excerpt from the trace from GitLab starting around the last detected "Error" (the complete trace is available here).
Details
File "./msl/psepalg.v", line 9, characters 15-40:
Error: Unable to locate library
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 2005 matching artifact files and directories
Uploading artifacts as "archive" to coordinator... 201 Created correlation_id=01KX5NTRN1DR9KRTSDWQ1A37AY id=7598818 responseStatus=201 Created token=64_G9C6xm
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
Loading