Draft of call for contributors/maintainers for Stdlib
send on:

• discourse (auto-replicated on zulip announcement thread)
• coq-club
• anywhere else?

Call for Contributors and Maintainers: Revitalizing the Rocq Stdlib

The Rocq Stdlib, the historical standard library of the Rocq Prover (formerly Coq), is at a turning point. While its development has faced challenges in the past decade, it remains a critical piece of the ecosystem, widely used and offering unique features. With a dedicated repository now separate from Rocq core, we see an opportunity to renew and modernize it. To achieve this, we are launching a call for contributors and maintainers to help shape the future of the library.

Current State of Stdlib

We recently gave the Rocq Stdlib a brand new repository distinct from the Rocq core repository, the later only retaining a minimal subset of files shared by most users (named Corelib). We hope that this new setting will help foster a renewal of the library.

At this point, the Rocq Stdlib offers some unique features and is massively used. However, there has been no team dedicated to its development for several years and we now want one to make it a solid, state of the art library on which Rocq projects can rely on.

Our Vision: A Community-Driven Renaissance

The future of the Rocq Stdlib is open-ended and ready to be shaped by
those who step forward. We aim to:

• establish a working Group of seasoned library builders to define a roadmap for the library’s renewal, with a consistent selection of technologies to support it;
• evaluate which components should remain, be refactored, or be moved out;
• identify key areas for modernization while ensuring backward compatibility where needed;
• reinforce the Stdlib’s role as a high-quality, recommended foundation for Rocq development, as well as an inviting entry point for newcomers.

How You Can Contribute

We are looking for contributors and maintainers of all experience levels. Whether you’re a seasoned Rocq developer or a newcomer there is a place for you.

• Developers with a long experience in building popular, generalist libraries (such as stdpp, math-comp, ext-lib, …) are more than welcome to help design the architecture and the roadmap of the library.
• Anyone can help with curation and organization: documenting what the Stdlib currently offers, refining the library, phasing out outdated content and structuring it more effectively.
• New contributions of various range or difficulty are very helpful: cleaning up proofs, adding features that align with community needs, …

Given the library’s breadth, volunteers can focus on specific domains (e.g., real numbers, lists, etc. - see https://rocq-prover.org/doc/V9.0.0/stdlib/index.html).

As a part of Rocq's official projects, the Stdlib follows the Rocq Governance rules. However, there are no rigid rules yet regarding release cycles and specific governance rules can be defined collectively by those involved.

To ensure that the Stdlib development is a safe and agreeable experience, the development of Rocq Stdlib follows Rocq's code of conduct.

We hope that contributors will:

• be part of a motivated team shaping a fundamental piece of the Rocq ecosystem;
• gain experience in open-source maintenance and formal library development;
• make a lasting impact by revitalizing a key library for the benefit of the entire community.

How to Get Involved

Interested? Let us know on the dedicated zulip channel. A brief note on your background and intended contribution would be helpful, but all interest statements are welcome, even with a small expected involvement or a limited prior experience.

(TODO) We aim to organize a first video call to launch development in June, in conjunction with the Rocq'n share first event.

Let’s work together to bring new life to the Rocq Stdlib!