Challenges in the collaborative evolution of a proof language and its ecosystem - Archive ouverte HAL Access content directly
Theses Year : 2019

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

(1, 2)
1
2

Abstract

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.
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.
Fichier principal
Vignette du fichier
ZIMMERMANN_Theo_va2.pdf (2.21 Mo) Télécharger le fichier
Origin : Version validated by the jury (STAR)
Loading...

Dates and versions

tel-02451322 , version 1 (04-01-2022)

Identifiers

  • HAL Id : tel-02451322 , version 1

Cite

Théo Zimmermann. Challenges in the collaborative evolution of a proof language and its ecosystem. Software Engineering [cs.SE]. Université Paris Cité, 2019. English. ⟨NNT : 2019UNIP7163⟩. ⟨tel-02451322⟩
701 View
1620 Download

Share

Gmail Facebook Twitter LinkedIn More