Rocqet equips Rocq with nested family polymorphism to enable scalable, extensible mechanized proofs.
We currently build with Rocq version 8.19.0 using OCaml 5.1.0.
Currently, we only support installation from source.
In the future, you can expect to install Rocqet like so:
$ opam install rocqetRight now, you can follow these steps:
-
Install opam
-
Create a new opam switch with OCaml
5.1.0:
$ opam switch create 5.1.0- Install Rocq:
$ opam pin add coq 8.19.0- The CompCert case study has a dependency on Flocq. You need to install it before trying out that case study.
- Finally, we can build by runinng the command:
$ dune bWe provide a flake.nix with all the dependencies (including Emacs, Proof General, Flocq, etc)
We recommend Proof General in Emacs for all platforms. If you prefer VSCode, we recommend VSCoq, but it only works properly for Linux systems with our plugin.
Other user interfaces exist, but we haven't tested them with our plugin. Feel free to try any of them out.
After building and installing a proof interface, you can now step through proofs. We provide lots of example programs here. You can step through the examples interactively, to get familiar with the proof language.
For more interesting programs, we have a framework for extensible certified C compilers, based on CompCert, here and modular mechanized simply-typed lambda calculi, based on Software Foundations, here.
See here.
Generally, issues/bugs with our plugin can be found here.
Others:
- VSCoq, as a proof user interface, doesn't work properly with our plugin on macOS