Canal coq pour Guix

Qu'est-ce que Coq ?

Coq est un assistant à la preuve. C'est un environnement de programmation avec un langage proche de celui d'OCaml, qui permet d'écrire à la fois des programmes et des énoncés mathématiques. Coq contient aussi un deuxième langage, de tactiques, qui permet de démontrer les énoncés mathématiques que l'on exprime dans le premier. En mélangeant programmes et énoncés mathématiques, on peut exprimer des propriétés très complexes sur les programmes que l'on écrit et les prouver.

Ce billet de blog n'est cependant pas un cours sur coq, ni même une introduction. Cependant, comme j'utilise Coq de temps en temps, et que j'utilise aussi vim pour l'édition de programmes en général, j'ai besoin d'un greffon pour faire fonctionner le système coq dans mon environnement favori

Pour cela, il y avait le greffon coquille qui fonctionnait sur d'anciennes versions de coq, mais le projet n'est plus très vivant. J'ai donc décidé il y a un peu plus d'un an de créer ma propre version de coquille, en partant de l'existant. J'ai porté le tout sous neovim, qui a l'époque était le seul à proposer la prise en charge du multithreading.

Un greffon, des tests, et un canal

Pour mes besoins de développements, j'ai fini par devoir utiliser des tests pour m'assurer que tout fonctionne. Bien qu'ils soient encore très balbutiants (et loin d'être complets), je savais que j'avais besoin de prendre en charge plusieurs versions de coq. Pour cela, je souhaitais utiliser Guix pour créer des environnements avec des versions différentes de coq.

Le problème, c'est que Guix ne contient qu'une seule version de chaque logiciel qu'il propose, sauf rares exceptions, dont coq ne fait pas partie. Je devais donc trouver un moyen d'avoir ces différentes versions, mais en dehors de Guix lui-même. Pour cela, le mécanisme de canal est le plus adapté : il permet d'étendre la distribution Guix sans y toucher directement. C'est assez facile à mettre en place, et c'est maintenant fait dans un dépôt framagit.

Utilisation

Pour pouvoir utiliser ces versions, il vous faudra ajouter le canal à la liste de vos canaux. Si le fichier ~/.config/guix/channels.scm n'existe pas, créez-le avec ce contenu :

(cons* (channel
   (name 'coq)
   (url https://framagit.org/tyreunom/guix-coq-channel.git))
  %default-channels)

Maintenant, après avoir lancé guix pull vous devriez pouvoir installer et utiliser coq dans plusieurs versions. Vous pouvez lister les versions de coq de cette manière :

$ guix package -A ^coq$

coq	8.7.2	out	coq/coq.scm:98:2
coq	8.10+beta1	out	coq/coq.scm:166:2
coq	8.6.1	out	coq/coq.scm:36:2
coq	8.8.2	out	coq/coq.scm:149:2
coq	8.9.1	out	gnu/packages/coq.scm:44:2