News Rocq Platform Docs

Announcements
1

Hi everyone,
Here to give some news about the project Rocq Platform Docs.
You can find a description below, if you don’t know what this is.
We have slowly been writing documentation for Rocq, and you can now find documentation for:

  • Ltac2 including a newly written tutorial “Ltac2 for Ltac1 users”, and “how to write a contradiction tactic using Ltac2”
  • The Equations Plugin
  • The Hierarchy Builder Plugin

As always we welcome contributions, and you can come chat with us on Zulip

–

The Rocq Platform Docs aims to collaboratively create an action-oriented and interactive documentation for the Rocq Prover and its Platform. Each core functionality and plugin of the Rocq Prover and the Rocq 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 run interactively in a web browser thanks to JsRocq, or downloaded and run with a text editor able to interact with Rocq (e.g. RocqIDE, Emacs with Proof General, Vim with CoqTail, VS Code with VsRocq).

2

I tried the first tutorial_intro_patterns It failed on the first Rocq line

From Stdlib Require Import List.

with message

Cannot find a physical path bound to logical path
List with prefix Stdlib.

3

As written on the webpage, the online interface is not great and not always working but downloading the tutorials are checked with the lastest version of the platform