Skip to Main content Skip to Navigation

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 greater 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, the design of new processes, 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 metadatas

Cited literature [340 references]  Display  Hide  Download
Contributor : Théo Zimmermann <>
Submitted on : Thursday, January 23, 2020 - 11:38:22 AM
Last modification on : Friday, April 10, 2020 - 5:28:19 PM
Long-term archiving on: : Friday, April 24, 2020 - 2:12:01 PM


Files produced by the author(s)


  • HAL Id : tel-02451322, version 1



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



Record views


Files downloads