[coq] Allow Coq libraries to depend on OCaml ones.

[ejgallego]

This commit adds experimental Coq support to Dune. See Dune issue #1446
for more details.

The patch adds a new stanza (coqlib ...) enabled by adding
(using coq 0.1) to dune-project. The stanza looks like:

(coqlib
 (name Ltac2)               ; Determines the `-R .` flag
 (public_name ltac2.Ltac2)  ; Generates install rules to `lib/coq/Ltac2`
 (synopsis "Ltac 2 Plugin") ;
 (libraries ltac2.plugin)   ; ML libraries that the coq lib depend on [`-I` flag]
 (modules :standard)        ; Modifies the default set of modules
 (flags -warn -no-cbv))     ; Flags for `coqc`

The functionality of the mode is basic, but it should suffice to
replace and extend most uses of coq_makefile.

The main remaining issue is the definition of on Coq libraries so we can enable a compositional build.

Local support for Coq libraries should suffice in the short-term. That is to
say, (coq_libraries ....) would only see libraries in the same
scope, and rely on Coq's default rules for the rest.

However, this doesn't seem straightforward. In particular, we may have
to re-implement Lib.DB which is not trivial.

Thanks to all for Dune, comments extremely welcome.

[rgrinberg]

However, this doesn't seem straightforward. In particular, we may have
to re-implement Lib.DB which is not trivial.

Indeed this seems like a problem. Off the top of my head, coq libraries need 2 main capabilities from this module:

• A lazily load database of libraries
• Calculating transitive closures

Things like resolving selects, variants, generation of META are all fairly specific to OCaml libraries.

We have a couple of options to proceed:

• Shoehorn coq libraries into OCaml libraries. Possibly the easiest thing to do, but is quite ugly.

• Coq can have its own library database. This seems preferable, but is a lot harder to do. This can be done by copying the existing the Lib module or start generalizing the Lib module (in particular the db).

We'll have to ask @diml what he thinks is the best way to proceed.

[ejgallego]

"Shoehorning" was my original idea, however I do agree that the current implementation seems cleaner.

I am wondering about the Lib.Sub_system API, I didn't have time to look at it yet but maybe it could be useful.

I guess this will also depend on how #1206 is implemented.

[ghost]

Generalising Lib.DB seems like the most promising approach to me. In general, it is nice if we can make such components reusable. It means that when we finally support plugins, they will come batteries included and adding support for new languages will be easier.

[andreypopp]

Just a small note from me: consider prefix — coqlib vs coq_lib — if coq libraries will be specified as coq_libraries it would be nice to make library stanza itself called coq_lib (for consistency).

[ejgallego]

Just a small note from me: consider prefix — coqlib vs coq_lib — if coq libraries will be specified as coq_libraries it would be nice to make library stanza itself called coq_lib (for consistency).

Sounds good @andreypopp , I will take this into account once the design advances a bit.

The next step here, and one that is crucial to have before this can build Coq well is to add support for recursive Coq libraries , in the style of (include_subdirs qualified).

I am not sure what is the best way to do this right now, but given that I don't include Coq modules in Dir_contents caches yet I may just tweak build_coq_modules to build the list of modules recursively.

With that, and once I fix the "depend on ML libraries" commit [see missing deps_of_caml_libs] Coq itself should be able to build well.

Another source of annoyance is that coqdep doesn't have a -module option yet, and it doesn't seem easy to do due to Coq's capability of having "prefixed" includes; in order to include A.B.C you can do From A Require C and that will work, however coqdep must perform the actual search in the file cache.

[ghost]

Do you think it would acceptable to not support such constructions? In general, having clever implicit dependencies is a pain. We were talking about this with a few other OCaml developers yesterday and we were saying that we wished OCaml had explicit imports rather than ocamldep, as it would make many things much simpler.

[ejgallego]

Do you think it would acceptable to not support such constructions? In general, having clever implicit dependencies is a pain. We were talking about this with a few other OCaml developers yesterday and we were saying that we wished OCaml had explicit imports rather than ocamldep, as it would make many things much simpler.

We could try to deprecate them step by step, as of today unfortunately coqdep does require indeed all the source files to be present and the right flags passed.

[Zimmi48]

BTW @ejgallego two small remarks:

• It's not clear to me and probably other Coq developers / users what are the open design questions here. If you could summarize, maybe we could help without looking at the code itself.
• Can you ensure that the Coq support works well for older Coq versions as well? It seems to me that this is the case with what you propose today, but if this were made to depend on a new -module feature of coqdep this wouldn't be the case anymore. If older versions are supported, this will allow much more rapid adoption of Dune in the community.

[ejgallego]

Thanks a lot @Zimmi48 , indeed sorry if I am maybe not doing the best job on communicating what I am trying to do, most of the time I am learning about things "on the fly", so it is hard to come with a 100% coherent view.

• Can you ensure that the Coq support works well for older Coq versions as well?

Absolutely; this is a top priority for me; if a newer coqdep has more advanced features we should detect them on the fly, otherwise fallback. I guess we will support Coq >= 8.8.

• It's not clear to me and probably other Coq developers / users what are the open design questions here. If you could summarize, maybe we could help without looking at the code itself.

I'd say the main question is about what a "Coq library" is. Currently, we have a model where compilation of a module requires the system to know the module name, and that in fact implies resolution over the global scope. This needs reverse lookup, with has some implications. Also, it is not clear what the exact semantics of prefix and module name are, for example are the following prefix/name pairs equivalent <Coq.Init, Prelude> vs <Coq, Init.Prelude>.

Another topic is indeed static vs dynamic resolution of dependencies.

This also has uncovered some bugs as coqdep / coqtop differ in their implementation.

Another point is native compilation, which turns out to be quite complex.

[Zimmi48]

Also, it is not clear what the exact semantics of prefix and module name are, for example are the following prefix/name pairs equivalent <Coq.Init, Prelude> vs <Coq, Init.Prelude>.

I would say (to use Dune's terminology) that Coq.Init is a library and Prelude is a module. Init is the name of the library and Coq.Init its public name. The possibility for a package to include several library units with a shared prefix is nice to define a common namespace (it is only used by big Coq packages), and this is something that is possible with OCaml too.

Another topic is indeed static vs dynamic resolution of dependencies.

This is indeed an important question. I wish the result to be as close as possible to what Dune has done for OCaml so far. It looks very useful to be able to seamlessly use installed or in-tree dependencies.

[ejgallego]

I would say (to use Dune's terminology) that Coq.Init is a library and Prelude is a module. Init is the name of the library and Coq.Init its public name. The possibility for a package to include several library units with a shared prefix is nice to define a common namespace (it is only used by big Coq packages), and this is something that is possible with OCaml too.

I guess that I would say that Coq.Init is a prefix, so we have a library is a root prefix + a collection of modules, each one with a prefix == [sub directory], plus the actual name. There are some more invariants, for example Coq cannot output object files with a different name than the module.

[ejgallego]

New version pushed, thanks! Comment about how to best locate lib.cmxs may still apply; please check.

[ejgallego]

New version pushed, I think it is starting to shape up, thanks a lot!

I tried to improve the Path.t surgery but actually importing the corresponding parts of Filename is far from trivial so I've kept the current solution.

[rgrinberg]

I've made a couple of tweaks. I think this is good enough to merge.

[rgrinberg]

By the way, I'm not sure how much sense it makes to start versioning at 0.1. The fact that breaking changes are expected should deter you from marking this plugin as 1.0. Allowing for graceful breakage is the reason why we have versions in the first place. In the next version of dune you can easily drop support for 1.0 and support 2.0+ only. Or you can maintain support for both 1.0 and 2.0.

For example, our initial plugin was also incomplete and almost entirely obsolete. It didn't stop us from making it 1.0

[ejgallego]

I've made a couple of tweaks. I think this is good enough to merge.

Thanks @rgrinberg , I am gonna add a couple of further tweaks related to errors and will merge.

By the way, I'm not sure how much sense it makes to start versioning at 0.1. The fact that breaking changes are expected should deter you from marking this plugin as 1.0. Allowing for graceful breakage is the reason why we have versions in the first place. In the next version of dune you can easily drop support for 1.0 and support 2.0+ only. Or you can maintain support for both 1.0 and 2.0.

My plan was to keep 0.1 as "no version really" then make it 1.0 once this sees a bit more testing and Coq stdlib itself is built with Dune. So 1.0 would support Coq 8.6-8.1x? and then we'd do a "2.0" that would support Coq 8.1x- ahead, hopefully fixing some annoying problems with coqdep etc...

How does that sound? IMHO there will be value for supporting 8.8-8.10 for a while.

[rgrinberg]

Feel free to version things however you want. I just prefer to start counting at 1:)

[ejgallego]

Feel free to version things however you want. I just prefer to start counting at 1:)

Yup, we will turn this into "1.0" the moment I am happy with testing .