Stream: Coq users

Topic: vos and vok


view this post on Zulip Ralf Jung (Jun 17 2020 at 14:35):

I recently started looking into vos/vok files to make the build more parallel and to be able to quicker go to a particular file without checking all proofs it depends on. my understanding was that "make vos" followed by "make vok" would basically do the same work as "make" but more cleverly organized.
However, now I realized that building the vok file does not depend on the vos file, so all the work on the vos file is done twice! For Iris, that means "make vok" does a lot more work than "make. This makes using vos/vok a very mixed game. Is there any chance this can be fixed? If vok could use the vos file instead of re-doing all that work, that would make it a clear win over normal make, which would be really useful.

view this post on Zulip Enrico Tassi (Jun 17 2020 at 14:40):

Hum, I think you may experience a bug. vok should depend on vos.

view this post on Zulip Ralf Jung (Jun 17 2020 at 14:51):

after a complete "make vok", I am doing:

$ touch theories/binders.v
$ make vok
make[1]: Entering directory '/home/r/Dokumente/Unisachen/iris/stdpp'
COQDEP VFILES
COQC -vok theories/binders.v
make[1]: Leaving directory '/home/r/Dokumente/Unisachen/iris/stdpp'

view this post on Zulip Ralf Jung (Jun 17 2020 at 14:51):

so clearly, vok processing doesnt need the vos file

view this post on Zulip Ralf Jung (Jun 17 2020 at 14:51):

if it was just a case of a missing dependency in the makefile, I'd expect it would error when trying to load the vos file

view this post on Zulip Gaëtan Gilbert (Jun 17 2020 at 14:57):

I'm not sure there's much use in compiling all the .vok instead of a specific one
AFAICT vok is more intended for the workflow where you add a lemma to A.v, compile A,B,C,D with -vos then use the lemma in E.v and check your new proof by compiling E.vok (so you got to skip all the proofs in ABCD trusting that adding a lemma didn't break them until you run your CI)

view this post on Zulip Enrico Tassi (Jun 17 2020 at 14:57):

I've misunderstood. Whant I was saying is that make vos; make vok is incremental

view this post on Zulip Enrico Tassi (Jun 17 2020 at 14:59):

and in particular the second step should scale to -j (all vok target depends on vos, so they can all be done in parallel), while the former target follows topological order (but skips proofs)

view this post on Zulip Enrico Tassi (Jun 17 2020 at 15:00):

the workflow is touch foo.v; make vos; coqide bar.v & make vok

view this post on Zulip Ralf Jung (Jun 17 2020 at 15:11):

@Gaëtan Gilbert my usecase for compiling all vok's is, I did some work in emacs (using vos mode to be quicker), and now before push I want to be reasonably sure everything is consistent

view this post on Zulip Ralf Jung (Jun 17 2020 at 15:11):

"make" would redo all the work that went into producing the vos files

view this post on Zulip Ralf Jung (Jun 17 2020 at 15:12):

so I use "make vok" (and I am okay with not checking universes globally, CI does that)

view this post on Zulip Ralf Jung (Jun 17 2020 at 15:13):

Enrico Tassi said:

the workflow is touch foo.v; make vos; coqide bar.v & make vok

but does the make vok here re-do the work that went into producing the vos files? for iris vos actually takes a while, I suspect some proofs are checked there as e.g. Program Definition does not support async.

view this post on Zulip Enrico Tassi (Jun 17 2020 at 15:14):

yes, vos->vos does the proofs, but also re-does the definitions. if you don't want to redo the definition you need the "proof thunks" that is what vio are for.

view this post on Zulip Enrico Tassi (Jun 17 2020 at 15:15):

vos and vio are the same, but the proof thunks are dropped in vos
so to do the proofs you also have to recompute the state that would be in the thunk

view this post on Zulip Ralf Jung (Jun 17 2020 at 15:22):

hm... IIRC vio had other problems though, like being huge because they transitively include state from all dependencies?

view this post on Zulip Enrico Tassi (Jun 17 2020 at 15:24):

they are large on disk, yep

view this post on Zulip Enrico Tassi (Jun 17 2020 at 15:24):

it's a tradeoff

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 15:25):

well, the implementation is very naive

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 15:25):

we could have a better way of formulating diffs to reduce the memory footprint

view this post on Zulip Enrico Tassi (Jun 17 2020 at 15:26):

indeed

view this post on Zulip Enrico Tassi (Jun 17 2020 at 15:26):

(but it will always be a tradeoff time/space) between vos/vok and vio

view this post on Zulip Ralf Jung (Jun 17 2020 at 15:27):

hm...

view this post on Zulip Paolo Giarrusso (Jun 17 2020 at 16:02):

  1. IIRC my workflow in 8.11.1, after make vos and editing code, was to re-run make vos -jN; make vok -jN — the output of running make vok seemed odd.

view this post on Zulip Paolo Giarrusso (Jun 17 2020 at 16:05):

  1. separately, make vos could be sped up in the future by dune caching, even more than make — it seems dune only recompiles a file if the compiled output of its dependencies changed, so it already ignores minor changes (say to comments) and for vos it could ignore changes to async proofs...

view this post on Zulip Paolo Giarrusso (Jun 17 2020 at 16:07):

/cc @Emilio Jesús Gallego Arias on the dune part — the context is, how to speed up development with vos and vok files, and my idea that dune caching might help


Last updated: Feb 06 2023 at 00:03 UTC