Stream: Dune devs & users

Topic: vos/vok support for dune


view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:23):

Let me start off. Do we need vok? AFAICT it is just a makefile thingright?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:23):

I think that's pretty easy to support as long as you set up rules as we do in coq_dune

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:23):

there are two strategies:

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:24):

wait — we got vos in already?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:24):

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:24):

(old thread https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/vos.2Fvok.20builds, MR https://github.com/ocaml/dune/pull/4050)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:24):

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:24):

and select accordingly

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:24):

if we go for 1, then dune will clean up all the stale .vo files automatically, and switching modes is great if using the cache

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:25):

option 2 allows both rules to co-exists

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:25):

does it make sense?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:25):

@Paolo Giarrusso we only have that for the stdlib

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:25):

(even vos alone would already be very valuable)

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:25):

What is the point of vok files though?

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:26):

I get that producing them is an act of checking, but the files themselves are never needed again right?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:26):

@Paolo Giarrusso I don't have the time to code that, but if you dare to try I can indicate you what code to touch

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:26):

should be just a few lines

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:26):

start by coq_module.ml

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:26):

there is a function that returns the object dir

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:26):

@Ali Caglayan the vok files themselves are just to track if the code has been checked

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

update it to append .vo to all objects

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

check it works

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

a .vo dir sorry to all object

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

to all objects

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

once that is working, add in another commit a mode parameter

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:28):

that will setup a .vos dir

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:28):

this has a problem tho, in that it makes dune build theory/foo.vo fail

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:28):

you know what I mean?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:28):

or @Paolo Giarrusso an easier try is just to replace all .vo by .vos

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:28):

depending on a flag

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:28):

(in a meeting right now, but I/@Rodolphe Lepigre will check later)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:29):

but you have the problem that it is a kind of global switch

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:34):

we always use the cache, and as you point out that's good enough

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:34):

and my colleagues tell me many never use vok — just vos and stepping in the editor

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:35):

then you can just patch dune to substitute .vo for .vos

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:36):

and enable that with some flag

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:36):

that's what we do in coq_dune

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:36):

works well

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:36):

what works bad is the following scenario (would be great if someone could write that down in the Dune issue)

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:36):

Right, we should be discarding vok (or just get Coq not to output it).

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:36):

The ambiguity with the vos /vo rule path is troubling tho

view this post on Zulip Ali Caglayan (Jul 11 2022 at 15:37):

I would suggest having a mode in the stanza we can switch

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:38):

We have file B.v which depends on A , then, if we setup rules

then calling coqc on B.v [it doesn't matter if for .vo or .vos] will try to pick B.vo, and if not present B.vos , IIRC. But there you have a race potentially!

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:41):

@Ali Caglayan but we don't want to change dune files to switch to vos

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:43):

@Paolo Giarrusso , indeed, that can be controlled with a profile for now

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:43):

@Emilio Jesús Gallego Arias letting Coq choose still seems an anti-feature, but we don't have new facts since the last chat

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:44):

I'd be happy not to let Coq choose, but note that this is due to Coq implementing the feature

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:44):

of "incremental compilation" with the wrong tool in this case

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:44):

what I mean is that once dune ensures vos XOR vo, Coq can't choose

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:44):

Oh, I have other idea

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:44):

yes, that's the idea, have Dune enforce that

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 15:45):

and profiles would work for that

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

another idea that maybe works is to setup object files like this

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

I think that'd work and allow files to coexists

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

tho

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

when a theory depends on another

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

how do we choose the right object dir?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:46):

so we have a problem of interface here :S

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:46):

so maybe all rules for .vos set -Q to the .vos object dir

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:46):

this would mean still the user can do dune build theory/foo.vo but for .vos the user has to do dune build .vos_theory/foo.vos

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:46):

that's a bit annoying, but a first step maybe

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:47):

all you need to do is to update `Coq_modules

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:47):

then the rules is the same, with just passing the mode

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 15:47):

as the rule already calls Coq_module to determine where the object files are

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 16:45):

Emilio Jesús Gallego Arias said:

that's the right way to do it.

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 16:46):

Emilio Jesús Gallego Arias said:

this would mean still the user can do dune build theory/foo.vo but for .vos the user has to do dune build .vos_theory/foo.vos

you can add a symlink rule %.vos: .vos_theory/%.vos to improve the UI here

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 16:47):

I didn't read the entire thread, but here's what I recall were the blockers:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:18):

Rudi the -no-vok flag is IMHO optional for now (a nice thing to have)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:19):

Wouldn't the symlink tho create the problem that coqc would then see the file (and the race could re-appear?)

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 17:27):

well if we have the -no-vos/-no-vok for coqc it would prevent that

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:31):

Coq doesn't produce the -vos unless you pass -vos I think

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:31):

tho indeed vos files are not installed, but a build all would produce them too ; umm

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:31):

so maybe we just go for the env flag

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:31):

and share the object dir

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 17:32):

-no-vos is for reading. in other words, prevent coqc from reading .vos files completely.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:32):

ah

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:33):

I see, that'd be another approach

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:33):

tho maybe just splitting the objects dirs is ok

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:33):

not a big deal if the target name is a bit special I think

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 17:33):

we could also add a vos alias i suppose

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 17:33):

for foo.v, we can have @foo.vos

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 17:34):

but it's still an issue if things like PG except the .vos file to be adjacent to the source

view this post on Zulip Rudi Grinberg (Jul 11 2022 at 17:34):

Emilio Jesús Gallego Arias said:

tho maybe just splitting the objects dirs is ok

I think that's needed to workaround the overlapping .glob and .aux target anyway

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 17:50):

the object files aren't adjacent to the real source anyway (only to dune's read-only copy), and we'd like to patch PG for it already

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2022 at 17:50):

the patch tuareg uses is very easy!

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 17:51):

agreed


Last updated: Jan 30 2023 at 18:04 UTC