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 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

https://hal.inria.fr/tel-02451322
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

File

memoirthesis.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02451322, version 1

Collections

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. ⟨tel-02451322⟩

Share

Metrics

Record views

172

Files downloads

640