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)
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.
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]
.v part, there are different scenarios:
coq_dune.exewhich is a tool that effectively generates
dunefiles 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.
dunefiles 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...
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)
see if we can come up with an alias @proofcheck that
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:
So to sum up
I forgot: native would be off (by default) in the vio and vos profiles, while it will be on in the regular one
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.
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?
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
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:
.vio, I'm still uncertain, there seems to be some dependency [optional ?] on
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.
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.
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.
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.
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.
FTR I've opened https://github.com/ocaml/dune/pull/3547
Last updated: Jun 09 2023 at 08:01 UTC