Coq est un assistant de preuve servant à la fois à la validation de preuves mathématiques et à la vérification de propriétés de programmes. Il est développé principalement par des chercheurs Inria depuis plus de 35 ans.
Logiciel libre, son développement est aujourd'hui entièrement ouvert et transparent, et organisé autour de la plateforme GitHub. Les développeurs de Coq font face à de nombreuses questions standards de génie logiciel que la complexité de ce logiciel ne fait que renforcer : dette technique, tests, sortie de nouvelles versions, compatibilité, documentation, accueil de nouveaux contributeurs, etc. Un défi supplémentaire est celui d'organiser la communauté pour améliorer la qualité, pas seulement de Coq lui-même, mais aussi de son écosystème (bibliothèques, plugins, outils, tutoriels...).
Les développeurs ont progressivement pris conscience de l'importance capitale de ces questions, au même niveau que les développements théoriques permettant de conduire à des améliorations du logiciel. Mes recherches, effectuées au cœur de l'équipe de développement de Coq, visent à s'y attaquer. Je vous parlerai donc de bug tracker, de pull requests, d'intégration continue, et notamment de test de dépendances inverses, de release management, de maintenance des paquets de l'écosystème, etc.