THIS SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
Bonjour à tous :),
Je présente aujourd'hui ce petit projet que je développe depuis quelques temps : un IDE pour coq 100% intégré dans Vim :). Le projet se présente donc sous forme d'un plugin vimscript+python. Open-source bien sur, je mets le lien vers le dépôt git en bas du post ;).
Je suis actuellement en prépa math, donc je n'ai "aucunes qualifications informatiques reconnues" (ou attendues), d'où la petite citation célèbre en intro 
(Et comme c'est du GPL :°)
Origine
J'ai commencé à utiliser Coq il y a quelques mois. De base (c'est à dire dans la tarball disponible en téléchargement), deux modes d'utilisations sont possibles : en console (exactement comme pyhton par exemple) ou dans un environnement graphique : CoqIDE.
La console c'est cool mais assez lourd, voir carrément inutilisable, pour des projets de grande ampleur (même des petits à vrai dire ^^). On se reporte donc sur CoqIDE (qui soit dit en passant est très complet).
Il n’empêche que sa zone d'édition n'est pas très pratique (pour les tabulations ..), et que quand on utilise Vim couramment on a l'impression de revenir au bloc-note :|.
J'ai donc décidé de créer un plugin vim pour remplacer CoqIDE.
Synopsis
Comme dis dans la partie précédente, l'objectif de ce plugin est de proposer une interface la plus vim-ième possible (J'entends par là simple et bourrée de raccourcis claviers :D) qui offriraient toutes les fonctions indispensables de CoqIDE (i.e. pour pouvoir utiliser Coq).
De tels raccourcis sont quasiment indispensables puisque les projets Coq se composent uniquement de Définitions/Théorèmes ordonnés. Donc (j'imagine que je ne suis pas le seul) l’exécution (i.e. l'envoi de ces Définitions/Théorèmes au moteur) pas à pas est très utilisée lors du développement.
Je comptais également à la base ajouter une tagbar qui afficherait la liste des Définitions/Théorèmes chargés dans la session en cours. Quand on est débutant, on (du moins je) se sent perdu devant le nombre de Théorèmes disponibles (D'où l'idée de la Tagbar).
Certes une modification de CoqIDE directement aurait été possible (bien qu'il soit codé en caml :D), mais je pense qu'un plugin Vim (qui de plus est en python) est beaucoup plus simple à modder ..
J'ai appris peu après le début de ce projet qu'il existait déjà un tel plugin : Coquille. Néanmoins je ne le trouvais pas assez pratique d'utilisation (Spécifique à Coq), donc j'ai quand même continué à développer Vcoq.
Intérêts de ce post
C'est un tout petit projet (comparé à d'autres projets présentés sur ce site). Voici tout de même quelques motivations à ce post :
- Si ça peut aider ou faciliter la tâche à quelqu'un. (Bien que Coq ne soit pas un logiciel utilisé très couramment )
- L'intérêt d'un logiciel open-source est d'être partagé (un de ses intérêts).
- Étant donné que c'est mon premier plugin Vim, j'aurais bien aimé avoir des retours sur son ergonomie "Vim-ième"
- Je compte ouvrir un petit blog pour faire des homepage pour mes projets. En attendant je présente vcoq ici.
Petit aperçu
Fonctionnalités
Déjà implémentées :
- Gestion avancée des fenêtres de l'IDE (redimensionnement automatique)
- Gestion des fichiers (Le plugin n'utilise pas les buffers de vim, les commandes classiques :w ou :e ne sont donc plus disponibles)
- Communication avec le processus coqtop
- Envoi de query commandes et affichage des résultats dans la console
- Mode pas à pas : fonctions Next() et Prev() pour envoyer ou revenir en arrière dans le code
À venir :
- Compiler (Je ne sais pas trop comment appeler cette fonctionnalité :s) jusqu'au curseur
- Implémentation de la Tagbar (La fenêtre est affichée, mais elle ne contient rien)
- Implémentation du mode "Preuve"
- Ouverture de plusieurs fichiers à la fois
Mot de fin
Pas grand chose à ajouter pour l'instant … 
Lien vers le dépôt Github : Github - vcoq
Si vous vous sentez d'attaque pour corriger une faute d'orthographe/d'anglais dans les commentaires .. n'hésitez pas 
(je ne relis jamais les com's, et comme dis plus haut :
THIS SOFTWARE IS PROVIDED "AS IS"