Skip to content

Remove dynamic scheme generation - #22192

Open
SkySkimmer wants to merge 3 commits into
rocq-prover:masterfrom
SkySkimmer:noforce-scheme
Open

Remove dynamic scheme generation#22192
SkySkimmer wants to merge 3 commits into
rocq-prover:masterfrom
SkySkimmer:noforce-scheme

changelog

ff4f147
Select commit
Loading
Failed to load commit list.
coqbot-app / GitLab CI job plugin:ci-mtac2 (pull request) failed Jun 30, 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-06-10-0c389ac2f4 with OCaml 4.14.2+flambda and depended on jobs build:edge+flambda library:ci-stdlib+flambda. It built targets unicoq mtac2.

We show below an excerpt from the trace from GitLab starting around the last detected "Error" (the complete trace is available here).

Details

File "./theories/Pattern.v", line 196, characters 2-11:
Error:
Missing "rew_r" scheme for meq.
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...
_install_ci: found 18 matching artifact files and directories 
saved_build_ci: found 535 matching artifact files and directories 
Uploading artifacts as "archive" to coordinator... 201 Created  correlation_id=01KWC89AY4589FTAZ6KPGTFXDZ id=7531615 responseStatus=201 Created token=64_Sx2y7w
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1