Download MetaPRL

MetaPRL can be downloaded from ftp://ftp.cs.cornell.edu/pub/nuprl/MetaPRL/. You will need four packages:

  1. Objective Caml: our version contains a small patch to install interface files needed by MetaPRL to evaluate programs in the toploop and a native code profiler patch.
  2. CamlP4: our version contains a small patch to compile the CamlP4 distribution in native code.
  3. Ensemble: you need Ensemble only if you want to use the distributed prover.
  4. MetaPRL

All source modules are available as source, and RedHat 5.1 RPM packages files for Linux i386. There is also a Win32 distribution that we'll be placing online soon (if you don't see it contact Jason Hickey). You will need the Cygnus Systems GNU-Win32 distribution.

CVS sources

If you plan any development in MetaPRL, you may consider using the public CVS repository. This will allow you to have access to the latest changes in the distribution. The normal service is read-only, but if you would like to become a contributor with write access, contact Jason Hickey or Alexey Nogin.

The CVS server is on the machine ensemble01.cs.cornell.edu. First log into the server by running 

% cvs -d :pserver:anoncvs@ensemble01.cs.cornell.edu:/cvsroot login
The password is anoncvs. It will be stored on your computer, so you only have to run the login command once.

Now you can checkout the distribution by running:

% cvs -d :pserver:anoncvs@ensemble01.cs.cornell.edu:/cvsroot checkout MetaPRL
You can find more information on CVS at Cyclic Software's pages

Installation and configuration

To install OCaml and CamlP4, unpack the distributions. The INSTALL files describe the process of installation.

To install Ensemble, unpack the distrubution, and edit the <ensemble>/mk/config.mk file. You will want to use the Ensemble socket library (not the Unix socket implementation), then change directories to <ensemble>/def, and run make. You can also build the native-code libraries by running make in the <ensemble>/opt directory. More information on Ensemble is available at the Ensemble Home Page.

To install MetaPRL, unpack the distribution into some directory <meta-prl>. You need to set the environment variables CAMLLIB=<your ocaml lib directory>, and ENSROOT=<root of the ensemble source tree>. Then you can build the distribution with these steps:

% cd <meta-prl>
% make all
or
% make opt

The MetaPRL program is <meta-prl>/editor/ml/mp. You will need to install the "Nuprl font" to be able to interact with some sense. The Nuprl font is in <meta-prl>/editor/fonts/mp12.bdf. You'll get the best success if you use MetaPRL from a shell window within Emacs. You can start Emacs with the Nuprl font by running emacs -fn nl12.

That's it. To navigate the MetaPRL logics and programs, you will need to read the User Guide.