Stream: Dune devs & users

Topic: Multiple `-Q` options per library

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))
  ....)

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

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)

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: Jun 03 2023 at 18:01 UTC