A guide to building your Coq libraries and plugins with Dune

Developing Coq plugins with Dune does offer some extra features and flexibility when compared to the traditional coq_makefile setup:

  • compositional build: you can drop your plugin inside the coq folder or the coq folder inside your plugin’s and Dune will know how to build them together in one go. That leads to significantly shorter edit/compile cycles,
  • Dune extra features: for example dune build @check, dune utop, or dune build -w,
  • easy linking with external packages or C libraries: using the standard Dune toolset.

In order to get started with Dune, you must add dune and dune-project files to your plugin. Typical content of the dune file is:

(library
 (name equations_plugin)
 (public_name equations.plugin)
 (libraries coq.stm))

This will properly compile the OCaml files. If you have some mlg grammar files, you must add rules to process them:

(coq.pp (modules g_equations))

dune-project helps determine the root directory of the project and typically contains something such as:

(lang dune 1.9)
(name equations)

The above does take care of the ML part, starting with Dune 1.9, support for .v -> .vo file compilation has also been added. In order to enable the compilation of Coq files, you should add to your dune-project file:

(using coq 0.1)

that will enable a (coq.theory ...) stanza; typical use is:

(coq.theory
 ; This determines the -R flag
 (name Equations)
 (public_name equations.Equations)
 (synopsis "Equations Plugin")
 (libraries coq.plugins.extraction equations.plugin)
 (modules :standard \ IdDec NoCycle))

 (include_subdirs qualified)

Note that the .v files can depend on the ML plugin, this will rebuild everything correctly!

There is an ongoing template here https://github.com/ejgallego/coq-plugin-template

For now, the official documentation resources are:

help us to make them better!

6 Likes

Thanks for this short guide!

Could you explain what you mean by “compositional build”?

Post updated, thanks!

1 Like

How does this integrate with a Makefile and _CoqProject?

It does replace them; for now only the ML part [but this is already useful in dev contexts], and soon (I hope < 1 month) the .vo part too.

I can definitely see that one would just remove .ml/.mlg from _CoqProject, but we still need to put .v files in _CoqProject to make CoqIDE and ProofGeneral happy, at least for Coq 8.9. So maybe there should also be examples of how to mix Dune and Make for 8.9 users?

CoqIDE and Proof-General can indeed take advantage of the _CoqProject file, but only the lines specifying the options such as -R or -Q and possible additional options for changing the default warnings. However, they don’t need the listing of .v files. Ideally, I would like that the coq-mode of Dune generates this (reduced) _CoqProject (like it does for .merlin). @ejgallego has said that he rather plan to have a new format resembling .merlin file, and this might be better indeed, but this won’t be backward compatible.

1 Like

Indeed Dune support is very experimental at this stage, you can still have _CoqProject of course. It is mainly of interest to developers, as it provides better tooling and allows to do some stuff in plugins that is hard; note anyways that until we don’t rewrite Coq’s plugin linker most of the advantages won’t be easy to reap.

We could indeed write a _CoqProject with -R flags, etc… That should be easy to do. .merlin files do indeed have some problems so it is not clear what should we use.

Hi Emilio,

Thanks for the post.
I’m trying to figure out if this can be used to build an OCaml tactic.
The original example seems to be outdated and doesn’t work well. It would be very helpful if you have a minimal example of building the “hello world” tactic with Dune.

Here you go @yangky11 https://github.com/ejgallego/coq-plugin-template

3 Likes

Hi, Thanks for the documentation and the helpful example.

Is there support for extraction? e.g. to see Coq as an OCaml code generator.

More precisely, I have a development with both Coq and OCaml code (in the style of CompCert, for instance). I’ve been able to set up a build system using dune by splitting the development into three parts: a pure Coq part and a pure OCaml part, both using dune; and a hackish glue that runs coqc extraction.v to populate the source tree.

I wished there were a better way.

2 Likes

Hey Vincent, thanks for the kind words. Indeed we hope to address that, for more info see https://github.com/ocaml/dune/issues/2178