English Version

Compiler Pcoq sous Unix

Pour installer pcoq à partir des sources du logiciel, vous devez vérifier que vous avez les bons outils pour le re-compiler. Pour ceci, vous avez besoin de:

  1. La bonne version de ocaml,
  2. La bonne version du kit de développement Java,
  3. Une installation locale de la bonne version du système Coq (attention, l'installation fournie par défaut par l'équipe de développement de Coq n'est pas une installation locale).

Pour Coq version 7.4, les bonnes versions sont 3.06 pour ocaml et 1.4 pour java (mais 1.3 fonctionne aussi où 1.3.1rc1 si vous utilisez un clavier avec caractères accentués)

Compiler Coq

Une installation incorrecte de Coq est la cause la plus fréquente d'échec dans la compilation de pcoq. De plus, les installations par défaut fournies par l'équipe de développement de Coq ne sont pas adaptées pour la re-compilation de pcoq. Pour cette raison, il est souvent préférable de re-compiler Coq en suivant les indication fournies dans cette documentation.

Construire une installation locale de Coq peut être difficile, surtout parce que la documentation fournie par Coq est un peu erronée sur ce point. Comme indiqué dans le fichier d'installation de Coq, on doit appeler la commande configure de coq avec l'option -local, mais il ne faut jamais (j'insiste: jamais) effectuer des étapes plus loin que l'étape 5.

Les commandes à exécuter sont les suivantes:

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

Compiler Pcoq

Une fois que l'on dispose d'une installation locale de Coq, il faut ajouter le répertoire des binaires de cette installation dans la variable PATH pour Unix, puis effectuer les opérations suivantes:

  1. Extraire les sources de l'archive tar compressée,
  2. Changer de répertoire vers le répertoire pcoq qui a été créé par l'extraction,
  3. Appeler la commande de configuration de pcoq, configure,
  4. Appeler les commandes compilation gmake depend et gmake world.

Si, en raison d'échecs dans la compilation on est amené à relancer la compilation, il peut être judicieux d'appeler gmake clean puis gmake depend avant de relancer la compilation.

Les commandes à exécuter sont les suivantes:

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

Utilisation de pcoq

La commande pour lancer pcoq se trouve dans le répertoire bin et s'appelle pcoq. Elle peut être copiée où vous le voulez, par exemple dans le repértoire /usr/local/bin, tant que le répertoire où la compilation a été effectuée n'est pas déplacé. si vous modifierz les fichiers ml du répertoire Coq et que vous désirez que les modifications soient prises en compte dans votre session pcoq, il est nécessaire d'appeler cette commande avec l'option -local. Par exemple, vous pouvez taper la commande 
pcoq IntroductionFrancais.v
pour trouver une explication rapide de l'utilisation de pcoq.

Yves Bertot
Last modified: Tue Feb 11 10:52:04 MET 2003