Home

Docker-Coq images

This GitHub repository contains definitions of Docker images of the Coq proof assistant. These images are automatically built by GitLab CI and stored in the Docker Hub coqorg/coq repository.

The content of these images is summarized below. Details regarding the use of these images are provided in the CI setup and CLI usage pages.

The Docker-Coq images are based on Debian 11 Slim and contain 17 essential APT packages (specified in the Dockerfile from the GitHub docker-base repository).

All images have coq as default user with UID = GID = 1000, along with sudo permissions.

Relying on the OCaml package manager opam 2.0, Coq is installed in a single opam switch.

A Docker image is provided for:

the development version of Coq (automatically built after each push to coq@master) via coqorg/coq:dev,
if applicable, the alpha version of Coq (nightly built from 00:00 UTC) via coqorg/coq:…-alpha,
the last patchlevel of each release (since Coq 8.4.6) via coqorg/coq:$VERSION.

The commit reference associated to coqorg/coq:dev is given by a Docker label org.label-schema.vcs-ref, mentioned in the Docker Hub tags explorer.

By convention, the coqorg/coq:latest image (or more succinctly coqorg/coq) always refers to the latest stable version of Coq:

For convenience, some synonymous image tags are also provided (e.g., coqorg/coq:8.4 for coqorg/coq:8.4.6) as summarized in the table below.

Supported tags

How to inspect a tag

One can always inspect the contents of a Docker image remotely (without running docker pull $IMAGE_TAG; docker inspect $IMAGE_TAG).

It suffices to use the following service: https://explore.ggcr.dev/?image=$IMAGE_TAG

e.g., https://explore.ggcr.dev/?image=coqorg/coq:dev

Then, click on the first link in config.digest.

For example, on 2023-09-06 at 14:40 UTC+2, the link at stake is

https://explore.ggcr.dev/?blob=coqorg/coq@sha256:0742feff0a3070e85cf959928f243299dba037e5b17e023de15f7d2288be03ce&mt=application%2Fvnd.docker.container.image.v1%2Bjson&size=11441&manifest=coqorg/coq:dev@sha256:9851c78167e328012f84e28a8f8a35f5902a8b0e957040babdf9575581267595

and it shows the following JSON:

{
  "config": {
    "ArgsEscaped": true,
    "Cmd": [
      "/bin/bash",
      "--login"
    ],
    "Entrypoint": [
      "opam",
      "exec",
      "--"
    ],
    "Env": [
      "PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin",
      "OPAM_VERSION=2.1.3",
      "NJOBS=2",
      "OPAMPRECISETRACKING=1",
      "COMPILER=4.13.1+flambda",
      "OCAMLFIND_VERSION=1.9.6",
      "DUNE_VERSION=3.9.1",
      "ZARITH_VERSION=1.12",
      "COQ_EXTRA_OPAM=coq-bignums",
      "COQ_VERSION=dev"
    ],
    "Labels": {
      "maintainer": "erik@martin-dorel.org",
      "org.label-schema.build-date": "2023-09-06T11:04:14Z",
      "org.label-schema.description": "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.",
      "org.label-schema.name": "The Coq Proof Assistant",
      "org.label-schema.schema-version": "1.0",
      "org.label-schema.url": "https://coq.inria.fr/",
      "org.label-schema.vcs-ref": "afaecfd",
      "org.label-schema.vcs-url": "https://github.com/coq/coq",
      "org.label-schema.vendor": "The Coq Development Team",
      "org.label-schema.version": "dev"
    },
    "OnBuild": null,
    "Shell": [
      "/bin/bash",
      "--login",
      "-o",
      "pipefail",
      "-c"
    ],
    "User": "coq",
    "WorkingDir": "/home/coq"
  },
  "…": "…"
}

which notably includes the SHA1 of the underlying coq.master commit: afaecfd.

High-level summary of the Docker-Coq images

See the remarks above for details on the semantics of coqorg/coq:dev and coqorg/coq:latest.
All images contain opam-depext and a pinned version of the opam packages ocamlfind, dune, zarith, num, and coq.
Images for coq ≥ 8.6 contain the opam package coq-bignums (which was part of coq's stdlib for 8.4 ≤ coq ≤ 8.5).
Images for 8.8 ≤ coq < dev and ocaml ≥ 4.07 contain the opam package coq-serapi (useful for Alectryon).
The naming convention for all images is: coqorg/coq:$COQ_VERSION-ocaml-$OCAML_VERSION where:
- $COQ_VERSION is a two-place version number (e.g., 8.15), latest, or dev.
- $OCAML_VERSION correspond to the "base" image, tagged coqorg/base:$OCAML_VERSION.
- The possible values of $OCAML_VERSION depend on $COQ_VERSION, according to the correspondence below.
If the suffix -ocaml-$OCAML_VERSION is omitted:
- The image coqorg/coq:$COQ_VERSION contains the "default" ocaml version, mentioned below as well.

`coq-native` tags

Images for 8.5 ≤ coq ≤ 8.12 also contain the opam package coq-native (see the CEP 48 for details).
For coq ≥ 8.13, dedicated images are distributed with the coq-native package (given "item 2" of CEP 48 only deals with Coq ≥ 8.13).
The naming convention for coq ≥ 8.13 images with coq-native is coqorg/coq:$COQ_VERSION-native where:
- $COQ_VERSION is a two-place version number (e.g., 8.13), latest, or dev.
- This image contains the "default" ocaml version (without flambda).

For example:

# coqorg/coq:dev-native
# coqorg/coq:latest-native
# coqorg/coq:8.13-native

OCaml-versions policy

The policy for choosing the available OCaml versions can be phrased as follows.

Each Coq version will be prebuilt with four different OCaml versions:

OCaml 4.09.1 (the minimal version for Coq ≥ 8.16)
| OCaml 4.05.0 (the minimal version for 8.10 ≤ Coq ≤ 8.15),
OCaml 4.13.1+flambda (the "default" version for Coq ≥ 8.16)
| OCaml 4.07.1+flambda (the "default" version for 8.7 ≤ Coq ≤ 8.15),
The last two compatible versions (e.g., for Coq 8.15.2: OCaml 4.14.0+flambda & 4.13.1+flambda)

NOTE:
Docker-Coq thus tracks the last two compatible versions of OCaml for each Coq version, so if a new OCaml is released and compatible with this Coq version, the ante-penultimate compatible OCaml won't be available anymore.

This results in the following correspondence, which has been automatically generated:

* Coq dev: 
      # coqorg/coq:dev
      default: ['4.13.1-flambda']
      # coqorg/coq:dev-ocaml-4.14-flambda etc.
      base: ['4.14.0-flambda', '4.13.1-flambda', '4.12.1-flambda', '4.09.1-flambda']
* Coq 8.16.0: 
      default: ['4.13.1-flambda']
      base: ['4.14.0-flambda', '4.13.1-flambda', '4.12.1-flambda', '4.09.1-flambda']
 * Coq 8.15.2: 
      default: ['4.07.1-flambda']
      base: ['4.14.0-flambda', '4.13.1-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.14.1: 
      default: ['4.07.1-flambda']
      base: ['4.14.0-flambda', '4.13.1-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.13.2: 
      default: ['4.07.1-flambda']
      base: ['4.14.0-flambda', '4.13.1-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.12.2: 
      default: ['4.07.1-flambda']
      base: ['4.11.2-flambda', '4.10.2-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.11.2: 
      default: ['4.07.1-flambda']
      base: ['4.11.2-flambda', '4.10.2-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.10.2: 
      default: ['4.07.1-flambda']
      base: ['4.09.1-flambda', '4.08.1-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.9.1: 
      default: ['4.07.1-flambda']
      base: ['4.09.1-flambda', '4.08.1-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.8.2: 
      default: ['4.07.1-flambda']
      base: ['4.09.1-flambda', '4.08.1-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.7.2: 
      default: ['4.07.1-flambda']
      base: ['4.09.1-flambda', '4.08.1-flambda', '4.07.1-flambda', '4.05.0']
 * Coq 8.6.1: 
      default: ['4.02.3']
      base: ['4.02.3']
 * Coq 8.5.3: 
      default: ['4.02.3']
      base: ['4.02.3']
 * Coq 8.4.6: 
      default: ['4.02.3']
      base: ['4.02.3']

Some hyperlinks of related discussions:

You can browse the corresponding images on Docker Hub to see their labels, or click on the badge below and follow the "Supported tags and respective Dockerfile links" to obtain the source Dockerfiles.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Home

Docker-Coq images

Supported tags

How to inspect a tag

High-level summary of the Docker-Coq images

`coq-native` tags

OCaml-versions policy

Clone this wiki locally

Home

Docker-Coq images

Supported tags

How to inspect a tag

High-level summary of the Docker-Coq images

coq-native tags

OCaml-versions policy

Clone this wiki locally

`coq-native` tags