Melocoton: a Coq model and separation logic for verified interoperability between OCaml and C
Building
You need to have opam >= 2.0 installed.
The simplest option is to create a fresh local opam switch with everything needed, by running the following commands:
opam switch create -y --repositories=default,iris-dev=git+https://gitlab.mpi-sws.org/iris/opam.git . ocaml-base-compiler.4.14.1
eval $(opam env)
Then run:
make
make html # optional, builds an html rendering of the sources
Troubleshooting
-
When visiting the artifact from a new terminal session, one needs to call opam to re-setup the terminal environment. To do this, call
eval $(opam env)from the root of the repository. -
If the
opam switchinvocation fails at some point, either remove the_opamdirectory and re-run the command (this will redo everything), or doeval $(opam env)and thenopam install -y .(this will continue from where it failed).
Browsing the development
An easy way to browse the development is to open html/toc.html
in a web browser after running make html. The webpage contains an HTML
rendering of the Coq scripts of the development.
Alternatively, using an IDE with Coq support is recommended.
Navigating the Coq development
- OVERVIEW.md describes the structure of the Coq development
- PAPER.md is a guide through the development following the paper
- NAMING.md describes the naming conventions followed through the Coq development