Refinement-based game semantics

Setup

1. Clone this project and its submodules,

git clone --recurse-submodules git@github.com:CertiKOS/rbgs.git

2. Create a local switch and install all dependencies using opam,

cd rbgs
opam switch create ./

3. Load local switch into environment variables,

eval $(opam env)

4. Our configure script will take care of retreiving the git submodule for Coqrel and CompCertO, and will configure them:

./configure

At this point make sure there were no error messages. In particular if your versions of Coq, Menhir, etc. are not suitable to build CompCert, this is when things will break.

5. If the configuration was successful you should be able to build the development using make. We recommend using the -jN option to enable parallel jobs as CompCert will take a while to build otherwise. For example on my 8-cores machine:

make -j8