Install/Build

There are three distinct possibilities:

1) Docker image

You can download the Docker image using this link (md5sum: 94f7ec5bc7ba16abd907fdf714742c70) After unziping it, load and start the image with:

docker load -i celsius.tar
docker run -it celsius

Inside the container, go to the celsius directory (with cd celsius).

You need to have opam installed. First, you can clone the project with

git clone https://github.com/clementblaudeau/celsius
cd celsius

Then, just run (~15 minutes as it recompiles Coq and rechecks the proofs):

opam switch create ./

First, you can clone the project with

git clone https://github.com/clementblaudeau/celsius
cd celsius

Then, just run (~5/10 minutes):

make Makefile.coq
make -j 4

In all cases, you should be able to run the following commands (in the celsius directory):

coqtop -Q src Celsius

And then:

From Celsius Require Import Soundness.
Check Soundness.
Print Assumptions Soundness.