Mots clés |
Génie logiciel empirique, Assistant de preuve, GitHub, Collaboration ouverte, Ecosystème de paquets, Evolution du logiciel |
Resumé |
Dans cette thèse, je présente l'application de méthodes et de connaissances en génie logiciel au développement, à la maintenance et à l'évolution de Coq ¿un assistant de preuve interactif basé sur la théorie des types¿ et de son écosystème de paquets. Coq est développé chez Inria depuis 1984, mais sa base d'utilisateurs n'a cessé de s'agrandir, ce qui suscite désormais une attention renforcée quant à sa maintenabilité et à la participation de contributeurs externes à son évolution et à celle de son écosystème de plugins et de bibliothèques.D'importants changements ont eu lieu ces dernières années dans les processus de développement de Coq, dont j'ai été à la fois un témoin et un acteur (adoption de GitHub en tant que plate-forme de développement, tout d'abord pour son mécanisme de pull request, puis pour son système de tickets, adoption de l'intégration continue, passage à des cycles de sortie de nouvelles versions plus courts, implication accrue de contributeurs externes dans les processus de développement et de maintenance open source). Les contributions de cette thèse incluent une description historique de ces changements, le raffinement des processus existants et la conception de nouveaux processus, la conception et la mise en œuvre de nouveaux outils facilitant l'application de ces processus, et la validation de ces changements par le biais d'évaluations empiriques rigoureuses.L'implication de contributeurs externes est également très utile au niveau de l'écosystème de paquets. Cette thèse contient en outre une analyse des méthodes de distribution de paquets et du problème spécifique de la maintenance à long terme des paquets ayant un seul responsable. |