Master 2014 2015
SVP
Installation de Coq

Installation en salle machine

Voici les étapes pour installer coq et proof general sur votre compte en salle de TME.

La dernière version de Coq est installée en salle machine.

Pour vérifier, lancez coqtop dans un shell.

Vous devrez voir les lignes suivantes :

Welcome to Coq 8.4pl4 (September 2014)

Coq <

(vérifiez bien le numéro de version)

Tapez Quit. (sans oublier le point) et validez pour sortir du top-level Coq.

Pour installer ProofGeneral, l’interface utilisateur de haut niveau pour coq, il faut ouvrir le fichier ~/.emacs et ajouter la ligne suivante :

(load-file "/usr/local/ProofGeneral/generic/proof-site.el")

Sauvegardez votre fichier ~/.emacs et lancez :

emacs test.v &

Avec un peu de chance, le général devrait apparaître ...

Installation sur votre machine personnelle

sudo apt-get install coq
sudo apt-get install proofgeneral

(d’abord sudo apt-get install emacs s’il n’est pas déjà installé)

Pour les autres versions de linux, cherchez les paquets correspondants.