# Coq Platform Docs: a documentation project for Coq and its Platform

**URL:** <https://discourse.rocq-prover.org/t/coq-platform-docs-a-documentation-project-for-coq-and-its-platform/2380>\
**Category:** Announcements\
**Created:** [July 18, 2024, 12:39pm UTC](https://discourse.rocq-prover.org/t/coq-platform-docs-a-documentation-project-for-coq-and-its-platform/2380 "2024-07-18T12:39:23Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [July 18, 2024, 12:39pm UTC](https://discourse.rocq-prover.org/t/coq-platform-docs-a-documentation-project-for-coq-and-its-platform/2380/1 "2024-07-18T12:39:23Z")

</div>

Dear Coq users and developers,

We would like to shed some light on our new project “Coq Platform Docs”.  
Our goal is to provide an online compilation of short, practical and interactive  
tutorials and how-to guides about Coq and the Coq Platform. We wish this content  
to be part of the upcoming Rocq website. A detailed description of the project can  
be found in our Coq Enhancement Proposal (CEP) here:

> <https://github.com/rocq-prover/rfcs/pull/91>
>
> Hi, it took a lot of effort to write, hope you think it is good.
> 
> \[Rendered\](h…ttps://github.com/thomas-lamiaux/ceps/blob/master/text/XXX-A-Compilation-of-Short-Interactive-Tutorials-and-How-To-Guides-for-Coq.md)

The first few tutorials are available as well as a (very preliminary) online  
interface here:

> **[About · Rocq Documentation](https://www.theozimmermann.net/platform-docs/)**
>
> Description of Rocq Platform Docs

(note that this is a temporary URL that will cease to be available  
once the tutorials are migrated to the official Coq organization)  
At this moment, it contains:

- a Search tutorial
- a Basic library file and module management tutorial
- 3 tutorials about the Equation plugin  
More will follow, especially with your help!

There is a dedicated Zulip channel to discuss and participate:

> **[Deactivated organization | Zulip](https://coq.zulipchat.com/login/)**

The preliminary git repository is [GitHub - rocq-prover/platform-docs: A project of short tutorials and how-to guides for Coq features and Coq Platform packages.](https://github.com/Zimmi48/platform-docs)

Any contribution would be greatly appreciated and we welcome in particular:

- help to improve or write tutorials or how-to guides
- comments or feedback on the project or existing tutorials or your needs
- new tutorials about your favorite feature/plugin
- help to turn folklore or secret powers into common knowledge
- propositions to enhance interactive and non-interactive interfaces
- reviews of our CEP

Do not hesitate to contact us, if you are interested in this project!

## Formally yours,

Thomas Lamiaux (@thomas-lamiaux),  
Pierre Rousselin (@Villetaneuse),  
Théo Zimmermann (@Zimmi48)