iRRAM-coq: Hoare logic for iRRAM in Coq
This repository contains the Coq development of a Hoare logic for iRRAM for supporting fearless verification.
The master branch is known to compile with:
The recommended way to build the development is using OPAM. To avoid conflicts with existing packages, we recommend to create a new opam switch:
opam switch iRRAM-coq --alias-of=4.04.0
It should work for any compiler version upwards of 4.04.0. After compiling OCaml, the new switch needs to be activated in your current shell. opam will print the necessary instructions.
To find all the dependencies of iRRAM-coq, opam needs to know about the Coq opam archive. This can be achieved by executing:
opam repo add coq-released https://coq.inria.fr/opam/released
make dep to install all dependencies of iRRAM-coq. Finally,
make to quickly compile the development, and
make build for fully
build the development.
opam install ocamlbuild batteries # install OCaml libraries ./run_ilog2.sh