Prosa v0.5: The POET Edition

Prosa v0.5 is the first release of Prosa to support POET.

Download

Download the release here: prosa_v05.zip

Organization

The directory and module structure is organized as follows. First, the main parts, of which there are currently five (plus the classic Prosa version).

Reading Prosa

The v0.5 release of Prosa uses CoqdocJS to obtain a prettier spec.

Alternatively, there is also a plain coqdoc version without proofs (which is better suited for printing to PDF).

We also provide HTML renderings of the classic (i.e., pre-2020) Prosa spec, which is no longer being developed:

Installing Prosa

With OPAM

Prosa can be installed using the OPAM package manager (>= 2.0).

opam repo add coq-released https://coq.inria.fr/opam/released
#or for the dev version (git master): https://coq.inria.fr/opam/extra-dev
opam update
opam install coq-prosa

From Sources with opam

OPAM can also be used to install a local checkout. For example, this is done in the CI setup (see .gitlab-ci.yaml).

opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam pin add -n -y -k path coq-prosa .
opam install coq-prosa

Manually From Sources

Dependencies

Besides on Coq itself, Prosa depends on

  1. the ssreflect library of the Mathematical Components project,
  2. the Micromega support for the Mathematical Components library provided by mczify, and
  3. the The Coq Effective Algebra Library (optional, needed only for POET-related refinements).

These dependencies can be easily installed with OPAM.

opam install -y coq-mathcomp-ssreflect coq-mathcomp-zify coq-coqeal

Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.

Compiling Prosa

Assuming all dependencies are available (either via OPAM or compiled from source), compiling Prosa consists of only two steps.

First, create an appropriate Makefile.

./create_makefile.sh

Alternatively, to avoid compiling the older “classic” Prosa, specify the --without-classic option. This can speed up compilation considerably and is a good idea during development. (It’s also possible to only compile the “classic” Prosa by specifying the --only-classic option, but this is rarely needed.)

./create_makefile.sh --without-classic

To avoid compiling the POET-related refinements (which require CoqEAL to be installed and inject a dependency on the proof irrelevance axiom), specify the switch --without-refinements. For example, to skip both “classic” Prosa and the refinements library, use the following command:

./create_makefile.sh --without-classic --without-refinements

Second, compile the library.

make -j

Depending on how powerful your machine is, this will take a few minutes.

Checking the Correctness of the Proofs

To check the correctness of all proofs, compile the code as described above and run make validate.

make validate

You should see the following output, confirming that all proofs in Prosa were mechanically checked and do not include any additional Axioms .

CONTEXT SUMMARY
===============

*Theory: Set is predicative
  
*Axioms:
    Coq.Logic.ProofIrrelevance.proof_irrelevance
  
*Constants/Inductives relying on type-in-type: <none>
  
*Constants/Inductives relying on unsafe (co)fixpoints: <none>
  
*Inductives whose positivity is assumed: <none>
  

The assumption of proof irrelevance is introduced by the CoqEAL library and can be avoided by running ./create_makefile.sh with the --without-refinements flag.