-
Notifications
You must be signed in to change notification settings - Fork 665
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
coqorg/coq:dev
build is broken since yesterday: ideas to improve the process?
#19962
Comments
The culprit PR seems to be #19927 |
At first sight, the overlay mechanism is not straightforwardly applicable because Docker-Coq is not in Coq's CI (and it is rather the other way around). Otherwise a minimal and useful action would be to ping the Docker-Coq maintainers (@himito and me) when a Coq PR impacts *.opam files... Maybe, we could be added in the CodeOwners for *.opam files, so that we are aware of this even if the PR assignee forgets to ping us? WDYT? |
docker-keeper: rebuild-keyword: dev Related: coq/coq#19962
docker-keeper: rebuild-keyword: dev Related: coq/coq#19962
Reviewed-by: Zimmi48 Co-authored-by: Zimmi48 <[email protected]>
Description of the problem
Docker-Coq CI/CD build and Docker-Rocq CI/CD build for
dev
are broken since yesterday:https://gitlab.com/coq-community/docker-coq/-/pipelines
https://gitlab.com/coq-community/docker-rocq/-/pipelines
It is the third time it happens, typically because of a refactoring that impacts the *.opam files for Coq
(either those stored in the Coq repo itself, or this one in coq/opam)
and this is a bit annoying since it's more difficult to react quickly after-the-fact, so end users cannot benefit from an up-to-date
dev
image for some time.Given the renaming from Coq to Rocq is on-going and more infrastructure changes will come,
do you have ideas to improve the process?
Small Rocq / Coq file to reproduce the bug
No response
Version of Rocq / Coq where this bug occurs
dev
Last version of Rocq / Coq where the bug did not occur
No response
The text was updated successfully, but these errors were encountered: