A guide to building your Coq libraries and plugins with Dune

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

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.

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.

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?

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.

Thanks for updating the repository @ejgallego. Greatly appreciated.

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

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.

@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 ◡̈

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.

The question is about a Coq library (not a Coq plugin). You still recommend your plugin template in this case? It seems that the library use case is pretty different and there are a lot of projects to choose from as examples (e.g. projects maintained by @palmskog in coq-community).

For (almost) pure Coq library use of Dune, I recommend people to look at https://github.com/palmskog/coq-program-verification-template which was inspired by Emilio’s plugin template but elides all the plugin-specific stuff.

Indeed good point, I was planning to update the template to be coq-dune-template and cover some different use cases, but I’d like to make a bit more progress on some existing issues first; I’ll edit the post to add Karl’s template too.

Thanks @ejgallego @palmskog and @Zimmi48 for the response and will certainly look at your repository as reference for a Coq library template. For understanding the usages of the files like Makefile and _CoqProject, is there any place that I can read about, or perhaps someone here can provide a practical introduction/guide to them here?

Here’s the documentation on _CoqProject: https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile