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 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: Mar 28 2024 at 23:01 UTC