A modality-parametric weakest precondition theory for the Iris program logic framework in Coq.
The project can be built locally or by using the provided Dockerfile, see the Using Docker section for details on the latter.
The project is known to compile with:
- Coq 8.13.0
- Versions of Iris and std++ as specified in the modal-weakestpre.opam file
The dependencies can be obtained using opam; see this guide for how to install opam. To obtain the dependencies, you have to add the following repositories to the opam registry by invoking
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam update
Once you got opam set up, run make build-dep to install the right versions of
the dependencies.
Run make -jN to build the full development, where N is the number of CPU
cores on your machine.
Run make install to install the development as a local Coq package for use in
your own developments.
The development can be built using
Docker.
Run make docker-build to build Dockerfile and the development.
Documentation can be generated using
coqdoc by running make html. Afterwards, a table of contents is generated from which
the documentation can be accessed.