Ralf Jung (Jun 17 2020 at 14:35): 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.
Enrico Tassi (Jun 17 2020 at 14:40):Hum, I think you may experience a bug. vok should depend on vos.
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'
so clearly, vok processing doesnt need the vos file
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
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)
Enrico Tassi (Jun 17 2020 at 14:57):I've misunderstood. Whant I was saying is that make vos; make vok is incremental
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)
Enrico Tassi (Jun 17 2020 at 15:00):the workflow is touch foo.v; make vos; coqide bar.v & make vok
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
Ralf Jung (Jun 17 2020 at 15:11):"make" would redo all the work that went into producing the vos files
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)
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.
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.
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
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?
Enrico Tassi (Jun 17 2020 at 15:24):they are large on disk, yep
Enrico Tassi (Jun 17 2020 at 15:24):it's a tradeoff
Pierre-Marie Pédrot (Jun 17 2020 at 15:25):well, the implementation is very naive
Pierre-Marie Pédrot (Jun 17 2020 at 15:25):we could have a better way of formulating diffs to reduce the memory footprint
Enrico Tassi (Jun 17 2020 at 15:26):indeed
Enrico Tassi (Jun 17 2020 at 15:26):(but it will always be a tradeoff time/space) between vos/vok and vio
Ralf Jung (Jun 17 2020 at 15:27):hm...
Paolo Giarrusso (Jun 17 2020 at 16:02):make vos and editing code, was to re-run make vos -jN; make vok -jN — the output of running make vok seemed odd. Paolo Giarrusso (Jun 17 2020 at 16:05):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... 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: Oct 03 2023 at 04:02 UTC