The bedrock from maximedenes

View Code? Open in Web Editor NEW

This project forked from jasongross/bedrock

Not necessarily up-to-date mirror of hg bedrock repository

License: Other

Emacs Lisp 0.01% Coq 98.22% Makefile 0.50% Assembly 0.37% C 0.42% Standard ML 0.05% OCaml 0.19% Verilog 0.22% Shell 0.01%

bedrock's Introduction

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.

Recommend Projects