Coq Platform Docs

About

Coq Platform Docs

This project aims to collaboratively create an action-oriented and interactive documentation for Coq and its Platform. Each core functionality and plugin of Coq and the Coq Platform will have one or several interactive tutorials and/or how-to guides explaining how to use them in practice. They should further be available online through an interactive interface, which this website is a demo page.

The first tutorials are already available and can be checked out below. They can either be runned interactively in a web browser thanks to JsCoq, or downloaded and runned with a text editor able to interact with Coq (e.g. CoqIDE, emacs with Proof General, vim with CoqTail, vscode with vscoq).

Some Ressources:

• The zulip channel we use to discuss and work on the project
• The associated Coq Enhacement Proposal describing the project in details
• The associated github repository

Contributing

We welcome contributions, and there are plenty to do depending on how much available time you have:

• Give feedbacks on the existing tutorial and how-to guides on zulip
• Answer people's questions and share folklore that should be known by all on zulip
• Help to review tutorials and how-to guides, whether you are an expert or not
• Help to improve and write tutorial and how-to guides
• Help with the technical aspects of the project

Small Disclamer

This is a demo, so not everything is working perfectly yet:

• In the future, the documentation is planned to be indexed on the Coq Platform's version, but as of yet, it is only guaranteed to fully work with the latest version of the Coq Platform for Coq 8.19.2.
• The interactive interface is relying on JsCoq1 that only supports Coq up to 8.17 so it may fail on some content requiring Coq 8.19. We are working towards switching to JsCoq2.

Documentation

Coq Tutorials

Writing Proofs

• Chaining Tactics to Simplify and Factorize proofs interactive version and source code

Coq's Functionalities

• Searching for Definitions and Lemma interactive version and source code
• Basic Library Files and Module Management interactive version and source code

Coq's Theory

• Template Polymorphism vs. Universe Polymorphism: interactive version and source code

Equations Tutorials

• The Basics of Equations interactive version and source code
• Equations and Obligations interactive version and source code
• Equations and Well-founded Recursion interactive version and source code