  The Coq Platform is a continuously developed distribution of the Coq proof
assistant together with commonly used libraries, plugins, and external tools
useful in Coq-based formal verification projects. The Coq Platform enables
reproducing and extending Coq artifacts in research, education, and industry,
e.g., formalized mathematics and verified software systems. In this paper, we
describe the background and motivation for the Platform, and outline its
organization and development process. We also compare the Coq Platform to
similar distributions and processes in the proof assistant community, such as
for Isabelle and Lean, and in the wider open source software community.
