vos/vok builds · Dune devs & users

I'm dune-ifying a large project which uses multiple -Q options for a single library — say -Q foo/bar bedrock.foo -Q baz/quux bedrock.baz, but with mutual dependencies across bedrock.foo and bedrock.bar. IIUC, I understand that support for this is not planned in dune, and I'll have to rearrange source code and logical paths accordingly — or split this into multiple libraries? That's what I'll probably be doing, but I wanted to confirm.

Aren't directories are a good natural barriers for dependencies? I find it natural to use directories to express how my dependencies flow. E.g. it's nice to assume that if someone depends on anything foo/*.ml then foo/*.ml cannot depend on them back.

Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):

The problem is that you can request dune to build both the vok and vo files

Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):

imagine you have 200 cores

Paolo Giarrusso (Jun 06 2022 at 20:59):

from my vague recollection, all that was missing was consensus to give up on alternatives — or otherwise, exploring those alternatives properly (but I recommend not)

Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):

then that conditional setup becomes racy

Paolo Giarrusso (Jun 06 2022 at 20:59):

@Emilio Jesús Gallego Arias yeah and if if you request both, just build both separately even if that repeats work.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:00):

so the solution is to separate, but still we need maybe to fix Coq

Paolo Giarrusso (Jun 06 2022 at 21:00):

Fixing Coq would not be required, right?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:00):

as for it to pick the right dep, we could always drop stuff to a .vok dir but that's a pain. But I solved this problem in the vio patch which waiting merge in Coq upstream

Rudi Grinberg (Jun 06 2022 at 21:01):

The vok rules never made enough sense to me to create something I was confident enough on the dune side.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:01):

Paolo Giarrusso said:

Fixing Coq would not be required, right?

maybe we need to change the logic for it to always prefer a .vok, I'm not sure how the code stands now

Paolo Giarrusso (Jun 06 2022 at 21:01):

can't you make it a separate "profile" or sth?

Paolo Giarrusso (Jun 06 2022 at 21:01):

default vs vosvok

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:01):

Paolo Giarrusso said:

can't you make it a separate "profile" or sth?

Still that may not help if what Coq is doing is non-deterministic

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:02):

Yeah we could use a different context (not profile), but that's a lot of overhead, we can fix it in the obvious way

Paolo Giarrusso (Jun 06 2022 at 21:02):

Okay, context — but the different context seems required for existing Coq versions

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:02):

Not sure.

Paolo Giarrusso (Jun 06 2022 at 21:03):

otherwise, you could manifacture the needed timestamps...

Paolo Giarrusso (Jun 06 2022 at 21:04):

ensure vos is newer for a vos build, that the vo is newer for a vo build, and insert locking against building both in parallel.

Paolo Giarrusso (Jun 06 2022 at 21:04):

doesn't seem a good idea, but seems required without separate directories (hence contexts IIUC)

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:05):

Actually that was fixed, current code is:

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:05):

let select_vo_file ~find base =
  let find ext =
    try
      let name = Names.Id.to_string base ^ ext in
      let lpath, file = find name in
      Some (lpath, file)
    with Not_found -> None in
  (* If [!Flags.load_vos_libraries]
        and the .vos file exists
        and this file is not empty
     Then load this library
     Else load the most recent between the .vo file and the .vio file,
          or if there is only of the two files, take this one,
          or raise an error if both are missing. *)
  let load_most_recent_of_vo_and_vio () =
    match find ".vo", find ".vio" with
    | None, None ->
      Error LibNotFound
    | Some res, None | None, Some res ->
      Ok res
    | Some (_, vo), Some (_, vi as resvi)
      when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
      warn_several_object_files (vi, vo);
      Ok resvi
    | Some resvo, Some _ ->
      Ok resvo
    in
  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()

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:06):

@Paolo Giarrusso "newer" is a useless notion in Dune

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:06):

it doesn't use time stamps, but hashes

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:06):

otherwise you can't cache anything

Paolo Giarrusso (Jun 06 2022 at 21:06):

sure, I know

Paolo Giarrusso (Jun 06 2022 at 21:07):

and that's why it can tell Coq which file to use by manufacturing timestamps.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:07):

then you defeat the cache

Paolo Giarrusso (Jun 06 2022 at 21:07):

no?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:07):

no, the cache you hardlink

Rudi Grinberg (Jun 06 2022 at 21:08):

There is some computation to be shared for building vos and vo files, right? Why can't it be done in a separate step?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:08):

But note the rules above, the newer nonsense was dropped from .vos

Paolo Giarrusso (Jun 06 2022 at 21:08):

okay, but preserving the original timestamp isn't important?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:08):

I am not expert on that but seems like you would have to write to the cache for a read action

Paolo Giarrusso (Jun 06 2022 at 21:09):

anyway, with the code above, you can just add or remove the hardlink to the vos file.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:09):

Rudi Grinberg said:

There is some computation to be shared for building vos and vo files, right? Why can't it be done in a separate step?

Because Coq knows nothing about incrementality

Paolo Giarrusso (Jun 06 2022 at 21:09):

and add/remove the hardlink to vo

Paolo Giarrusso (Jun 06 2022 at 21:10):

in fact, you might need that anyway if you support older releases — but I'm happy enough with 8.15 (or the latest release at the time, but 8.16 isn't out yet)

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:10):

@Paolo Giarrusso how? How would you write the build rule in a way that is deterministic and still fit into Dune's "Memo" engine?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:10):

Only way to support .vos is to disable the rules for all .vo in the workspace

Paolo Giarrusso (Jun 06 2022 at 21:11):

let's go a step back — which libraries should be loaded? IMHO, vos builds should only load vos files, and vo builds should only load vo files. Makes sense?

Paolo Giarrusso (Jun 06 2022 at 21:11):

also, separate build output folders achieve that — you say they add overhead, but what overhead is that?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:12):

@Paolo Giarrusso yes, but current Coq, when generating a .vo file, it also writes a 0-size .vos

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:12):

as make can't handle stale files....

Paolo Giarrusso (Jun 06 2022 at 21:12):

yes, so the vo folder will also contain empty vos, which Coq will not read.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:12):

so what they are trying to do is a poor man form of incrementality

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:12):

yeah, that in Dune cannot be even expressed

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:12):

as it is insane

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:13):

Dune will complain with "foo.vos is generated by two different rules"

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:13):

and indeed Dune is right

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:13):

when demanded to build foo.vos , Dune can't choose the rule to execute

Rudi Grinberg (Jun 06 2022 at 21:13):

For OCaml code, we keep separate obj dirs for bytecode and native. Seems like it would be the same thing here? As long as we get rid of the annoying behavior Emilio pointed out

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:13):

make just ignores the .vo rule as producing a target, but it doesn't track targets anyways

Paolo Giarrusso (Jun 06 2022 at 21:13):

but must the vo rule actually output the vos file? Coqc will produce it, but the rule could delete it?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:14):

so .vos is hopeless for git bisect etc...

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:14):

Paolo Giarrusso said:

but must the vo rule actually output the vos file? Coqc will produce it, but the rule could delete it?

You got Dune confused now, as a target was modified without it realizing

Rudi Grinberg (Jun 06 2022 at 21:14):

Paolo Giarrusso said:

but must the vo rule actually output the vos file? Coqc will produce it, but the rule could delete it?

We could sandbox the vo producing rule to discard the annoying .vos file coq spits out. Although sandboxing would be expensive here

Paolo Giarrusso (Jun 06 2022 at 21:15):

yeah, I keep saying "different folders" and you keep saying "expensive" without explaining...

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:15):

Still you don't have this "poor man" incremental feature.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:15):

That's a lot of code to modify

Paolo Giarrusso (Jun 06 2022 at 21:15):

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:15):

But you could do that yes

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:16):

but Coq semantics for -Q with recursive scanning means that's a lot of code to touch in Dune

Paolo Giarrusso (Jun 06 2022 at 21:16):

I don't care for the incrementality that Coq attempts to do, and it's pointless anyway... if a file depends on N other libraries, we get more than 2^N variants

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:16):

easier is to disable the .vo rules

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:17):

Well actually the incrementality Coq is trying to is what @Rudi Grinberg was asking, it should be possible to do .vos to .vo

Rudi Grinberg (Jun 06 2022 at 21:17):

How does coq know where to put the hidden .vos file?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:17):

but it is not

Paolo Giarrusso (Jun 06 2022 at 21:17):

would it not be possible to use _build/vosvok or such instead of _build/default, or something similar?

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:17):

@Rudi Grinberg Coq can take -o to set output dir/file

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:17):

@Paolo Giarrusso yes you could use _build/$context/theory/.vo and _build/$context/theory/.vos etc...

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:18):

that's maybe not so much code

Rudi Grinberg (Jun 06 2022 at 21:18):

Can we setup the vo rules to do this:

coqc foo.v -o /tmp/foo.v/foo.vo
mv /tmp/foo.v/foo.vo .

Paolo Giarrusso (Jun 06 2022 at 21:18):

$context_vo and $context_vosvok, but yes

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:18):

Rudi Grinberg said:

Can we setup the vo rules to do this:
coqc foo.v -o /tmp/foo.v/foo.vo
mv /tmp/foo.v/foo.vo .

For the empty .vos problem? I'd rather just patch Coq and remove that feature

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:19):

or add a flag to Coq

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:19):

@Paolo Giarrusso context is a different thing

Paolo Giarrusso (Jun 06 2022 at 21:19):

@Emilio Jesús Gallego Arias but the Coq patch would require 8.16 or 8.17

Paolo Giarrusso (Jun 06 2022 at 21:19):

oh, I see — .vo and .vos are output folders

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:19):

Yes, but if you do different output folders you don't need a patch

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:20):

that's not so hard actually

Rudi Grinberg (Jun 06 2022 at 21:20):

Honestly I'd caution using contexts for this. Contexts seem fine until your build query is a bit more complex.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:20):

yeah context is not the right thing for this

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:20):

but easiest is just "when in vos mode, just don't setup the rules for .vo, but for .vos"

Rudi Grinberg (Jun 06 2022 at 21:20):

Emilio Jesús Gallego Arias said:

Yes, but if you do different output folders you don't need a patch

Just remember that dune like it when you write stuff to only a single folder. We had this false start with native once. I'm sure you remember...

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:21):

Yes I know, but here that should be fine

Rudi Grinberg (Jun 06 2022 at 21:21):

Emilio Jesús Gallego Arias said:

but easiest is just "when in vos mode, just don't setup the rules for .vo, but for .vos"

Dune loads rules lazily, so you don't need to worry about that. It's just matter of factoring them into different dirs

Paolo Giarrusso (Jun 06 2022 at 21:22):

okay, it sounds like you dune experts have found some easy way to express "different output folders" that fits dune :-)

Paolo Giarrusso (Jun 06 2022 at 21:23):

and it also sounds like that need not depend on Coq patches, so it'll work at least for 8.15 and probably for past releases

Paolo Giarrusso (Jun 06 2022 at 21:24):

even if some of those use timestamps, IIUC you wouldn't give them the chance to pick the wrong thing

Paolo Giarrusso (Jun 06 2022 at 21:25):

only choice left: what should dune coq top load, vos or vo (cc @Rodolphe Lepigre )? The simple/robust thing seems to let the user choose instead of making up some heuristic.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:25):

Need to go folks, but that's my understanding of .vos:

option one is just have a flag that setup the rules to use .vos instead of .vo ; that way, a .vo file can never appear before the .vos producing a non deterministic build, that's as simple as to change the extension in the current setup and pass -vos
option two is to have two output directories for Coq_lib.obj_dir , so when calling coqc -R dir name , diris pointing to the corresponding object dir for the current mode
option three would be to do as Coq does, but this is not possible due to ambiguity as Dune has no way to guess the intent of the user when building the deps for a .vos file , unless I'm missing some API that would allow us to query Dune "is bar.vo up to date? Then, for foo.vos, use bar.vo as a dep instead of bar.vos"

Paolo Giarrusso (Jun 06 2022 at 21:25):

(If somebody has a good heuristic it could be added later)

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:26):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

but easiest is just "when in vos mode, just don't setup the rules for .vo, but for .vos"

Dune loads rules lazily, so you don't need to worry about that. It's just matter of factoring them into different dirs

Yes you don't need to worry as long as coqc don't see the .vo when in .vos mode, otherwise Dune will think coqc is picking foo.vos but it is gonna pick foo.vo. Sandboxing would help here yes!

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:26):

Paolo Giarrusso said:

only choice left: what should dune coq top load, vos or vo (cc Rodolphe Lepigre )? The simple/robust thing seems to let the user choose instead of making up some heuristic.

yes, you can use a flag to dune coq top for that

Paolo Giarrusso (Jun 06 2022 at 21:26):

@Emilio Jesús Gallego Arias I don't think we want option 3 ever: bar.vo and bar.vos can have different interfaces (universe constraints) for the same theorems, so foo.vos would depend on this choice.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:27):

Paolo Giarrusso said:

Emilio Jesús Gallego Arias I don't think we want option 3 ever: bar.vo and bar.vos can have different interfaces (universe constraints) for the same theorems, so foo.vos would depend on this choice.

That's what happens today with regular coq_makefile right?

Paolo Giarrusso (Jun 06 2022 at 21:27):

yes, and without caching it's not so terrible.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:27):

The idea being "if you have paid the effort to build bar.vo , check foo.vos with the more exact constraint

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:28):

Paolo Giarrusso said:

yes, and without caching it's not so terrible.

Umm, you want what happens today (option 3) or not?

Paolo Giarrusso (Jun 06 2022 at 21:29):

option 3 seems tempting but too much trouble, because foo.vos is not deterministic, so if I use it in baz.vos then I'd keep getting cache misses

Paolo Giarrusso (Jun 06 2022 at 21:30):

it's easy to draw examples where foo.vos loads N libraries and exists in 2^N variants, with a 2-layer dependency tree.

Paolo Giarrusso (Jun 06 2022 at 21:32):

with 3 layers, I think I can get (2^N)^N variants

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:33):

ok, I understood

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:33):

so should we remove option 3 from Coq then?

Paolo Giarrusso (Jun 06 2022 at 21:35):

I'd make sure that dune avoids using option 3

Paolo Giarrusso (Jun 06 2022 at 21:36):

and your option 2 plan seems to guarantee that, even without changes to Coq.

Paolo Giarrusso (Jun 06 2022 at 21:36):

if you're using coqc from coq_makefile, so without a cache, then my argument doesn't apply.

Paolo Giarrusso (Jun 06 2022 at 21:37):

and I'd probably remove option 3 from Coq if we've all switched to dune or at least by the time we've stopped caring.

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:38):

Option 1 also works without patching Coq

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:38):

it is what I implemented in the coq_dune rules

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:38):

and couldn't be simpler

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:39):

hehe

Paolo Giarrusso (Jun 06 2022 at 21:39):

could be but no comment — there are some details I don't follow, but I should let you go

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

just change

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

  let obj_files =
    match obj_files_mode with
    | Build -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ]
    | Install -> [ x.name ^ ".vo" ]
  in

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

in coq_module.ml

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

to say .vos hehe

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

ah, and add the -vos flag to coqc

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

you are good to go, you got a .vos build

Paolo Giarrusso (Jun 06 2022 at 21:41):

I don't get why the spurious .vo don't get in the way, but if they don't that's great :-)

Paolo Giarrusso (Jun 06 2022 at 21:41):

let's forget the vok build, but hopefully that's easy

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:44):

you also need to tweak the coqdep parsing likely

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:45):

or to rename .vo to .vos there, but it works

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:45):

Paolo Giarrusso said:

I don't get why the spurious .vo don't get in the way, but if they don't that's great :-)

it doesn't get in the way because dune will see that the rule producing (for example bar.vo) is gone

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:45):

so in this case, Dune cleans bar.vo !

Emilio Jesús Gallego Arias (Jun 06 2022 at 21:45):

as it has become, effectively, stale!

Paolo Giarrusso (Jun 06 2022 at 21:46):

@Rudi Grinberg since vok was confusing, I'd say the TLDR is: today if a vok file exists and is up-to-date (wrt the .v), it means the implementation in .v actually typechecks.

Paolo Giarrusso (Jun 06 2022 at 21:47):

if you build a vos from the same source, then the vok will also match that implementation.

Paolo Giarrusso (Jun 06 2022 at 21:49):

it seems that in coq_makefile the foo.vok does not depend on the foo.vos, but that part is likely worth discussing more deeply.

Rudi Grinberg (Jun 07 2022 at 00:57):

let me try and refresh my vos PR then. I'lll ask @Ali Caglayan or @Emilio Jesús Gallego Arias to help out on the coq side. Just to re-iterate, conditional are the wrong way to go IMO and we avoid them as much as possible in dune. They work very poorly in practice with build requests, watch mode, editor integration etc. Consider how painful it would be to work with dune's OCaml rules if bytecode and native rules were mutually exclusive in the same build.

Rudi Grinberg (Jun 07 2022 at 00:58):

There are some cases where dune lacks the api to define all rules at once, so conditional rules become a last result

Emilio Jesús Gallego Arias (Jun 07 2022 at 07:29):

Yes @Rudi Grinberg , IMHO non-ambiguos conditionals have their use case, but in this case we just have an ambiguous build path

Emilio Jesús Gallego Arias (Jun 07 2022 at 07:30):

The feature that is implemented makes sense tho, if you did check the proofs of module foo, generating foo.vo, then it makes sense to be incremental and use foo.vo in the rev deps of foo instead of generating another foo.vos

Emilio Jesús Gallego Arias (Jun 07 2022 at 07:30):

However as proofs are intra-object files, here we hit the limitation of Dune's granularity being currently at the file level

Rudi Grinberg (Jun 07 2022 at 15:02):

Emilio Jesús Gallego Arias said:

The feature that is implemented makes sense tho, if you did check the proofs of module foo, generating foo.vo, then it makes sense to be incremental and use foo.vo in the rev deps of foo instead of generating another foo.vos

On its own, this might not sound bad. But if we think about it how large builds are supposed to work, it is actually defeating the dune cache. If there are multiple dependency closures for a single target, it means that we are going to mostly miss the cache.

As I said earlier, if you want to be friendly to dune, you should save the intermediate work in some other target.

Paolo Giarrusso (Jun 07 2022 at 18:49):

I think I agree with @Rudi Grinberg here — IIUC what “dependency closure” means (a complete set of dependencies), my earlier argument is that there are exponentially many such closures for each file, so the cache is defeated pretty badly.

Emilio Jesús Gallego Arias (Jun 07 2022 at 19:22):

Indeed, the cache is defeated for the reason I point out: file-based incremental computation does fit the proof document model well

Rudi Grinberg (Jun 07 2022 at 19:23):

Emilio Jesús Gallego Arias said:

However as proofs are intra-object files, here we hit the limitation of Dune's granularity being currently at the file level

We'll think about how to lift that limitation with the DAP

Last updated: Oct 13 2024 at 01:02 UTC