mit-plv / bedrock

The BEDROCK Coq library
Mostly automated verification of higher-order programs with higher-order separation logic, with a small trusted code base
http://plv.csail.mit.edu/bedrock/


This release requires Coq 8.4pl2.

To build, run one of the following:
   make native
or
   make ltac
to select whether to use the OCaml or Ltac reification code, respectively.
By default, you get the Ltac version, which is _much_ slower (i.e., adds hours to the time to build the library and all examples serially), but avoids the need to load a plugin into Coq, which can be tricky to do on some platforms.

Then, just run (one of the two):
(1)
   make
and go take a break while it runs for an hour or so (if you're lucky enough to have a new-ish machine). ;)  Using the '-j' switch for parallel build is highly recommended.

(2) Or:
   make cito
(no need to run "make" beforehand) to make the Cito compiler.

To make executable Cito example programs, see 'Bedrock/Platform/Cito/README'.
Also see the 'Examples', 'Platform', 'Platform/Cito', and 'Platform/Facade'
subdirectories of 'Bedrock/', and their READMEs.