Coq is a proof assistant used both for the validation of mathematical proofs and for the verification of program properties. It has been developed mainly by Inria researchers for over 35 years.
As free software, its development is today entirely open and transparent, and organized around the GitHub platform. Coq's developers face many standard software engineering issues that the complexity of this software only reinforces: technical debt, testing, release of new versions, compatibility, documentation, welcoming new contributors, etc. An additional challenge is to organize the community to improve the quality, not only of Coq itself, but also of its ecosystem (libraries, plugins, tools, tutorials...).
Developers have gradually become aware of the crucial importance of these issues, on the same level as theoretical developments leading to software improvements. My research, carried out in the heart of the Coq development team, aims at tackling these issues. I will talk about bug tracker, pull requests, continuous integration, and especially reverse dependency testing, release management, maintenance of ecosystem packages, etc.