In the following, we catalog available material related to Prosa, Coq and ssreflect.
As a still young project, most of the documentation is very much a work in progress. Please consider contributing to Prosa by improving and correcting the available documentation, or by asking questions on the Prosa mailing list when the existing documentation is insufficient.
ECRTS’16 Artifact Evaluation (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.
Reduction-based analysis for APA Scheduling (v0.2): provides an overview of the APA-related definitions and proofs.
Prosa tactics guide (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.