A guide to building your Coq libraries and plugins with Dune

Developing plugins
1

Developing Coq plugins and libraries using Dune as their build system 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 2.0)
(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)
 (package 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!

9 Likes
2

Thanks for this short guide!

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

3

Post updated, thanks!

1 Like
4

How does this integrate with a Makefile and _CoqProject?

5

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.

6

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?

1 Like
7

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
8

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.

9

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.

10

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

3 Likes
11

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
12

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

13

I realized today that if a plugin (in my case extraction_relation) depends on a Coq plugin (here extraction), and a file of the Coq plugin is used in the new plugin (here table.ml), then Extraction_plugin.Table and Table are both valid to compile the plugin but they are different at linking time. The first one refers to the copy of Table in the .cmxs associated to the pack, the second one refers to the file table.cmi itself. As a consequence, using the second fails, because it is the pack extraction_plugin.cmxs that Coq loads while for the second case to work, it is table.cmx which would have to be loaded.

One issue is that the -I plugins/extraction in coq_makefile does not prevent to do the mistake of referring to table.cmi.

Dune is told to avoid this problem.

14

Indeed @herbelin we had this problem in the past requiring open Ltac_plugin everywhere to avoid a link problem, I understand this is a shortcoming of `-pack ; see Section 8.9 https://caml.inria.fr/pub/docs/manual-ocaml/manual031.html#s%3Amodule-alias of the OCaml manual for an alternative strategy [implemented by Dune]

We could port our makefiles to do this, but likely not worth the effort. The workaround for most cases is to refer to the long version of the module.

15

Hi @ejgallego, I’m trying to understand what the various entries mean.

Regarding file theories/dune, I have the following questions.

 (public_name my-plugin.theory) ; Adding this line will make your
                                ; library installable
  1. Does public_name enable the functionality one would achieve by running make install?
  2. And if so does writing my-plugin.theory mean that after somehow using dune to install, then module my-plugin.theory.Test will become available to be required in Coq?
16

Hi @cogumbreiro, first of all check the coq-plugin-template again, I’ve updated it. Actually I had updated it some days ago but the push failed and I didn’t realize.

Regading the (package foo) field, indeed what this tells Dune is to consider that library for install. For example you may want to have two libraries, one for tests which is not installed, and the main one.

As of today Coq’s library namespace is global tho; that is to say, when you install a library using Dune or coq_makefile Coq will always see it; this will be improved hopefully soon.

17

Thanks for updating the repository @ejgallego. Greatly appreciated.

Is it possible to build and install a Coq package without creating an .opam file?

18

Newer dune versions do indeed support defining the packages in the dune-project file, see https://dune.readthedocs.io/en/stable/opam.html

However the notion of Dune and OPAM package are still too tightly coupled, as you can infer from the documentation.

19

@ejgallego I’m trying to understand how I can use the guide that you have provided here to build my own Coq library. However, the related documentations at your github and dune readthedocs are too cryptic for me to understand. Is there anyone who can provide a more gentle guide for someone who is still relatively new to this process of setting up a Coq library?

Many thanks in advance ◡̈

20

I would start from https://github.com/ejgallego/coq-plugin-template ; I’d suggest we work on that repository as to improve the documentation of the template, so indeed, please submit issues on that repos for any questions / problems with the template doc.