Stream: Coq devs & plugin devs

Topic: CI docker images?


view this post on Zulip 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

)

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jason Gross (Sep 17 2020 at 23:16):

I guess I could switch from GH Actions to GitLab?

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.htmlhttps://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:

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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:

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

view this post on Zulip Jason Gross (Sep 19 2020 at 00:42):

@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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

  1. the docker-coq-action runs inside a container, which implies its filesystem is isolated from the runner, except the specified bind-mount (cf. https://github.com/coq-community/docker-coq-action/blob/89fce4f8c51c06b8e2fe3dfbf9e6f9a55a6c74dc/entrypoint.sh#L150). This means (i) the installed opam packages that are put in /home/coq/.opam are "lost" when docker-coq-action terminates; but (ii) all the files you put in /github/workspace (which is the initial current-working-directory in custom_script) are kept.
  2. there might be a permission mismatch issue if you don't use 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: Dec 07 2023 at 06:38 UTC