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

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:

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 GitHub - Zimmi48/platform-docs: A project of short tutorials and how-to guides for Coq features and Coq Platform packages.

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)