Documentation

The following lists some available material related to Prosa, the Rocq prover, and ssreflect.

Note that Rocq was previously known as Coq, and that the older name is still used in many places.

Setup Instructions

• Step-by-step instructions for setting up a Rocq environment suitable for working with Prosa.

Getting Started with the Rocq Prover

• Rocq Prover Foundations for Beginners, the official overview of introductory materials

• Mike Naha’s Rocq tutorial, a short, very accessible intro to Rocq basics.

• Software Foundations • Book 1, a gentle textbook introducing Rocq with lots of helpful excercises.

• Programs and Proofs, detailed, book-like lecture notes by Ilya Sergey that introduce both Rocq and ssreflect.

• Rocq documentation

Reference Information and API Docs

• MathComp homepage, including their documentation

• ssreflect manual

• You will want to master how to search for lemmas within Rocq.

• There is also a Web-based search engine for Rocq lemmas: lemmasearch.com

Prosa Documentation

As an always-evolving research project, most of the available Prosa documentation is continuously a work in progress. Please consider contributing to Prosa by improving and correcting the available documentation, or by asking questions when the existing documentation is insufficient.

Prosa Artifacts

1. ECRTS’16 Artifact Evaluation (for Prosa v0.1): provides instructions for how to install the prerequisites, how to compile all proofs, how to check for incorrect proofs, how to enumerate all axioms, etc.

2. Reduction-based analysis for APA Scheduling (in Prosa v0.2): provides an overview of the APA-related definitions and proofs.

3. Self-Suspending Tasks and Weak Sustainability (in Prosa v0.3): explains the formalization of the proof of weak sustainability of the dynamic self-suspension model.

4. Abstract Response-Time Analysis (in the completely refactored Prosa v0.4): presents the new generic framework for response-time analyses in Prosa.

Prosa Guidelines

• Prosa tactics guide (severely incomplete)

• Prosa writing and coding guidelines: please follow these guidelines when extending or improving Prosa. Patches making existing code more conformant with these guidelines and the core principles are very welcome, too.