Support for Coq "vos" builds

[rlepigre]

This is an alternative to #4050, implementing @ejgallego's idea from #4050 (comment).

The "vos" mode is enabled using (mode vos) in coq.theory stanzas.

CC @Alizter.

[Alizter]

What happens when a user builds once in VoOnly stops the build realising they should have VosOnly and then continues? Doesn't this make the build inconsistent? IIRC Coq loads vo files if they are available and then vos files in vos mode.

We wouldn't have that problem if Coq rules could be sandboxed, but they cannot today for other unrelated reasons.

To be clear, I am in favour of adding something like this, but last time I worked on it I got blocked by the fragility of the build questions. So I just need to be sure we think through the design.

[rlepigre]

Since you configure vo or vos per theory, you can't have both vo and vos at the same time. Will that not save us?

[Alizter]

The issue is that Coq goes and finds the files itself so if you have a dirty build directory you might corrupt the build. I can try and cook up an example later. Worst case we warn people to clean their builds when using vos.

[rlepigre]

Just added a test, seems to just work to switch to normal mode without cleaning.

[Alizter]

What I am suggesting is the opposite situation. If you had 3 files:

A.v -> B.v -> C.v

Now if I had (mode vo) and built B.vo I would have A.vo and B.vo in my build directory. Now if I switch to (mode vos) I will and build C.vos, Dune will give us: A.vos, B.vos and C.vos. However when compiling C.vos, coqc would have used B.vo rather than B.vos.

This is if I recall what coqc does correctly, since I believe it prefers vo over vos. I could be wrong

[Alizter]

Actually nevermind. Reading the Coq refman I see that vos is indeed preferred over vo. https://coq.inria.fr/refman/practical-tools/coq-commands.html#compiled-interfaces-produced-using-vos

[ejgallego]

It is a pity we can't be more dynamic yet but the patch is a start thanks!

Needs documentation / changes entry, rest looks good to me!

[Alizter]

One more design consideration is if we want users to have to edit their stanzas at all. Perhaps it would be OK to have both rules at the same time as they are independent. We could even add vos to the check alias for example. We could even remove the vos targets from the @default alias.

[ejgallego]

What happens when a user builds once in VoOnly stops the build realising they should have VosOnly and then continues? Doesn't this make the build inconsistent? IIRC Coq loads vo files if they are available and then vos files in vos mode.

You don't have that problem as all the .vo targets in the first run become stale (as rules won't generate them anymore) so Dune will clean them up.

[ejgallego]

Perhaps it would be OK to have both rules at the same time as they are independent

That won't work but the reasons you state, coqc will become non-deterministic.

In order to be able to setup both rules you need indeed to make the targets directory different (and also ensure that rules are lazy enough because 2x rules can be felt I bet)

[Alizter]

@ejgallego It won't become nondeterministic see my retort above.

[ejgallego]

@ejgallego It won't become nondeterministic see my retort above.

If I understood your comment above, you actually are giving an example of a non-determinitic build for C.vos, as it now depends on what was built before.

[Alizter]

No, according to the Coq refman, vos is always preferred in -vos mode.

[ejgallego]

No, according to the Coq refman, vos is always preferred in -vos mode.

The key word is preferred, but still if coqc can't find the vos it will fallback to the vo.

[ejgallego]

Tho indeed maybe the race is for the vo objects, let me check coq's source

[rlepigre]

One question I have is: can we somehow make it so that we can configure the mode in the profile? Is it already possible with what I did?

[Alizter]

@rlepigre We can detect the -vos flag in (coq (flags ...)) if a user has that and prefer the mode that way. I think it is better to do that in a later PR though.

If I am correct about being able to have both the vo and vos rules at the same time, then that would mean we wouldn't need it anyway.

[Blaisorblade]

@Alizter coqc can mix vo and vos files, so you do need separate directories; also the vo build overrides vos/vok files but dune might be able to handle that. And since we need separate profiles, can we use that to enable vos mode?

Let me quote the manual (since there's no anchor to link)

Interaction with standard compilation

When compiling a file foo.v using coqc in the standard way (i.e., without -vos nor -vok), an empty file foo.vos and an empty file foo.vok are created in addition to the regular output file foo.vo. If coqc is subsequently invoked on some other file bar.v using option -vos or -vok, and that bar.v requires foo.v, if Coq finds an empty file foo.vos, then it will load foo.vo instead of foo.vos.

The purpose of this feature is to allow users to benefit from the -vos option even if they depend on libraries that were compiled in the traditional manner (i.e., never compiled using the -vos option).

[ejgallego]

Indeed I'm not sure we have the right mechanism to perform this kind of selection at runtime, it seems to me that using flags is not better than using mode, as both require updating the stanza which we def don't want.

I can't check the exact dependency rules now, so indeed the next step would be to see if we can enable both modes without getting unsoundness as Ali proposes.

In the immediate term, I propose we merge this PR once the docs are added, and continue the discussion in the issue / subsequent PR

[rlepigre]

I guess I need to change the Coq language version @ejgallego?

[Alizter]

@rlepigre You don't need to bump the coq lang version since for Dune 3.8 it will be 0.8 and we haven't released Dune yet.

[ejgallego]

@rlepigre You don't need to bump the coq lang version since for Dune 3.8 it will be 0.8 and we haven't released Dune yet.

Indeed, thanks @Alizter ; the changelog of language versions should make this clear by maybe adding the Dune version next to the coq lang version https://github.com/ocaml/dune/blob/main/doc/coq.rst#coq-language-version

Note that indeed we bumped the lang in the implementation https://github.com/ocaml/dune/blob/main/src/dune_rules/coq/coq_stanza.ml#L4
but not in the docs.

[Alizter]

It will be bumped in the docs, that is what #7384 is about. I don't mind adding the vos doc later as long as you make a note in that PR.

[rlepigre]

Sorry, I'm just only seeing your last messages now: I pushed some documentation, but maybe not exactly what you had in mind. In particular I did not bump the version in the doc, only added a paragraph about the option.

[Alizter]

LGTM I'll let @ejgallego decide when to merge.

[rlepigre]

Actually, we have a CI failure on the test I added: apparently, the output is not consistent with what I get locally. Any clue why this happens @Alizter? I'm running Coq 8.16.0, and CI seems to be using 8.16.1: could that be the reason?

diff --git a/_build/.sandbox/d3bcb07409ea29304d4499ea0e5fe788/default/test/blackbox-tests/test-cases/coq/vos-build.t/run.t b/_build/.sandbox/d3bcb07409ea29304d4499ea0e5fe788/default/test/blackbox-tests/test-cases/coq/vos-build.t/run.t.corrected
index 1b5e703..65ef517 100644
--- a/_build/.sandbox/d3bcb07409ea29304d4499ea0e5fe788/default/test/blackbox-tests/test-cases/coq/vos-build.t/run.t
+++ b/_build/.sandbox/d3bcb07409ea29304d4499ea0e5fe788/default/test/blackbox-tests/test-cases/coq/vos-build.t/run.t.corrected
@@ -35,8 +35,8 @@ Checking that we can go back to vo mode (without cleaning).
 
   $ mv dune-vo dune
   $ dune build --display short --debug-dependency-path @all
-          coqc foo.{glob,vo}
-          coqc bar.{glob,vo}
+          coqc Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
+          coqc Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
   $ dune build --debug-dependency-path @default
   lib: [
     "_build/install/default/lib/base/META"
@@ -44,6 +44,10 @@ Checking that we can go back to vo mode (without cleaning).
     "_build/install/default/lib/base/opam"
   ]
   lib_root: [
+    "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmi"}
+    "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi"}
+    "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs"}
     "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"}
     "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"}
     "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"}

[ejgallego]

@rlepigre the difference you see is because dune's CI test with the coq-native opam package installed

[ejgallego]

We can still improve the docs of the (mode ...) field but IMHO that can be done in a different PR.