README.md

docker-coq-vst

Docker images of the Coq proof assistant, with compcert and VST pre-installed.

Based on docker-coq. Compatible with docker-coq-action.

Docker Images

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

Building

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"