Pour Windows et MacOS

Installation de Coq

Utiliser les installeurs officiels pour Windows et MacOs, disponibles là : https://coq.inria.fr/download. Prendre la version 8.6.1.

Installation de Pactole

Les paquets Pactole (archive zip) pour le tutoriel sont disponibles ici. Il suffit de les décompresser dans un répertoire accessible en lecture, disons /full/path/to/pactole. La bibliothèque devra être compilée pour coq-8.6.1.

Démarrage de coqide

Il est possible de démarrer coqide depuis l'interface graphique de Windows et MacOs. Quelques étapes supplémentaires sont cependant nécessaires pour exploiter Pactole depuis coqide, voir le paragraphe Pactole et coqide.

Pour Linux

On peut utiliser opam pour installer coq. Ce système permet les mises à jour et le passage entre différentes versions installées de coq. La page de coq opam est disponible ici.

Installation d'opam

De nombreuses distributions de Linux disposent d'un paquet pour opam.

Pour Debian :

sudo apt-get update
sudo apt-get install opam

Autres distributions

Voir cette page : http://opam.ocaml.org/doc/Install.html.

Installation de coq

NE PAS PRENDRE LE PAQUET COQ DE LA DISTRIBUTION,
la plupart d'entre eux ne sont pas à jour.

opam init # y pour accepter la modification de .profile et .ocamlinit

opam pin add coq 8.6.1
# y to confirm
# compiles coq and its libraries
# takes ~ 5mn (up to 10mn on slow laptops)

opam pin add coqide 8.6.1
# y to confirm
# take 1-3mn

Ajouter le répertoire opam à la variable path

PATH=~/.opam/system/bin:$PATH
#(put this in your favorite shell init file)


Un fichier pour le tutorial Coq est disponible ici.

Installation de Pactole

Les paquets Pactole pour le tutoriel (archive zip) sont disponibles ici. Il suffit de les décompresser dans un répertoire accessible en lecture, disons /full/path/to/pactole. La bibliothèque devra être compilée pour coq-8.6.1.

Tester coq et Pactole rapidement

coqide -R /absolute/path/to/rep-pactole Pactole  myfirstcoq.v

(Si opam n'est pas dans le path il est possible d'invoquer ~/.opam/system/bin/coqide -R ...)

Taper la ligne suivante dans le buffer :

Require Import Pactole.Robots.

Composer [ctrl-down], si la ligne passe du bleu au vert sans erreur, tout est prêt.

Pactole et coqide

Placer les options dans un _CoqProject

Créer un fichier dont le nom exact est _CoqProjectdans le répertoire consacré au développement coq. Entrer les options coq

-R /absolute/path/to/pactole Pactole

dans ce fichier et le sauver. (Les utilisateurs de shell Unix peuvent invoquer : cd my-coq-dev ; echo "-R /absolute/path/to/pactole Pactole" > _CoqProject) Dès lors, les fichiers dans le même répertoire que _CoqProjectpourront accéder aux bibliothèques Pactole.

Utilisateurs de shell Unix : l'invocation de coqide sera désormais coqide my-coq-dev/myfirstcoq.v.