Bonjour,
J’ai le plaisir de vous inviter à ma soutenance de thèse, intitulée :
Challenges in the collaborative evolution of a proof language and its ecosystem
Soit, en français :
Défis dans l’évolution collaborative d’un langage de preuve et de son écosystème
Une version préliminaire du manuscrit est disponible à cette adresse :
La soutenance aura lieu en français. Elle se tiendra le 12 décembre
2019 à 14h en salle 2014, au deuxième étage du bâtiment Sophie Germain
(place Aurélie Nemours, Paris 13). Elle sera suivie d’un traditionnel
pot en salle 3052, au troisième étage du même bâtiment.
Le jury est composé de : Benoît Combemale et Jean-Rémy Falleri
(rapporteurs), Pierre Courtieu, Anne Etien, Tom Mens et Ralf Treinen
(examinateurs), Hugo Herbelin et Yann Régis-Gianas (directeurs de
thèse).
Résumé en français :
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.
Résumé en anglais :
In this thesis, I present the application of software engineering
methods and knowledge to the development, maintenance, and evolution
of Coq —an interactive proof assistant based on type theory— and its
package ecosystem. Coq has been developed at Inria since 1984, but has
only more recently seen a surge in its user base, which leads to much
stronger concerns about its maintainability, and the involvement of
external contributors in the evolution of both Coq, and its ecosystem
of plugins and libraries.
Recent years have seen important changes in the development processes
of Coq, of which I have been a witness and an actor (adoption of
GitHub as a development platform, first for its pull request
mechanism, then for its bug tracker, adoption of continuous
integration, switch to shorter release cycles, increased involvement
of external contributors in the open source development and
maintenance process). The contributions of this thesis include a
historical description of these changes, the refinement of existing
processes, and the design of new ones, the design and implementation
of new tools to help the application of these processes, and the
validation of these changes through rigorous empirical evaluation.
Involving external contributors is also very useful at the level of
the package ecosystem. This thesis additionally contains an analysis
of package distribution methods, and a focus on the problem of the
long-term maintenance of single-maintainer packages.