The Coq mailing list

[Thomas Lamiaux <thomas.lamiaux AT ens-paris-saclay.fr>]

Dear Rocq users and developers,

We are excited to announce the launch of an official Rocq project: "Rocq Platform Docs",
aimed at creating practical, user-friendly documentation for Rocq and its platform.

Our goal is to provide a comprehensive resource that serves both as:

• A learning tool for users exploring new features.
• A practical (action-oriented) reference for those working with Rocq daily.

This is complementary to the existing reference manual, that provides technical documentation,
and courses, which provide a broader perspective but often lack feature specific materials.

Why it matters

Accessible, well-structured documentation is essential both to attract new users and to retain current users!
It allows everyone -- from beginners to experts -- to learn, explore new features, and troubleshoot issues independently.

Currently, Rocq’s documentation is often fragmented, incomplete, or outdated, making it challenging
for newcomers to get started and even difficult for experienced users to fully leverage certain features.

How you can help

Consequently, we need your expertise and contributions -- whether it’s writing, reviewing, or structuring content --
to make this project a success, and to make Rocq more accessible and user-friendly.
If you have time, please consider participating. Your input will make a real difference!

The Project

This project is composed of four distinct, complementary kinds of documentation, all practice-oriented:

• Learning games that introduce the basics of a feature or concept through a step-by-step game, like the natural number game.
  Several games are needed, and in particular, in addition to generic games,
  it would be useful to have thematic games, e.g., for cryptography people.
  
  
• Tutorials which are learning-oriented: they introduce and tour a feature,
  gradually, through (nice) predetermined examples.
  
  
• How-to guides which are use-case-oriented: they use examples to show
  what to do when facing a specific problem, accounting for real-life complexity.
  
  
• Explanations which aim at giving a deeper understanding of a feature to users
  by discussing how or why a feature works.

This documentation is accessible online, directly on Rocq's new website, and the first few tutorials are already available,
for instance, tutorials about Search, Modules, or a new documentation for the package Equations.
Moreover, in the long run, it will be accessible interactively, and indexed on the version of the Rocq Platform.

Contributing

To make this project successful, we need help to port and write documentation.
We are well aware that people are busy and that it is not easy to free up time,
but the advantage of this project is that everyone can contribute,
even if they have little time available.

Indeed, the documentation can be built gradually and collaboratively, as tutorials can be improved step by step through PRs,
and new tutorials can be written and added independently.

There are several ways to contribute depending on the time you have. First, by giving feedback:

• Give feedback on the existing tutorials, how-to guides, and explanations.
• Answer questions on Zulip, in particular share folklorish tricks that are regularly needed,
  but hard to come up with on your own, and good practices.
• Give feedback on your subject on draft tutorials, how-to guides.

But also by directing improving and writing documentation:

• Add folklore knowledge, either from Zulip, Stack Exchange, or another source that would be missing in a tutorial, or how-to guide
• Write a **quick PR** to add an extra example or section that would be missing, or to clarify an explanation that would be unclear or imprecise.
• Adapt / Port currently existing classes, references, or tutorials
• Write new tutorials, or how-to guides, that would be missing
• Write a learning game, either generic, or specific to your domain like cryptography, PL, algo, etc...

In any case, if you wish to contribute, please check out:

• The webpage on Rocq's new website
• The dedicated Zulip channel
• The GitHub repository.

Best,
Thomas Lamiaux