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 you that you need to use exactly Coq version 7.2 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.
Dowload the zipped file Pcoqzip.zip (60 Megas), et unzip it under C: (150 Megas needed)
Under windows 95/98 et perhaps XP, a manipulation is needed:
click with the right button on the file C:\pcoq\bin\pcoq.bat, and select Properties
in the new window, click on Memory,
tput 4096 in the field Initial Environment
cclick then on Apply and Ok.
To launch Pcoq, execute the command C:\pcoq\bin\pcoq.bat
Under Pcoq, dowload the file C:\pcoq\IntroductionFrancais.v that explain (in French) the basic use of Pcoq.
To uninstall Pcoq, delete the folders:
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 pcoq installation.
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. 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.
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.
Last modified: Wed Jan 23 09:24:07 MET 2002