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:
site = ftp.inria.fr
dir = lang/caml-light
file = ocaml-3.0*.tar.gz
site = www.lama.univ-savoie.fr
or
site = ftp.logique.jussieu.fr
dir = pub/distrib/phox/current/
file = phox-0.xxbx.tar.gz
gunzip phox-0.xxbx.tar.gz; tar xvf
phox-0.xxbx.tar
) PHOXPATH
variable, for instance like
this (with csh): setenv PHOXPATH /usr/local/lib/phox/lib:$USERS/phox/examples
http://www.proofgeneral.org/~proofgen
Proof-General works better with xemacs, but pre-releases 3.4 works reasonably well with gnu-emacs 21.