A guide to building your Coq libraries and plugins with Dune

Developing plugins
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.

21

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).

22

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.

23

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.

24

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?

25

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

26

Is there a way to let VSCoq understand where to look for libraries while using a dune-based build?

Unable to locate library LIBNAME. (While searching for a .vos file.)

I just get the above in the ProofView while importing libraries.

27

As of today you need to do a mock _CoqProject adding the build path, this is indeed quite unoptimal.

1 Like
28

Thanks, I am still confused about what exactly is required in the _CoqProject file.

$ tree -d
.
├── _build
│   └── default
│       └── src
└── src

I have my .v sources, dune and _CoqProject in the src directory and the dune-project file at the root.

Using ../_build/default/src/ for -I and/or -R doesn’t seem to be working.

29

If you do not have OCaml files, you shouldn’t use -I, only -R.
What about putting your _CoqProject file at the root containing only:

-R _build/default/src MyProjectNamespace

And then running code . from the root of the project?

1 Like
30

Aha! That did it. Thanks Théo!

31

I don’t think you explain how you actually do the build. You run make? dune build?

32

dune build is the usual command to build/check Coq projects locally when there are dune files in a project.

If one has declared several packages package1, package2, etc., each package can be built/checked in isolation by running:

dune build -p package1
dune build -p package2

etc.

1 Like
33

@ejgallego if we use dune, is the coq project still expected to have a:

  1. coq_proj.opam file?
  2. does it still need a Makefile (or a command we run like make)?

Thanks!

34

@brando90

  1. If you are distributing the project, then you will also need to provide a coq_proj.opam file. You can also have Dune generate this automatically, have a look at the documentation here.
  2. A Makefile is not necessary for building with Dune, but you can of course include one to call Dune commands if you wish. Typically you would have one where the default target calls dune build or something.
35

Hi, I followed your guide but I get the following error message:

$ dune build
#File "dune-project", line 30, characters 1-11:
30 | (coq.theory
      ^^^^^^^^^^
Error: Unknown field coq.theory

Let me know if you have any ideas. I am including (using coq 0.7). Thanks.

36

coq.theory isn’t legal in dune-project files, only in dune files.