Docker images of the Coq proof assistant, with compcert and VST pre-installed.
Based on docker-coq. Compatible with docker-coq-action.
We currently maintain the following images:
| Image | Base | compcert variants | Provides |
|---|---|---|---|
| appliedfm/coq | coqorg/coq | (Base image) | |
| appliedfm/coq-compcert | appliedfm/coq | ✓ x86_64-linux ✓ x86_32-linux |
compcert |
| appliedfm/coq-vst | appliedfm/coq-compcert | ✓ x86_64-linux ✓ x86_32-linux |
compcert, VST |
| appliedfm/coq-vst-certigraph | appliedfm/coq-vst | ✓ x86_64-linux ✓ x86_32-linux |
compcert, VST, CertiGraph |
We provide pre-built images on Docker Hub, which means you probably do not need to build the images yourself. However, if you need a specific combination of versions that we do not provide, then your best bet is to build your own image.
$ source build.sh
$ build__coq "8.15.0"
$ build__coq_compcert "8.15.0" "3.10"
$ build__coq_vst "8.15.0" "3.10" "2.9"
$ build__coq_vst_certigraph "8.15.0" "3.10" "2.9"