Stream: Coq devs & plugin devs

Topic: Switching to dune (the compilation of Coq)

view this post on Zulip Enrico Tassi (May 13 2020 at 15:39):

There are the problems as far as I have understood (only the first one was discussed at the Coq call held on 13/5/2020)

  1. support for native, vos and vio
  2. maintenance of the dune build system when Coq evolves

I'm asking my question on 2 here. Today if coqc generates one extra file (or one less, as we hope to do in the future) we can update the rules in the Makefiles. There is no need to patch GNU Make or wait for a release of that tool. I don't understand the story for dune here, since the rules are hard coded in the sources of dune. Even if dune is released often, it may be a bit complicated as a workflow. If this is true, then having all "compilation chains/modes" generate the same files (ideally one single .vo) and having the .cmx generated by native embedded in .vo files as well could simplify this aspect of the switch to dune.

view this post on Zulip Emilio Jesús Gallego Arias (May 13 2020 at 22:39):

Indeed 2 is a very good question, I'll try to summarize what it has been discussed so far. First, we have to split the ML part of Coq vs the .v part. For the ML part, I think that it is reasonable to assume that Dune will be supported and cover Coq use cases in the long-term future. Thus, migration of the ML build to Dune poses little risk [not 0 obviously]

Regarding the .v part, there are different scenarios:

Note that, while more powerful, Dune API is quite straightforward, and it is more accessible IMO to OCaml programmers than make. This is obviously a matter of preferences, but I feel much more comfortable programming build rules in OCaml than I would ever be in make.

It should be noted that part of this worry is shared by OCaml, for example there is natural reluctance to move the build of the compiler itself to Dune on similar concerns; personally I agree and this is why I am not trying to rush a Dune transition anymore, but I'm just happy with keeping the build system as an alternative and happy to bear all the maintenance burden that could arise from it. In my view dune hasn't been such a burden for the rest of developers that don't use it; other than the occasional question about it; when compared to make problems I do believe we have fared significantly better. It is true that duplication of subsystems is a real problem in Coq, but IMHO we have worse significant areas in that for example we could merge the native support tomorrow [even without the smart disabling] and we could remove entirely either Dune or Make and users would see no impact.

If that is a concern for people I think there is also a way to keep dune support in Coq: move the dune build to an allow_failure status and let the dune maintainers take care of fixing it; or even moving the dune infrastructure out of tree. In the end, in what concerns tooling there is not perfect solution, and moving from make does indeed make people nervous and this is not exclusive of the OCaml world, see other systems such as Ninja, etc...

view this post on Zulip Enrico Tassi (May 14 2020 at 07:43):

Ok, I see the plans in case Coq changes its needs in terms of rules, and I'm ok with them. For the 3 subpoints of 1 (native, vos, vio) I have thse comments/questions in addition to what discussed at the Coq call.

1.1 native - I think we should merge the PR as is, later make it optional via profiles

1.2 and 1.3 (vos and vok)

view this post on Zulip Enrico Tassi (May 14 2020 at 07:43):

I forgot: native would be off (by default) in the vio and vos profiles, while it will be on in the regular one

view this post on Zulip Théo Zimmermann (May 14 2020 at 08:37):

figure out clean rules for profile switching (it would help to have a pointer to the coq code in dune where these cleaning rules can be declared)

From what I understood, you don't have to define these clean rules yourself. Dune does it based on the dependency information. As long as the options that you passed to coqc are hashed into the dependency information, you're good to go and Dune will take care of removing outdated files.

view this post on Zulip Enrico Tassi (May 14 2020 at 09:27):

Nice, but where is is "dependency information"? Is it the hash of the vo, or something else? Should we store these compilation flags into the .vo?

view this post on Zulip Théo Zimmermann (May 14 2020 at 09:29):

Again, everything I say should be double-checked with @Emilio Jesús Gallego Arias but I understood that Dune stores this information on the side. So no, it would not be needed to store the compilation flags into the .vo.

view this post on Zulip Emilio Jesús Gallego Arias (May 14 2020 at 11:53):

w.r.t. 1.1: Given that dune by default won't happen for 8.12 I'd rather wait a bit so we are sure we do have a good solution for the dev profile, and configure setting.

Indeed you don't need to figure out clean rules or build rules, Dune understands the targets and flags present in actions and will produce sound rules by default. Regarding vok:

view this post on Zulip Emilio Jesús Gallego Arias (May 14 2020 at 11:53):

Playing with flags is certainly not going to be enough as even if you use the .vo renaming trick, build rules are different. Adding a different rule setup to coq_rules is fairly easy so I'd prefer that route.

view this post on Zulip Théo Zimmermann (May 14 2020 at 12:03):

If build rules are different, there is no point in going this route indeed. This idea only makes sense is build rules are exactly the same.

view this post on Zulip Emilio Jesús Gallego Arias (May 14 2020 at 12:05):

I guess the point of vok/vio is precisely to allow different build rules; I like the idea of .vo files moving to a more incremental format where proof s can be added later, however I'm not sure this is needed at least for the dune setup. As discussed in the call, OCaml profiles already modify build rules for linking -opaque so that is well supported.

view this post on Zulip Enrico Tassi (May 14 2020 at 13:07):

The rules for a .vos or a .vio are the same for .vo (same dependencies, only difference is an extra flag to coqc).
What is different are the rules to turn a .vio into a vo, or to turn a .vos into a .vok, this is the part I think can be modeled with a new @target with a specific rule.
The .aux business can be dropped as well. It serves two purposes: better schedule the vio2vo things (that I propose to drop); use section variables computed by the previous run (if Proof using is missing). This last feature is nice, IMO, but totally optional. I don't know if we can do that with dune or not, but again it is not mandatory.

view this post on Zulip Enrico Tassi (May 14 2020 at 13:09):

To me, the proof using business is maybe where promotion can help, but this requires features on the Coq side that are not there yet.

view this post on Zulip Enrico Tassi (Jun 11 2020 at 13:04):

FTR I've opened

Last updated: Jun 23 2024 at 01:02 UTC