Edit (March 13, 2018): all links to software from this page are now invalid, only the link to the proof by pointing article has been revived.
If you want a fast, hassle-free installation of pcoq to try it out, we suggest you download our setup file (10Mbytes) and execute it in a terminal window. For instance, you may have to execute the following commands:
/bin/sh setup
It will ask that you provide a directory or confirm the default choice and then perform a quick (and maybe dirty) installation of coq and pcoq so that you can try it out right away.
For users who already have Coq on their machine, beware that you need to use exactly Coq version 7.4 for this version of pcoq to run with it. If you have an older version, you may want to look at the older versions of pcoq too. Pcoq is simply available as a java archive in jar format, with a small shell script, in which three variables must be updated when it is installed. These files and the files describing copyright and license policies are provided in a compressed tar archive. To install Pcoq from this archive, build the directory of your choice (for instance /usr/lib/pcoq, extract the tar archive in this directory, and execute the install command that appears in this directory. This creates a pcoq that can be copied everywhere (for instance, in /usr/bin/pcoq). The other files should not be moved. If you need to move them, then you will need to re-run the install command. Before you use this installation of pcoq, make sure you use the right version of java (see below).
We also provide a rpm package, which requires that coq is already installed with the rpm package provided by the coq developers.
To run pcoq on a windows machine, you only need to download the file pcoq.zip (42 Megas), and unzip it under C: (150 Megas needed)
To run pcoq, you simply need to start the program C:\pcoq\bin\pcoq.BAT
Last, we distribute this software as sources (Pcoq sources). To compile them on a Unix platform, you should follow the instructions given by this link
To run correctly pcoq requires java version 1.3 or 1.4. To know which version of java is available on your machine, just type
java -version
On non-american keyboards, like french or german keyboards it is necessary to take at least java version 1.3.1.rc1. These version are available, for instance, from Sun at the their address.
Once pcoq runs on your machine, we suggest you start practicing with it using the small tutorial (in French, for the moment) called
IntroductionFrancais.v
This file is provided in the pcoq installation.
Pcoq is still moving. To keep being informed about future releases and bug fixes, please have a look at the web page for this software.
Past releases of pcoq can be accessed through our ftp site.