Stream: Dune devs & users

Topic: vos/vok builds


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:04):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:05):

Actually that was fixed, current code is:

view this post on Zulip 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()

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:06):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:06):

it doesn't use time stamps, but hashes

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:06):

otherwise you can't cache anything

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:06):

sure, I know

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:07):

then you defeat the cache

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:07):

no?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:07):

no, the cache you hardlink

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:08):

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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:08):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:09):

and add/remove the hardlink to vo

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:12):

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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:12):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:12):

yeah, that in Dune cannot be even expressed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:12):

as it is insane

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:13):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:13):

and indeed Dune is right

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:14):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:15):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:15):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:15):

That's a lot of code to modify

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:15):

?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:15):

But you could do that yes

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:16):

easier is to disable the .vo rules

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Jun 06 2022 at 21:17):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:17):

but it is not

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:17):

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

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:18):

that's maybe not so much code

view this post on Zulip 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 .

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:18):

$context_vo and $context_vosvok, but yes

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:19):

or add a flag to Coq

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:19):

@Paolo Giarrusso context is a different thing

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:19):

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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:19):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:20):

that's not so hard actually

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:20):

yeah context is not the right thing for this

view this post on Zulip 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"

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:21):

Yes I know, but here that should be fine

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:25):

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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:25):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:27):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:32):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:33):

ok, I understood

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:33):

so should we remove option 3 from Coq then?

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:35):

I'd make sure that dune avoids using option 3

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:36):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:38):

Option 1 also works without patching Coq

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:38):

it is what I implemented in the coq_dune rules

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:38):

and couldn't be simpler

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:39):

hehe

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

just change

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

in coq_module.ml

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

to say .vos hehe

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

ah, and add the -vos flag to coqc

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:40):

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

view this post on Zulip 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 :-)

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:41):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:44):

you also need to tweak the coqdep parsing likely

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:45):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:45):

so in this case, Dune cleans bar.vo !

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:45):

as it has become, effectively, stale!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Feb 04 2023 at 01:03 UTC