Skip to Main content Skip to Navigation
Theses

Challenges in the collaborative evolution of a proof language and its ecosystem

Théo Zimmermann 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
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.
Complete list of metadata

Cited literature [340 references]  Display  Hide  Download

https://hal.inria.fr/tel-02451322
Contributor : Théo Zimmermann Connect in order to contact the contributor
Submitted on : Tuesday, January 4, 2022 - 10:40:08 AM
Last modification on : Tuesday, January 11, 2022 - 11:16:05 AM
Long-term archiving on: : Friday, April 24, 2020 - 2:12:01 PM

File

ZIMMERMANN_Theo_va2.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-02451322, version 1

Citation

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

Share

Metrics

Les métriques sont temporairement indisponibles