Stream: Dune devs & users

Topic: vos/vok support for dune

Ali Caglayan (Jul 11 2022 at 15:23):

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

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:23):

there are two strategies:

Paolo Giarrusso (Jul 11 2022 at 15:24):

wait — we got vos in already?

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:24):

• have coq_rules generate only one of .vo or .vos target

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)

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:24):

• have coq_rules to output objects in $theory/.vo and $theory/.vos

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:24):

and select accordingly

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:25):

option 2 allows both rules to co-exists

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:25):

does it make sense?

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:25):

@Paolo Giarrusso we only have that for the stdlib

Paolo Giarrusso (Jul 11 2022 at 15:25):

(even vos alone would already be very valuable)

Ali Caglayan (Jul 11 2022 at 15:25):

What is the point of vok files though?

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?

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:26):

should be just a few lines

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:26):

start by coq_module.ml

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:26):

there is a function that returns the object dir

Paolo Giarrusso (Jul 11 2022 at 15:26):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

update it to append .vo to all objects

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

check it works

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

a .vo dir sorry to all object

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

to all objects

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:27):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:28):

that will setup a .vos dir

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:28):

you know what I mean?

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:28):

depending on a flag

Paolo Giarrusso (Jul 11 2022 at 15:28):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:29):

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

Paolo Giarrusso (Jul 11 2022 at 15:34):

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

Paolo Giarrusso (Jul 11 2022 at 15:34):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:35):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:36):

and enable that with some flag

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:36):

that's what we do in coq_dune

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:36):

works well

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)

Ali Caglayan (Jul 11 2022 at 15:36):

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

Ali Caglayan (Jul 11 2022 at 15:36):

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

Ali Caglayan (Jul 11 2022 at 15:37):

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

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

• A.v --[coqc]--> B.vo
• A.v --[coqc -vos]--> B.vos

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!

Paolo Giarrusso (Jul 11 2022 at 15:41):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:43):

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

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

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:44):

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

Paolo Giarrusso (Jul 11 2022 at 15:44):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:44):

Oh, I have other idea

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:44):

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

Paolo Giarrusso (Jul 11 2022 at 15:45):

and profiles would work for that

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

• $theory/foo.vo
• .vos_$theory/foo.vos

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

I think that'd work and allow files to coexists

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

tho

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

when a theory depends on another

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:45):

how do we choose the right object dir?

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:46):

so we have a problem of interface here :S

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:46):

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

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:46):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:47):

all you need to do is to update `Coq_modules

Emilio Jesús Gallego Arias (Jul 11 2022 at 15:47):

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

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

Rudi Grinberg (Jul 11 2022 at 16:45):

Emilio Jesús Gallego Arias said:

• $theory/foo.vo
• .vos_$theory/foo.vos

that's the right way to do it.

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

Rudi Grinberg (Jul 11 2022 at 16:47):

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

• Introduce a -no-vok mode in coq so that it stops producing these junk files.
• Have a way for dune query for the availability of -no-vok. This could rely on the coqc -config PR.

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)

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?)

Rudi Grinberg (Jul 11 2022 at 17:27):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 17:31):

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

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 17:31):

so maybe we just go for the env flag

Emilio Jesús Gallego Arias (Jul 11 2022 at 17:31):

and share the object dir

Rudi Grinberg (Jul 11 2022 at 17:32):

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 17:32):

ah

Emilio Jesús Gallego Arias (Jul 11 2022 at 17:33):

I see, that'd be another approach

Emilio Jesús Gallego Arias (Jul 11 2022 at 17:33):

tho maybe just splitting the objects dirs is ok

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

Rudi Grinberg (Jul 11 2022 at 17:33):

we could also add a vos alias i suppose

Rudi Grinberg (Jul 11 2022 at 17:33):

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

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

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

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

Emilio Jesús Gallego Arias (Jul 11 2022 at 17:50):

the patch tuareg uses is very easy!

Paolo Giarrusso (Jul 11 2022 at 17:51):

agreed

Last updated: Jun 04 2023 at 23:30 UTC