This repository contains a template for writing a plugin for the Coq proof assistant using the Dune build system. It showcases a few advanced features such as linking to C code or to external libraries.
The current version is tested (and requires):
- Dune 2.9
- Coq 8.16
Minimal historical requirements are Coq 8.9 and Dune 1.10, but they are not supported anymore. See template history / branches for changes at your own risk.
See the Dune documentation for more help.
The official tutorial
for writing Coq plugins in the Coq repository, which already includes dune files
for OCaml parts.
$ dune buildand the rest of the regular Dune commands. To test your library, you can use
$ dune exec -- coqtop -R _build/default/theories MyPluginor starting with Dune 3.2
$ dune coq top theories/Test.vYou can use
dune-release to
automatically release OPAM packages.
For that, you need to update the included .opam file, and configure
your Github tokens as described in the documentation of dune-release.
Starting with Coq 8.16, Coq will load dependencies of your plugin. This requires that your plugin is named as a findlib package.
See Coq documentation for more information.