ANN: (docker-coq: Bump to Debian 11) & (docker-coq-action: Remove `ocaml_version: "minimal"`)

Announcements
1

TL;DR: if you use docker-coq images and (install Debian packages manually or use the docker-coq-action with ocaml_version: "minimal"), then you could be impacted by the upgrade planned on next Monday 2022-06-27.

Up to now, all changes done in docker-coq and docker-coq-action repositories have been done with a special focus on backward compatibility.

However, two upcoming changes might impact Docker-based CI scripts in some corner cases, while these changes appear necessary, and should rather be seen as “fixes”.

Hence this post to let you know about these two changes in advance, before the corresponding two PRs are merged (after Monday 2022-06-27 next week).

docker-coq: Bump to Debian 11

Since the beginning, all docker-coq and docker-mathcomp images are based on Debian 10, which is now the oldstable distribution of Debian.

We would like to bump the base image of all docker-coq / docker-mathcomp images to debian:11-slim → PR coq-community/docker-base#20

But coq projects maintainers that manually install APT packages in their CI script (see Related docs below) may be impacted if a necessary package was available in Debian 10, but not in Debian 11.

Please, let us know in this Discourse thread by next Monday 2022-06-27 if you think you are in this case.

Related docs

If need be, see also:

docker-coq-action: Remove ocaml_version: "minimal"

As the docker-coq-action is intended to act as a GHA facade (to simplify the CI testing of opam projects using a Docker-Coq image or a custom one), and as the mapping between valid coq_version and ocaml_version already is the responsibility of the Docker-Coq registry, it appears irrelevant to also maintain one similar mapping in docker-coq-action’s entrypoint.sh.

Hence the decision to stop supporting the value ocaml_version: "minimal" within the docker-coq-action → PR coq-community/docker-coq-action#75

As of today, this setting is still available but raises a warning as a so-called GitHub Actions annotation:

image
image1445×138 27.6 KB

This warning will become an error once the PR above is merged (after Monday 2022-06-27).

Side remarks

  • To avoid the warning, ocaml_version: "minimal" can just as well be emulated with:

    - uses: coq-community/docker-coq-action@v1
  with:
    ocaml_version: "4.05"
      # for 8.10 <= coq_version <= 8.15
      #
      # or:
      #
    ocaml_version: "4.09-flambda"
      # for coq_version >= 8.16

  • At the time this announcement is posted, only one GitHub public repository appears to rely on "minimal"; but several GitHub private repositories might be impacted as well!

  • Finally, it can be noted that the docker-coq-action now supports a similar, but more useful setting ocaml_version: "default", to directly rely on Docker-Coq’s default tag, see e.g.:

2

ocaml_version: “4.09-flambda”

Why flambda?

3

@SkySkimmer
because all Docker-Coq images actually have +flambda enabled in the underlying opam switch,
except for ocaml 4.02, 4.05 (which were too old to support the option), and
except for …-native Docker-Coq images (because some performance issues had been spotted combining coq-native and flambda)

4

After the merge of PR coq-community/docker-base#20, the images of the four Docker Hub repos below now all(§) come with Debian 11, as well as with the latest release of dune.3.3.1:

(§) except for coqorg/coq:8.5.3-ocaml-4.02.3 for the time being, because of an opam build issue to be investigated.