DopCert is a framework for formally verifying query optimization. Our website: http://dopcert.cs.washington.edu/.
Our coq code has been tested using HoTT library with Coq 8.5pl1. To save from building HoTT library and Coq, we recommend docker based development environment described below:
A detailed documentation could be found here.
Build project and call it dopcert
with:
docker build -t dopcert .
Run development environment named dopcert
with:
docker run -d --name dopcert -v $(pwd)/src/:/src/ dopcert sleep infinity
Build changes to the project with:
docker exec dopcert make -C src
Connect to the docker process with emacs and edit Coq files using ProofGeneral.
Emacs must have docker-tramp
installed, and enable-remote-dir-locals
enabled.
emacs /docker:dopcert:/hott/UnivalentSemantics.v
To connect to the docker process on another machine, run:
emacs "/ssh:user@machine|docker:dopcert:/hott/UnivalentSemantics.v"
Remove development environment with:
docker rm -f dopcert
Remove all old docker containers with:
docker rm -f $(docker ps -aq)