Dune for Coq General Issue

[ejgallego]

Dear Dune developers:

this is a progress report and RFC on the ongoing integration of Dune
as build tool for Coq libraries and for Coq itself.

For those curious, Coq is an interactive proof assistant with a close
relationship to OCaml. The codebase is medium-sized, with around
200.000 lines of OCaml and 150.000 lines of Coq scripts. The first
versions of Coq date from almost 35 ago, so there is certainly a lot
of history on it.

So far, apart from some minor annoyances documented in
coq/coq#8729 , the OCaml part of Coq builds in
a pretty clean way, with performance on par or better than make,
which is in our opinion pretty good. We have started the process to
consider Dune as the main build system for Coq.

Coq libraries are a mix of Coq scripts and OCaml "Coq plugins". As of
today, they are built in a slightly hackish way, using a tiny tool
coq_dune, that generates the corresponding dune build files from
the information generated by coqdep.

This poses several problems, and indeed it was suggested that we
should try to add native Coq support to Dune, which we think it does
make sense.

The compositionality aspect of Dune seems extremely interesting for
Coq, as there exist many 3rd party libraries and plugins and it is
common for developers to want to compose them as to have a larger
"develop" view.

In relation to build Coq libraries, there is nothing very special so
far about building them. Usually, a single .v file will generate an
object file .vo, tho there are special modes for quick compilation
that won't check proofs. Some plugins need to use a custom Coq
preprocessor, but that is done in a standard way too.

It seems that there are two main questions to solve before we can
begin the work on a native Coq mode for Dune:

• extensions of dune files: Coq "libraries" do map very well to
  the notion of OCaml libraries, to the extent that they are a
  superset of them. Thus, the main question here is "how should we
  extend the Dune syntax to support Coq libs"? In principle, I think
  that being able to write something such as:

(library
  (public_name coq.stdlib.streams)
  (mode coq)
  (coq_flags ...)
  (libraries coq.stdlib.coq))

would be the more convenient option. WDYT?

• plugin interface: it is not clear to us what files of the source
  tree we should modify in order to add Coq build rules to Dune. We
  could follow the example of Menhir, however we are not sure, due to
  the above considerations that this is the right thing to do.

[rgrinberg]

Coq libraries are a mix of Coq scripts and OCaml "Coq plugins". As of
today, they are built in a slightly hackish way, using a tiny tool
coq_dune, that generates the corresponding dune build files from
the information generated by coqdep.

Is it possible to build the OCaml component of a coq library separately? In other words, can we consider the coq library as a normal OCaml library + a coq library?

Thus, the main question here is "how should we
extend the Dune syntax to support Coq libs"? In principle, I think
that being able to write something such as:

I think it is preferable for coq to introduce its own stanzas. The main concern is that dune's versioning policy works best on the stanza level. Hence if the coq team maintains its own stanzas in dune, they will have more control over the backwards compatibility they'd like (or not like) to provide. The dune language has a very strict compatibility guarantee, and it's not necessary for plugins to adhere to it. This is similar to how the menhir plugin is versioned independently of the dune language and was able to introduce a breaking change in dune 1.4.

Of course, if building coq requires some extra option in the library stanza to make things work for OCaml plugins then the dune is likely to oblige. But to me it seems best for the coq team to maintain its own stanza frontend for maximum flexibility. Note that this doesn't necessarily entail more work, as you can always just desugar coq specific stanzas to existing dune stanzas.

plugin interface: it is not clear to us what files of the source
tree we should modify in order to add Coq build rules to Dune. We
could follow the example of Menhir, however we are not sure, due to
the above considerations that this is the right thing to do.

I think that starting off with the menhir way is sensible. If today's library stanza is deficient in anyway for building coq plugins in OCaml, then those issues should be raised as soon as possible.

[ejgallego]

Thanks a lot for the comments @rgrinberg,

Is it possible to build the OCaml component of a coq library separately? In other words, can we consider the coq library as a normal OCaml library + a coq library?

Yes, that's what we do today. The Coq libraries may depend on the OCaml ones, but not the other way around. [In particular a .vo file may depend on a .cmo file.

I think it is preferable for coq to introduce its own stanzas. The main concern is that dune's versioning policy works best on the stanza level.

I'd dare to say that this shouldn't be too much of a concern.

Of course, if building coq requires some extra option in the library stanza to make things work for OCaml plugins then the dune is likely to oblige.

Building works very well other than the already submitted feature requests [that mainly improve dev experience]

But to me it seems best for the coq team to maintain its own stanza frontend for maximum flexibility. Note that this doesn't necessarily entail more work, as you can always just desugar coq specific stanzas to existing dune stanzas.

The thing is that Coq libraries are basically OCaml libraries without .mli. Thus, if you replace .ml by .v, .cmo by .vo, and ocamlc by coqc things work. Even coqdep has the same output format than ocamldep I believe.

It is a very simple model, and my concern was to avoid code duplication.

I think that starting off with the menhir way is sensible. If today's library stanza is deficient in anyway for building coq plugins in OCaml, then those issues should be raised as soon as possible.

Ok, we will try the Menhir way, I will have to get familiar with the codebase. Thus we will basically add a coqlib stanza:

(coqlib
 (name ...)
 (public_name ...)
 (synopsis ...)
 (flags ...)
 (modules ...)
 (recurse ...)
 (libraries ....))

and that is I think.

[ejgallego]

Ok, so I've managed to get something "running" following misc bits here and there. I will be busy for the next few days with other stuff but I think I should be able to produce a first PR on my own. Thanks for all the help!

[rgrinberg]

Yes, that's what we do today. The Coq libraries may depend on the OCaml ones, but not the other way around. [In particular a .vo file may depend on a .cmo file.

Does coqdep discover these coq on ocaml dependencies?

Ok, we will try the Menhir way, I will have to get familiar with the codebase. Thus we will basically add a coqlib stanza:

Regarding the libraries field, do you plan for this to work for both coq and ocaml libraries? Seems like you might want to maintain a different namespace for coq and ocaml libs.

Ok, so I've managed to get something "running" following misc bits here and there. I will be busy for the next few days with other stuff but I think I should be able to produce a first PR on my own. Thanks for all the help!

Awesome, don't hesitate to put up a WIP and ask us any questions you'd like.

[ejgallego]

Does coqdep discover these coq on ocaml dependencies?

Yup, it emits something like that:

theories/Init/Notations.vo theories/Init/Notations.v.beautified: theories/Init/Notations.v plugins/ltac/ltac_plugin.cmxs

Regarding the libraries field, do you plan for this to work for both coq and ocaml libraries? Seems like you might want to maintain a different namespace for coq and ocaml libs.

Indeed even if Coq libraries may include OCaml libs, I think a different namespace does make sense. However note that we would like to use the same exact location machinery, etc... for both of them, as a Coq lib is a superset of an OCaml lib, and in fact we can have the case where coqlib1 defines an OCaml library and coqlib2 defines another OCaml library that needs the OCaml part of coqlib1 to build.

Awesome, don't hesitate to put up a WIP and ask us any questions you'd like.

Great, thanks!

[rgrinberg]

theories/Init/Notations.vo theories/Init/Notations.v.beautified: theories/Init/Notations.v plugins/ltac/ltac_plugin.cmxs

One thing that is puzzling here is that the dependency here is on the entire shared object. There's only one such shared object per library in dune, so it's a bit strange that coqdep is "discovering" it here. Usually such library dependencies are specified explicitly in dune, so I'd expect something like (libraries ltac_plugin)in an appropriate stanza instead. Am I misunderstanding?

Coq lib is a superset of an OCaml lib, and in fact we can have the case where coqlib1 defines an OCaml library and coqlib2 defines another OCaml library that needs the OCaml part of coqlib1 to build.

I see. I understand that a coq library may consist of OCaml and coq code but I'm wondering if it makes sense to keep those separate from the dune point of view. E.g.

(library ;; pure ocaml component
 (name foo))

(coq ;; coq only component but depends on the ocaml
 (ocaml-libraries foo)
 (public_name foo))

This might give flexibility such as keeping the OCaml component private (to prevent it from being used by other OCaml libraries) while keeping the coq library public.

Apologies if not everything I'm saying here is relevant, feel free to just proceed with whatever you have in mind.

[ejgallego]

Hi folks, thanks for your patience, I finally got some code I'm reasonably happy with, see https://github.com/ejgallego/dune/tree/coq

There still are quite a few TODOs, but I don't expect a problem in those except for implementing the notion of "Coq library"; this indeed is going to be tricky as I am not sure how can I get similar functionality to Lib.BD without doing quite a bit of work.

Anyways, even without support for Coq libraries the PR should be ready for review soon, and it would still be useful as it should be able to fully replace coq_makefile.

cc: @anton-trunov

[rgrinberg]

Thanks @ejgallego. Would you mind putting up a PR? I know it's WIP but it will be easier to discuss things there.

[ejgallego]

Thanks @ejgallego. Would you mind putting up a PR? I know it's WIP but it will be easier to discuss things there.

Sure, @rgrinberg thanks! I will submit a PR as soon as I finish some more details and docs.

Note that I was able to port a few key development to Dune without major problems so far.

[ejgallego]

Basic support is in; IMO we can close this issue, further specific points, such as the library model, will be addressed individually.