Build Instructions
==================

This directory contains the Coq files associated with the paper

    "Modular Enforcement of Information Flow
          Policies in Data Structures"

To compile the files, you need a recent version of the Ssreflect extension
to Coq.

Obtaining and installing Ssreflect
==================================

This code compiles with 
-Ssreflect version 1.3pl1; and 
-Coq V8.3pl1. 
It may also compile with more recent versions of Coq and Ssreflect.

To install Ssreflect-1.3pl1, download the sources at 

   http://www.msr-inria.inria.fr/Projects/math-components

unpack, and follow the instructions in the INSTALL and README files.

Compiling RHTT libraries and examples
=================================================

After installing ssreflect-1.3, go to the directory containing our
distribution and edit the paths in Make to point to your installation
of Ssreflect.  Alternatively, set the SSR environment variable to
point to the base of your Ssreflect installation.  (For interactive
execution of the Coq files in Proof General, edit loadpath.v in the 
distribution directory by updating <path-to-ssr-base> to point to
the root of your Ssreflect installation.) Then type

  coq_makefile -f Make -o Makefile
  make
