Quelques liens

la page officielle ;
Cocorico! le wiki de coq ;
Pour voir à quoi ça ressemble et/ou rentrer rapidement dans le vif du sujet :
- Coq in a Hurry : d’Yves Bertot ;
- ou Petit guide de survie en Coq d’Alexandre Miquel ;
- Un cours de Jean Dupras en 13 leçons que je trouve très clair ;
Coq’Art : la page du livre sur Coq,
un long cours en vidéo d’Yves Bertot ;
un autre très bon cours : Software Foundations par Benjamin C. Pierce, introduit COQ en détail, et parle également de sémantique des programmes, etc.
POPL’2008 tutorial : “How to write your next POPL paper in Coq”
HELM : peut aider à trouver des choses dans les bibliothèques de coq (quand ça marche…)
Cours MPRI
Adam Chlipala utilise beaucoup Ltac et présente ces expériences dans Certified Programming with Dependent Types. Ça serait intéressant de passer un peu de temps a étudier ça…
A mes tout début de Coq, je me suis fait un petit aide mémoire auquel a également contribué Clément Hurlin
ProofWeb permet d’utiliser COQ sur le Web. Il contient également une série d’exercices…
le Sudoku de Laurent: une applet java à partir d’un programme COQ…
A explorer/tester un jour :
- Tactics for Rewriting modulo associativity and commutativity

Editeur externe dans coqide

Configurer un éditeur externe pour coqide est assez facile car c’est prévu : il suffit de spécifier la commande dans les préférences :

Edit/Preferences/Externals/External editor

Par exemple :

/usr/bin/gvim -geometry 81x62 %s

Par ailleurs, pour y associer un accélérateur clavier, il faut copier le fichier .coqide.keys (dans son HOME jusqu'à la version 8.3, et dans ~/.config/coq/ à partir de la v8.4), puis modifier la ligne :

; (gtk_accel_path "<CoqIde MenuBar>/Edit/External editor/" "")

en :

(gtk_accel_path "<CoqIde MenuBar>/Edit/External editor/" "<Primary>e")

c’est-à-dire qu’il faut la décommenter (ôter le ; en début de ligne) et ajouter la combinaison de touches choisie (ici, <Ctrl>e).

Attention: il faut quitter coqide avant de faire ça, sinon, ça risque d'être écrasé.

Ouvrir les onglets dans le bon ordre

Quand on a plusieurs fichiers dans un développement COQ, il peut être pratique de les ouvrir dans l’ordre de leurs dépendances. Celà peut se faire en utilisant coqdep:

if test "$COQDIR" = "" ; then
  echo "Warning : COQDIR is not set "
  COQIDE=``which coqide``
else
  COQIDE=$COQDIR/bin/coqide
fi
echo "Launching $COQIDE"
FILES=``$COQDIR/bin/coqdep -sort -suffix .v *.v``
$COQIDE $COQOPT $FILES

COQ : un assistant de preuve formelle

Quelques liens

Editeur externe dans coqide

Ouvrir les onglets dans le bon ordre

Voir aussi :