The Coq mailing list

[thomas lamiaux <thomas.lamiaux AT inria.fr>]

Dear Coq users and developers,

We would like to shed some light on our new project "Coq Platform Doc".
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/coq/ceps/pull/91

The first few tutorials are available as well as a (very preliminary) online
interface here:
https://www.theozimmermann.net/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:
https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs
The preliminary git repository is 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)