Installation.

You can read up-to-date instructions at the following url :

http://www.lama.univ-savoie.fr/~raffalli/phox.html

We will explain how to install on a Unix machine. If you are familiar with Objective-Caml, it should not be difficult to get it work on any machine which can run Objective-Caml.

To install the `` Proof Checker'', proceed as follow:

1. Get and install Objective-Caml version 3.0* (at least 3.08). You can get it by ftp:

   site = ftp.inria.fr
   dir = lang/caml-light
   file = ocaml-3.0*.tar.gz

2. Get the latest version of by ftp :

   site = www.lama.univ-savoie.fr
   or
   site = ftp.logique.jussieu.fr
   dir = pub/distrib/phox/current/
   file = phox-0.xxbx.tar.gz

3. Uncompress it and detar it (using gunzip phox-0.xxbx.tar.gz; tar xvf phox-0.xxbx.tar)

4. Move to the directory phox-0.xxbx which has just been created.

5. Edit the file "./config", to suit you need.

6. Type "make".

7. Type "make install"

8. If you want the program to look for its libraries in more than one directory, you can set the PHOXPATH variable, for instance like this (with csh):

   setenv PHOXPATH /usr/local/lib/phox/lib:$USERS/phox/examples
   

9. You are strongly encouraged to use the emacs interface to . To install an emacs-mode, use Proof-General (release 3.3 or greatest) from:

   http://www.proofgeneral.org/~proofgen

   Proof-General works better with xemacs, but pre-releases 3.4 works reasonably well with gnu-emacs 21.