To build Vericert, the provided Makefile can be used. External dependencies are needed to build the
project, which can be pulled in automatically with nix using the provided
The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:
- Coq: theorem prover that is used to also program the HLS tool.
- OCaml: the OCaml compiler to compile the extracted files.
- dune: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.
- menhir: parser generator for ocaml.
- findlib to find installed OCaml libraries.
- GCC: compiler to help build CompCert.
These dependencies can be installed manually, or automatically through Nix.
Downloading CompCert #
CompCert is added as a submodule in the
lib/CompCert directory. It is needed to run the build
process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded
together with the repository. To clone CompCert together with this project, you can run:
git clone --recursive https://github.com/ymherklotz/vericert
If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:
git submodule update --init
Setting up Nix #
Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.
To open a shell which includes all the necessary dependencies, one can use:
which will open a shell that has all the dependencies loaded.
Makefile build #
If the dependencies were installed manually, or if one is in the
nix-shell, the project can be built
and installed locally, or under the
PREFIX location using:
Which will install the binary in
./bin/vericert by default. However, this can be changed by changing
PREFIX environment variable, in which case the binary will be installed in
To test out
vericert you can try the following examples which are in the test folder using the
./bin/vericert test/loop.c -o loop.v ./bin/vericert test/conditional.c -o conditional.v ./bin/vericert test/add.c -o add.v
Or by running the test suite using the following command: