Challenges in the collaborative evolution of a proof language and its ecosystem
Défis dans l'évolution collaborative d'un langage de preuve et de son écosystème
par Théo ZIMMERMANN sous la direction de Hugo HERBELIN et de Yann RÉGIS-GIANAS
Thèse de doctorat en Informatique
ED 386 Sciences Mathematiques de Paris Centre

Soutenue le jeudi 12 décembre 2019 à Université Paris Cité

Sujets
  • Coq (logiciel)
  • Git (logiciel)
  • Logiciels -- Maintenance
  • Logiciels libres

Les thèses de doctorat soutenues à Université Paris Cité sont déposées au format électronique

Consultation de la thèse sur d’autres sites :

TEL (Version intégrale de la thèse (pdf))

Description en anglais
Description en français
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.