Version française

Installing Pcoq from the sources in Unix

To install pcoq from the software sources, you need to make sure you are able to re-compile it. For this you need:

1. The adequate version of ocaml,
2. The adequate version of the Java Development Kit,
3. A "local" installation of the Coq system (beware that this kind of installation is different from the one provided by default by the Coq developer's team).

What we mean by "adequate versions" varies from one version of Coq and Pcoq to the other. For pcoq-1.4 and Coq version 7.4, the adequate version of ocaml is 3.06, the adequate version of java is 1.4 (but 1.3 is enough or 1.3.1rc1 if you are using a non-US keyboard).

Compiling Coq

Beware that an incorrect installation of Coq is the most frequent reason for failing to compile or run pcoq. Moreover, default installations of Coq, as they can be obtained from the binary distributions made by the Coq team are not adapted to working with pcoq. For this reason, it is often better to re-compile Coq with the indications provided in this documentation.

Constructing a local installation of the Coq system is a bit difficult, especially since the Coq documentation is a bit erroneous on this aspect. As mentioned in the Coq installation file, one should call the coq configure command with the -local option, but one should never (repeat: never) proceed beyond step 5 of that installation documentation to get a local installation.

The commands to run are the following ones:

PATH=/usr/local/ocaml-3.06/bin:/usr/local/jdk1.4/bin:$PATH
tar xfz coq-7.4.tar.gz
cd coq-7.4
./configure -local
make world
cd ..

Compiling Pcoq

Once coq has been installed, you should add its binary directory in front of you Unix path variable and proceed with the installation of pcoq.

1. Extract the sources from the compressed tar archive.
2. Change directory to the pcoq directory that was created by the extraction.
3. Call the configure command.
4. Call gmake depend, then gmake world.

If anything fails, make sure you call gmake depend and gmake clean before any new try at re-compiling the system.

The commands to run are the following ones:

PATH=$(coq-7.2/bin/coqtop -where)/bin:$PATH
tar xfz pcoq.tgz
cd pcoq
./configure
make depend
make world

Using pcoq

The command to run pcoq is found in the directory bin and is called pcoq. It can be copied where you want, for example in /usr/local/bin, as long as the directory where you ran the compilation does not move. If you modify the ml files provided with the pcoq distribution and want the effect of your changes to be taken into account, you need to call this command with the option -local. For instance, you can type

bin/pcoq -local IntroductionEnglish.v