Paolo Giarrusso (Jun 06 2022 at 20:46): Paolo Giarrusso (Jun 06 2022 at 20:46):I'm dune-ifying a large project which uses multiple -Q options for a single library — say -Q foo/bar bedrock.foo -Q baz/quux bedrock.baz, but with mutual dependencies across bedrock.foo and bedrock.bar. IIUC, I understand that support for this is not planned in dune, and I'll have to rearrange source code and logical paths accordingly — or split this into multiple libraries? That's what I'll probably be doing, but I wanted to confirm.
Paolo Giarrusso (Jun 06 2022 at 20:47):For simplicity, let's ignore the option of splitting into multiple libraries — I know it's possible, but let's say there are valid internal reasons for this setup.
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:47):@Paolo Giarrusso we could support that but it'd take time
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:49):would be really a single library with multiple binding points, something such as
(coq.theory
(names
(foo/bar as bedrock.foo)
(baz/quux as bedrock.baz))
....)
but looks a bit complex to me, so it'd be good for us to think together was is really going on
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:50):is that setup coming due to file generation?
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:50):Dune can do much better in this front that make
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:51):Something crutial in Dune is to manage the filesystem scan centrally
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:51):so that kind of "distributed setup" complicates code a lot as now dune has to merge to compute the list of files
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:52):this is necessary remember both to have soundness when a file is deleted and to properly account for generated files
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:53):Don't hesitate to open a feature request with a small motivating example, maybe we can do something different that solves the original problem
Paolo Giarrusso (Jun 06 2022 at 20:55):sorry, nevermind I guess, other things have probably more value (currently: vos/vok and dune/IDE integration)
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:56):Rudi had a PR for vos/vok
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:56):however last time I looked into that, the rules for that were crazy
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:56):Coq again doing conditional selection of deps
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:57):based on mtime
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:57):that's in direct conflict with any notion of cache or incremental build
Paolo Giarrusso (Jun 06 2022 at 20:57):IIRC the simple solution was to split vos/vok entirely from vo builds?
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):Yes that's what I did in the vio patch
Rudi Grinberg (Jun 06 2022 at 20:59):Paolo Giarrusso said:
I'm dune-ifying a large project which uses multiple
-Qoptions for a single library — say-Q foo/bar bedrock.foo -Q baz/quux bedrock.baz, but with mutual dependencies acrossbedrock.fooandbedrock.bar. IIUC, I understand that support for this is not planned in dune, and I'll have to rearrange source code and logical paths accordingly — or split this into multiple libraries? That's what I'll probably be doing, but I wanted to confirm.
Aren't directories are a good natural barriers for dependencies? I find it natural to use directories to express how my dependencies flow. E.g. it's nice to assume that if someone depends on anything foo/*.ml then foo/*.ml cannot depend on them back.
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):The problem is that you can request dune to build both the vok and vo files
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):imagine you have 200 cores
Paolo Giarrusso (Jun 06 2022 at 20:59):from my vague recollection, all that was missing was consensus to give up on alternatives — or otherwise, exploring those alternatives properly (but I recommend not)
Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):then that conditional setup becomes racy
Paolo Giarrusso (Jun 06 2022 at 20:59):@Emilio Jesús Gallego Arias yeah and if if you request both, just build both separately even if that repeats work.
Emilio Jesús Gallego Arias (Jun 06 2022 at 21:00):so the solution is to separate, but still we need maybe to fix Coq
Paolo Giarrusso (Jun 06 2022 at 21:00):Fixing Coq would not be required, right?
Emilio Jesús Gallego Arias (Jun 06 2022 at 21:00):as for it to pick the right dep, we could always drop stuff to a .vok dir but that's a pain. But I solved this problem in the vio patch which waiting merge in Coq upstream
Rudi Grinberg (Jun 06 2022 at 21:01):The vok rules never made enough sense to me to create something I was confident enough on the dune side.
Emilio Jesús Gallego Arias (Jun 06 2022 at 21:01):Paolo Giarrusso said:
Fixing Coq would not be required, right?
maybe we need to change the logic for it to always prefer a .vok, I'm not sure how the code stands now
Paolo Giarrusso (Jun 06 2022 at 21:01):can't you make it a separate "profile" or sth?
Paolo Giarrusso (Jun 06 2022 at 21:01):default vs vosvok
Emilio Jesús Gallego Arias (Jun 06 2022 at 21:01):Paolo Giarrusso said:
can't you make it a separate "profile" or sth?
Still that may not help if what Coq is doing is non-deterministic
Emilio Jesús Gallego Arias (Jun 06 2022 at 21:02):Yeah we could use a different context (not profile), but that's a lot of overhead, we can fix it in the obvious way
Paolo Giarrusso (Jun 06 2022 at 21:02):Okay, context — but the different context seems required for existing Coq versions
Emilio Jesús Gallego Arias (Jun 06 2022 at 21:02):Not sure.
Paolo Giarrusso (Jun 06 2022 at 21:03):otherwise, you could manifacture the needed timestamps...
Paolo Giarrusso (Jun 06 2022 at 21:52):[follow-ups moved into https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/vos.2Fvok.20builds)
Last updated: Feb 04 2023 at 02:03 UTC