[coq] Add .vos support

[rgrinberg]

We now build and install .vos files. This requires us to parse coqdep
with -vos and setup a .vos rule for every file.

[rgrinberg]

I'd add .vok support too, but it will require a little more jiggering. The .glob and .aux targets of .vok overlap with the .vo targets so we need to go through a temporary directory + copy.

[ejgallego]

Thanks @rgrinberg , so cool, I'll have a look.

I'd add .vok support too, but it will require a little more jiggering. The .glob and .aux targets of .vok overlap with the .vo targets so we need to go through a temporary directory + copy.

You should be able to disable those using command line flags.

[ejgallego]

Tho it could indeed make sense to have different object directories à la OCaml, for .vo, .vos etc...

[ejgallego]

Tho it could indeed make sense to have different object directories à la OCaml, for .vo, .vos etc...

This may be safer in the long run, as one of the very tricky features on the upstream implementation of .vos support is that when Coq is doing a require, it will look for .vos and .vo files and use some strange rules to decide which one to load when present.

So indeed, having a clear control over the Coq's loadpath could help avoid this kind of situations and provide better incrementality.

[rgrinberg]

You should be able to disable those using command line flags.

It's only possible to disable .glob files. I don't see a way to disable .aux files.

This may be safer in the long run, as one of the very tricky features on the upstream implementation of .vos support is that when Coq is doing a require, it will look for .vos and .vo files and use some strange rules to decide which one to load when present.

Sounds good. What about the installation layout? Do we flatten .vo and .vos files there? It seems like we should keep things separate there, but it will make it really hard for make files.

[rgrinberg]

Another downside of having a separate object directory for .vos files: users aren't going to be able to do $ dune build ./foo.vos as the .vos targets will be hidden in a sub directory. Probably not a huge a deal, as we have two standard workarounds:

• Just have a @vos alias
• Allow them to $ dune build %{vos:./foo} instead

[ejgallego]

Will have a closer look soon, but we have the same problem here with native, this feature was introduced in Coq 8.11 so we need to guard the feature under a new coq lang flag [or if we could get the major coq version reliably then with the Coq version]

[ejgallego]

[rebased]

[ejgallego]

This needs to be conditional as to support Coq older than 8.11

[rgrinberg]

But we don't have a way to check the version of Coq. Perhaps it should be enabled explicitly in the project file? E.g. (coq.vos enable)

[ejgallego]

We can also say that (coq lang 0.4) is required and only 8.11 upwards is supported

[ejgallego]

Ok, I had a look and I'm not sure I understand how this is supposed to work from the point of view of the user.

Coq documentation on vos is here https://coq.inria.fr/refman/practical-tools/coq-commands.html#compiled-interfaces

A few comments:

• vos files are not meant to be installed, and if so, they should be installed with zero size. This is a horrible hack to avoid coqc and make-based setups to use stale vos files, as they cannot clean targets, so when coqc writes a .vo file it willl also overwrite the .vos...
• I'm not sure how this is meant to be used, in particular it seems bizarre to me that setup rules for both .vo and .vos. IIUC we should only setup one of the two, as it doesn't make sense to run both coqc and coqc -vos in the same run.

[ejgallego]

There are some other small issues such as duplicate rules when native or extraction are used.

[rgrinberg]

vos files are not meant to be installed, and if so, they should be installed with zero size. This is a horrible hack to avoid coqc and make-based setups to use stale vos files, as they cannot clean targets, so when coqc writes a .vo file it willl also overwrite the .vos...

I'm then confused by this passage from the docs:

When compiling a file bar.v that depends on foo.v (for example via a Require Foo. command), if the compilation command is coqc -vos bar.v or coqc -vok bar.v, then the file foo.vos gets loaded (instead of foo.vo).

How would this work when bar.v is in the workspace and foo.v is part of an installed theory without foo.vos being installed?

I'm not sure how this is meant to be used, in particular it seems bizarre to me that setup rules for both .vo and .vos. IIUC we should only setup one of the two, as it doesn't make sense to run both coqc and coqc -vos in the same run.

If .vos don't need to be installed then it definitely doesn't make sense. In that case it would make sense to make them a part of @check perhaps?

[ejgallego]

How would this work when bar.v is in the workspace and foo.v is part of an installed theory without foo.vos being installed?

Indeed that's a bit confusing, the real code does:

  if !Flags.load_vos_libraries then begin
    match find ".vos" with
    | Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos
    | _ -> load_most_recent_of_vo_and_vio()
  end else load_most_recent_of_vo_and_vio()

so if there is no vos file, Coq will fallback to .vo. Actually, Coq will overwrite the .vos to zero when compiling a .vo file, so it is actually pretty hard to install both .vos and .vo for non-empty .vos files.

How would this work when bar.v is in the workspace and foo.v is part of an installed theory without foo.vos being installed?

It will just use foo.vo, note that this has little performance impact on itself, as the proofs in the vo file are loaded lazily. Only thing that foo.vo contains more than foo.vos from the point of view of a user requiring that lib is information that leaks from proofs, in this case universe constraints.

If .vos don't need to be installed then it definitely doesn't make sense. In that case it would make sense to make them a part of @check perhaps?

Yup, that seems the way to go! I'd keep @check for OCaml targets tho and introduce maybe @vos_check or something like that as it can be very expensive still.

So indeed as to be correct we cannot setup both rules unfortunately, as this would lead to non-determinism, as we have

• coqc foo.v produces foo.vo foo.vos
• coqc -vos foo.v produces foo.vos

So this is very similar to ocamlc / ocamlopt producing both a .cmi files when to .mli is present.

I'm ccing @charguer as he knows all the details.

[charguer]

Thanks @ejgallego for your precise answers.

The .vos business can appear awkward, especially regarding the use of the empty .vos file. This was the price to pay for achieving something usable and backward compatible.

Regarding the basic assumption:

• To compile and distribute a library, you should only care to produce .vo files; coqc will produce empty .vos files, but you would not distribute them.
• To develop a Coq project, you either want a "safe" compilation, and then aim to produce all .vo files; or you want "fast though potentially unsafe" compilation of foo.v, in which case you aim for foo.vok, which depends on bar.vos for all the dependencies. In both cases, installed libraries should be loaded via .vo files; in the second case (fast though potentially unsafe), coqc looks for mylib.vos and does not find it thus loads mylib.vo.

I hope this clarifies the intended usage.

[rgrinberg]

I see. This means that we need to setup sandboxes for the rules as they produce the same target.

Thinking about a setup that makes sense from dune's perspective:

• .vok files are useless to dune and the same mechanism can be achieved with dune's aliases. So coqc -vok foo.v can produce some alias @vok:foo.v with the same effect (dune creates marker files for aliases transparently).

• It would be nice if coqc supported .vos to .vo compilation. This would make it possible to share work as much as possible between the two pipelines.

[charguer]

It would be nice if coqc supported .vos to .vo compilation.

This was the original intention of .vio files, which correspond pretty much exactly to the contents of .vos files plus "suspended proofs" needed to complete to ".vo" files. With two caveats: (1) universes can't be checked on a per-file basis, and (2) the suspended proofs, as implemented, were taking quadratic amount space in a large project (dozens of Gb, for a project whose vo files sum up to no more than a few hundred megabytes).

Due to reason (1), having .vo pipeline reuse the .vos pipeline is doomed to failure. It's tempting to try to make the .vos and the .vo pipeline live completely separately, but then the cost is that (1) the user will often need to recompile .vos file even when the .vo files are already at hand, and (2) we need to distinguish between library files and local files---not an easy thing to do.

[ejgallego]

@rgrinberg another issue we ought to be careful with is what is outlined in coq/coq#13921 , in particular:

• imagine you do dune build @vos, then we get a.vos b.vos.
• then you do regular dune build @vo, which will write {a,b}.vo and truncate {a,b}.vos
• then you do dune build @vos again, will we rebuild the vos?

[Alizter]

@rgrinberg Any progress with this?

[Blaisorblade]

• then you do regular dune build @vo, which will write {a,b}.vo and truncate {a,b}.vos

As you mentioned on zulip, dune should separate vos and vo targets (through different... profiles?); it doesn't need to truncate the vos as long as it knows if it's up-to-date.

I wonder if dune should ask coq to disable the vos truncation (via a new option), since it conceptually belongs in the coq_makefile build system, but actually migrating it there is probably not worth it?

[charguer]

I wonder if dune should ask coq to disable the vos truncation

It's not that simple. The problem is that the behavior of coq is to load whichever is available between .vos and .vo.

One could argue that the issue comes from that behavior: the user should specify whether .vos or .vo files should be loaded. However, there is a quite high cost to this approach, because for every library, one needs a way to indicate whether to load .vos or .vo files. Indeed, for installed libraries it does not make much sense to load .vos files, but for local libraries it can make sense. At the time of developing .vos files, it seemed too impractical to go that way.

Hence, the need to clear .vos files when dumping .vo file, to make sure that coq is not loading stale versions. If you are interested in a different way to do things, my suggestion would be to introduce an option that, in the presence of flags -vos or -vok, allows the user to indicate which libraries should be loaded in .vo format; all the other Require would be loaded in .vos format only (ignoring .vo file if it exists, simply raising an error if the .vos file is not found). I believe that if you follow this discipline you could get away with not truncating the .vos files.

For example, you could call this flag -vos-load-vo LIB1,LIB2, and the syntax -vos-load-vo _ if there are no require of installed library. This flag would mean that .vo production does not need to truncate .vos files AND that .vos and .vok production loads only .vos files, except for LIB1 and LIB2 for which it loads only .vo files. Does that match your idea?

conceptually belongs in the coq_makefile build system

I wouldn't say this. I'd say it is associated with the "make" build system, combined with the behavior of coq for loading libraries.

[Blaisorblade]

-vos-load-vo risks overflowing command-line limits, and would risk adding O(n^2) overhead to a build of n files (for instance if they’re in linear dependencies).

The problem is that the behavior of coq is to load whichever is available between .vos and .vo. [snip]

Sure, but that doesn’t mean that coq must remove vos files, only that the coq + dune combo must handle this problem somehow — and dune has more info. However, dune might not need that option, if it can move and copy files in the right way.

After reading coq/coq#13921, I’d propose that dune default to stop Coq from ever loading vo files in vos mode, by never making them available, to make build outputs more reproducible. I’m not sure if Coq’s current behavior can/should be replicated in dune.

That might mean building and loading vos files when vo ones are available, but I don’t see such a big problem with that, especially with caching. That’d also ignore accurate universes from vo files, but universe-checking requires a full vo build anyway.

(I’m also imagining a tool extracting vos from vo, but if you want deterministic vos builds it’d have to drop the universes from the proofs which sounds controversial and maybe complex, and it doesn’t seem a priority).

[charguer]

I also think it's fine to rebuild vos when vo exists. Generation of vo is something that could run once every night. During the day, I suspect 99% of the users only need vos generation.

If you configure dune to use separate folders for producing vo and vos files you won't have any problem. If dune really is as fancy as I hear, no doubt that it would be able to handle that. Concretely, keep the standard folders for working with vos files only, and set up a totally separate folder for the purpose of building vo files at night.

If I read you well, this would implement your suggestion "I’d propose that dune default to stop Coq from ever loading vo files in vos mode, by never making them available."

PS: If you want to extract a vos from a vo, I think that you can just use cp foo.vo foo.vos and that would work. But you have to make sure that the vo is up to date, and that is nontrivial.

[Blaisorblade]

Agree with 99%.

PS: If you want to extract a vos from a vo, I think that you can just use cp foo.vo foo.vos and that would work. But you have to make sure that the vo is up to date, and that is nontrivial.

That wouldn't guarantee byte-for-byte reproducible outputs, but we can leave that aside.

[rgrinberg]

@Alizter can take over this if he's interested.

[rlepigre]

@Alizter can take over this if he's interested.

That'd be great! Some of us have been dying to get .vos/.vok support!

[ejgallego]

@Alizter can take over this if he's interested.

That'd be great! Some of us have been dying to get .vos/.vok support!

@Alizter has been working on it I think, but actually a quick form of support for it should be just a few lines of code, so let's coordinate in Zulip if you want. The idea is as follows:

• pass a flag to coq_rules.ml (maybe from the workspace or profile, for the first PR you can just make it fixed) that says "vos mode"
• then extend Coq_mode.t with that, and Coq_module.obj_files should do the right thing almost.

thanks to target cleaning, everything should work fine, voilà !