Rocq now has a tool rocqblueprint for creating formalization blueprints! I’ve made a first tentative v0.0.9 release of it, see the repo for more details:
If you wish to test rocqblueprint, its available on PyPi, so you should be able to install it via the
pip Python package manager, e.g.
python3 -m pip install rocqblueprint
A very basic example of a website for a simple formalization of even numbers available here:
- Website: An example Rocq blueprint project | by Reinis Cirpons
- Interactive dependency graph: Dependency graph (clicking the Rocq link associated to a node should take you to the documentation for the Rocq declaration of the definition or theorem)
- Github of example project: GitHub - reiniscirpons/example-rocq-blueprint-project: An example project showcasing the use of `rocqblueprint`
The tool implements:
- Linking to
rocqdocumentation in generated PlasTeX documents. - A tentative
blueprint.ymlgithub action template, which builds the project docs assuming a_CoqProjectand opam project definition files exists. - A basic setup wizard for starting a new blueprint available by running
rocqblueprint new.
Next milestone is to add support for rocq-checkdecls (as provided by the latest release of coq-lsp) for flagging up missing rocq declarations and to improve the CI job to use more caching (at the moment a lot of time is spent building the project dependencies via opam, if these could be cached it would provide a significant speedup in the deployment CI).
I would appreciate any feedback you may have. Please feel free to file any issues which may arise on the github issue tracker for the project: https://github.com/reiniscirpons/rocqblueprint/issues .
And of course PRs are very welcome!