Stream: Dune devs & users

Topic: Multiple `-Q` options per library


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:47):

@Paolo Giarrusso we could support that but it'd take time

view this post on Zulip 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))
  ....)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:50):

but looks a bit complex to me, so it'd be good for us to think together was is really going on

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:50):

is that setup coming due to file generation?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:50):

Dune can do much better in this front that make

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:51):

Something crutial in Dune is to manage the filesystem scan centrally

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:56):

Rudi had a PR for vos/vok

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:56):

however last time I looked into that, the rules for that were crazy

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:56):

Coq again doing conditional selection of deps

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:57):

based on mtime

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:57):

that's in direct conflict with any notion of cache or incremental build

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 20:57):

IIRC the simple solution was to split vos/vok entirely from vo builds?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):

Yes that's what I did in the vio patch

view this post on Zulip Rudi Grinberg (Jun 06 2022 at 20:59):

Paolo Giarrusso said:

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.

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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):

imagine you have 200 cores

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 20:59):

then that conditional setup becomes racy

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:00):

Fixing Coq would not be required, right?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:01):

can't you make it a separate "profile" or sth?

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:01):

default vs vosvok

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:02):

Okay, context — but the different context seems required for existing Coq versions

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2022 at 21:02):

Not sure.

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 21:03):

otherwise, you could manifacture the needed timestamps...

view this post on Zulip 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