Jason Gross (Sep 17 2020 at 22:47): Jason Gross (Sep 17 2020 at 22:47):How do I make use of the base docker images used for building Coq on the gitlab CI? (I want to do this for https://github.com/coq/bot/issues/107, getting coqbot to automatically minimize CI failures into test-suite cases. I was previously running the script to build the docker image myself, but the script that was previously working now reliably fails for me with
[ERROR] The sources of the following couldn't be obtained, aborting:
- ocamlgraph.1.8.8: curl error code 403
)
Erik Martin-Dorel (Sep 17 2020 at 23:02):@Jason Gross I don't know exactly the details of your use case(?), but maybe you could be interested in one of these pointers:
https://github.com/coq-community/docker-coq/wiki/CI-setup#gitlab-ci-config − https://github.com/coq-community/templates/issues/25 (to use existing images of coqorg/coq in a GitLab CI config)
https://coq-workshop.gitlab.io/2020/slides/Coq2020_02-02-docker-slides.pdf − https://gitlab.com/erikmd/docker-keeper-template (to make GitLab CI build and deploy your own images to Docker Hub)
Erik Martin-Dorel (Sep 17 2020 at 23:03):anyway feel free to post a link to a test you performed, I'll try to have a look tomorrow or this WE
Jason Gross (Sep 17 2020 at 23:12):@Erik Martin-Dorel I'm looking for something to replace the top lines of coqbot-ci.sh in https://github.com/coq-community/run-coq-bug-minimizer/pull/3/files with. I've never actually used docker before, so I don't really know how to write anything for it. I don't think GitHub actions includes special support for it (and if it does, I'm not sure I can make effective use of it, since the base image needs to be matched to the one that was used to build a particular PR (i.e., needs to be up to date), so I'm not sure how to load up a docker container from a script.
Jason Gross (Sep 17 2020 at 23:16):I guess I could switch from GH Actions to GitLab?
Jason Gross (Sep 17 2020 at 23:18):But note also that I think I need access to the images such as $CI_REGISTRY_IMAGE:bionic_coq-V2020-08-28-V92; are these publicly accessible? (Also, what is $CI_REGISTRY_IMAGE?)
Jason Gross (Sep 17 2020 at 23:21):Note also that I also need to be able to upload files generated within the docker container to an artifact via GH Actions or whatever
Théo Zimmermann (Sep 18 2020 at 07:27):The Docker images that you need are the Coq's CI ones and not the Docker-Coq ones.
Théo Zimmermann (Sep 18 2020 at 07:27):We are using the GitLab container registry to store them, so this is where you need to look for them.
Théo Zimmermann (Sep 18 2020 at 07:28):It is possible to run Docker containers on GH Action. This is basically what Docker-Coq-Action does.
Théo Zimmermann (Sep 18 2020 at 07:35):To be more specific, the Docker-Coq-Action runs a base Docker image containing Docker (https://github.com/coq-community/docker-coq-action/blob/master/Dockerfile) and invokes the docker command to load the right Docker-Coq image (https://github.com/coq-community/docker-coq-action/blob/89fce4f8c51c06b8e2fe3dfbf9e6f9a55a6c74dc/entrypoint.sh#L149-L151).
Erik Martin-Dorel (Sep 18 2020 at 19:59):Hi @Jason Gross, indeed as pointed out by @Théo Zimmermann:
(1) you need to use the Coq images from GitLab CI registry (https://gitlab.com/coq/coq/container_registry), not the Docker-Coq images in Docker Hub; and this requirement does not imply your "script" also runs in GitLab CI: it can just as well be run in GitHub Actions' CI, or even locally in your workstation if you have Docker installed. (and CI_REGISTRY_IMAGE is a variable documented here: https://docs.gitlab.com/ee/ci/variables/predefined_variables.html − https://docs.gitlab.com/ee/ci/variables/README.html#list-all-environment-variables)
So, you can just do:
docker pull registry.gitlab.com/coq/coq:bionic_coq-V2020-08-28-V92
docker run --rm -it registry.gitlab.com/coq/coq:bionic_coq-V2020-08-28-V92
for more details on the Docker CLI commands, see e.g. this wiki page: https://github.com/coq-community/docker-coq/wiki/CLI-usage
(2) GitHub Actions natively support Docker, but in two ways:
docker run commands are transparently handled by the container action in the background, so that we don't actually need write any docker command) → see e.g. the Coq-Workshop example (https://gist.github.com/erikmd/6d4af38edcf6e8a6ce3207304d74300b)run: command → even if leads to a more low-level, verbose and less readable workflow file (so it is not recommended for usual Coq-projects CI configurations), I guess it might be better suited for your use case, as it seems you need to build/run two Docker images at the same time, and compare them. I'll try to come up with a sample configuration to give you more hints, and I'll post it in this Zulip thread. Jason Gross (Sep 18 2020 at 20:19):I don't plan to ever run two docker images at once. However, different branches will run different docker images, and the workflow will be simpler if I can load a docker image whose name is stored in some file, rather than having to edit the config file to change images. I'll take a look at the resources, thanks!
Erik Martin-Dorel (Sep 18 2020 at 20:25):Hi @Jason Gross
I don't plan to ever run two docker images at once.
OK. But you still want to do a comparison of two coq versions, in the same build, right?
as shown by these two lines in the link you posted:
https://github.com/coq-community/run-coq-bug-minimizer/pull/3/files#diff-82b3a23828303dab7c2a1ef3580c5605R60-R66
so IIUC your plan after you latest message:
you'd just want to spin a single Docker image taken from the GitLab CI registry (the base image), then in this image you'd run your Python script, mostly keeping the lines
https://github.com/coq-community/run-coq-bug-minimizer/pull/3/files#diff-82b3a23828303dab7c2a1ef3580c5605R60-R66
do you confirm?
Erik Martin-Dorel (Sep 18 2020 at 20:44):If yes, to follow-up my last-but-one message, I'd say that the docker-coq-action approach seems suitable for your use case (and writing docker run commands by hand would be unnecessary).
Also, you would probably be interested in these fields:
custom_script: (https://github.com/coq-community/docker-coq-action#custom_script)custom_image:(https://github.com/coq-community/docker-coq-action#custom_image)e.g.:
jobs:
example:
runs-on: ubuntu-latest
steps:
- name: Check out the repo
uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'dummy.opam'
custom_image: 'registry.gitlab.com/coq/coq:bionic_coq-V2020-08-28-V92'
custom_script: |
startGroup Example
echo ${{ github.ref }}
endGroup
startGroup Install APT dependencies
sudo apt-get update -y -q
sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q libgmp-dev # for example
endGroup Run test
./run.sh
endGroup
@Erik Martin-Dorel The docker-coq-action looks appealing. Are the files that are created within that script available for subsequent upload-artifact jobs? If not, is there a way to make them available, e.g., by copying them somewhere?
Jason Gross (Sep 19 2020 at 00:43):do you confirm?
That's almost right. Actually I want to keep more lines, namely https://github.com/coq-community/run-coq-bug-minimizer/pull/3/files#diff-82b3a23828303dab7c2a1ef3580c5605R27-R68 , so that I in fact get two copies of Coq
Théo Zimmermann (Sep 19 2020 at 09:50):Oh, nice idea to reuse Docker-Coq-Action with both a custom image and a custom script! There will need to be an intermediate step to read the right values for the custom image, but that's supported in GitHub workflows, right? The sudo apt-get install step will never be necessary as all the dependencies will already be available in the Docker image BTW.
Erik Martin-Dorel (Sep 20 2020 at 13:49):Jason Gross said:
Are the files that are created within that script available for subsequent upload-artifact jobs? If not, is there a way to make them available, e.g., by copying them somewhere?
Yes this is feasible, but there are two pitfalls to take into account:
/github/workspace (which is the initial current-working-directory in custom_script) are kept.opam install but manual coqc or so commands with a docker-coq image or another base image with a different convention than the GitHub Actions runner. This is documented in the README (https://github.com/coq-community/docker-coq-action#custom_script):Note-1: if you use the docker-coq images, the container user has UID=GID=1000 while the GitHub action workdir has (UID=1001, GID=116). This is not an issue when relying on opam to build the Coq project. Otherwise, you may want to use sudo in the container to change the permissions. […]
To give more details on how to workaround these two pitfalls, I've just pushed an example workflow that allows for artifact generation and upload (either using curl within the container, or running a subsequent workflow command with run:):
HTH
Last updated: May 28 2023 at 13:30 UTC