Stream: Coq devs & plugin devs

Topic: Switching to dune (the compilation of Coq)

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.

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:

• for the short term we can assume Coq Dune support to be maintained and adapting to the needs of Coq; in general, makefile-equivalent support is fairly easy to do [~200 lines of OCaml] . Would that become a problem there are two possible fallback strategies:
  • resurrect coq_dune.exe which is a tool that effectively generates dune files with the right rules for vo , etc... files. This is how we have been doing until recently and it should work fine in the foreseeable future; as of now the build rules are quite verbose but support for makefile-style generic rules is planned to be added in Dune so it would be the case that no tool is needed at all.
  • resurrect the make specific part for vo files. This would be something cool to have now [as I mentioned], we could even use the current work to adapt Coq for dune to just use coq_makefile to build the stdlib.
• in the medium-term , Coq support should become a Dune plugin; there have been already quite a few proposal for a Dune plugin API so people don't have to modify Dune / generate dune files for their particular use case. This has been postponed as more work is going on w.r.t. to the core of Dune, but it is still planned. For example a leading candidate for the test-bed for the pluging API is Coq's test-suite. Once Dune Coq support is a plugin, work on maintaining it should be equivalent to maintaining a make setup with the same set of features.

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

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)

• play with profiles once https://github.com/ocaml/dune/issues/3486 is solved, in a coq branch where -quick and -vos generate .vo files (the other extensions really make no sense oustide the context of make). This choice also simplifies/clarifies the ugly code in vos that says "we may load a vo instead of a vos, if ..." and similarly for "read the vio if more recent than...". That code is, for both compilation chains, a hack to try to deal with the fact that make would put all build artifacts in the same place and that one has to name them differently and that, while you are at it, you try to be opportunistic and load "the best" thing you find.
• 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)
• understand the interaction of composition and profiles

• see if we can come up with an alias @proofcheck that

  • in regular mode, does nothing, since .vo are already complete and proof were checked
  • in vos mode does nothing, since "make vok" essentially amounts to switching to the normal profile. (it should print a message maybe telling you this)
  • in vio mode does coqc -schedule-vio-checking ${ncpu} *.vo (not to be confused with vio2vo, which makes no more sense in this scenario). This checks every proof independently, potentially all in parallel (all proofs of all files). It will still be "unsound" wrt universes (globally) but may come handy in CI if one has many cores.

  Note that this plan for vos and vio drops a couple of features, which I believe are not crucial, but this is only my opinion:

  • make vos; make vok can actually be a bit more parallel, in the second step, than switching to the regular profile (but less than the vio thing), but would not check universes fully
  • make vio2vo can generate proper vo files out of vio files, where proper means that that coqcheck accepts them. Given the IO overhead this did never fly.

  So to sum up

  • the regular profile is the one for releases or users which don't have to recompile huge libraries or that can just wait
  • the vos profile is for rapid hacking: you move a thing here, flip an attribute there, and go back to work on the file you were before quickly rebuilding interfaces, you will check proof later
  • the vio is for CI or users with powerful computers.

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

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.

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?

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.

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:

• Indeed there are two possibilites, use an alias, or a profile; this is being discussed with upstream.
• for .vio, I'm still uncertain, there seems to be some dependency [optional ?] on .aux files too?

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.

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.

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.

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.

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.

Enrico Tassi (Jun 11 2020 at 13:04):

FTR I've opened https://github.com/ocaml/dune/pull/3547

Last updated: Oct 13 2024 at 01:02 UTC