Docker images of Coq (v. 8.4 to 8.20): a Rocq-community project
May 13, 2025 · View on GitHub
Note
This repository provides Docker images of the Coq proof assistant (versions 8.4.6 to 8.20.1), maintained as part of the Rocq-community project. Note that Docker tags for Coq versions < 8.7 are not actively rebuilt anymore, and thereby do not show up in the list of Supported tags below: these old Coq images are stalled because of this opam-repository PR that archived old versions of the OCaml compiler. For newest versions of the Rocq Prover ≥ 9.0, use rocq/rocq-prover images instead.
These images are based on this parent image, itself based on Debian 12 Slim and relying on the last version of opam 2.x:
| GitHub repo | Type | Docker Hub | |
|---|---|---|---|
| docker-coq-action | GitHub Action | N/A | |
| ⊙ | docker-coq | Dockerfile | coqorg/coq |
| ↳ | docker-base | Dockerfile | coqorg/base |
| ↳ | Debian | Linux distro | debian |
See also the docker-coq wiki for details about how to use these images.
This Dockerfile repository is mirrored on GitLab, but issues and pull requests are tracked on GitHub.