/docker-coq-vst

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

Primary LanguageShellMIT LicenseMIT

docker-coq-vst

GitHub

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"

applied.fm