This repository provides parent images for Docker images of the Coq proof assistant.
These images are based on Debian 12 Slim:
| GitHub repo | Type | Docker Hub | |
|---|---|---|---|
| docker-coq-action | GitHub Action | N/A | |
| docker-rocq | Dockerfile | rocq/rocq-prover |
|
| ⊙ | docker-base | Dockerfile | rocq/base |
| ↳ | Debian | Linux distro | debian |
This Dockerfile repository is mirrored on GitLab, but issues and pull requests are tracked on GitHub.
Note
-
Note that these base images do not contain the Rocq Prover nor the Coq proof assistant.
They just contain a sudo user with UID=GID=1000 and /home/rocq or /home/coq as homedir,
as well as one opam switch, and some minimal apt and opam dependencies. -
The "bare" images do not contain any opam switch, just the opam binary.
-
The default entrypoint is
ENTRYPOINT ["opam", "exec", "--"]for all these images.