Stream: Dune devs & users

Topic: Multi-package repositories


view this post on Zulip MackieLoeffel (Feb 17 2022 at 07:19):

Can someone explain the text about multi-packages repositories in the dune README? (https://github.com/ocaml/dune#gracefully-handles-multi-package-repositories)
In particular, it says:

When building via Opam, it is able to correctly use libraries that were previously installed, even if they are already present in the source tree

I have an opam file for pkg1 that lives in the same repository as pkg2 and depends on it.

  ["dune" "build" "--display=short" "-p" "pkg1,pkg2" "-j" jobs]

Now if I do opam install pkg1, it first installs pkg2 (as expected), but then when it installs pkg1 it recompiles all the files from pkg2 as well! Based on the text above I would expect that dune automatically detects the situation and does not compile pkg2 twice. Can someone explain what is going on?

view this post on Zulip MackieLoeffel (Feb 17 2022 at 07:35):

If I just use

  ["dune" "build" "-p" "pkg1" "-j" jobs]

I get the following error:

# File "theories/lang/dune", line 7, characters 4-11:
# 7 |     (theories pkg2)
#                   ^^^^
# Error: Theory pkg2 not found

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 07:36):

are these Coq packages? Compositional builds don't work for Coq

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 07:37):

you can still get the effects but that requires some surgery: basically, remove all dune-project but the top-level one.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 07:39):

_However_, even then I'm surprised by (theories pkg2), because theories takes a list of logical prefixes.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 07:40):

For instance, I've locally used (theories iris.heap_lang) to let Iron depend on iris heap_lang

view this post on Zulip MackieLoeffel (Feb 17 2022 at 07:43):

Yes, these are Coq packages (for context, this is the concrete MR I am working on: https://gitlab.mpi-sws.org/iris/refinedc/-/merge_requests/129)
There is only one dune-project. I am not sure what you mean with theories taking a list of logical prefixes. Doesn't it just take a list of names of other coq.theory?

view this post on Zulip MackieLoeffel (Feb 17 2022 at 07:44):

See e.g. https://gitlab.mpi-sws.org/iris/refinedc/-/blob/1b6606a3870798ddc8ed1643d42f95d03974916d/theories/lang/dune
(Note that the MR currently contains a hack to remove all mentions of pkg2 / coq-lithium in the dune files when installing, but I would like to not use that hack.)

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 08:06):

Doesn't it just take a list of names of other coq.theory?

Nevermind, same thing [those names are passed to -Q/-R as well as "logical prefixes" (the manual uses "logical directory" instead, not sure where I picked this up)].

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 08:10):

Anyway, you wrote (theories lithium) not (theories coq-lithium), while the other pkg2 is coq-lithium — so that part seems alright.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 08:12):

I am not 100% confident, but I suspect this cannot be fixed without compositional builds. What that text means is that for OCaml, when pkg2 is installed, dune notices (with ocamlfind) and resolves your dependency against installed libraries. For Coq, it'd need to do the same, but coqfind is not a thing.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 08:18):

and I guess opam stops the build artifacts from pkg2 to be used for pkg1, hence the recompilation

view this post on Zulip MackieLoeffel (Feb 17 2022 at 08:25):

I see, thanks for the explanation!

view this post on Zulip Rodolphe Lepigre (Feb 17 2022 at 08:49):

Paolo Giarrusso said:

I am not 100% confident, but I suspect this cannot be fixed without compositional builds. What that text means is that for OCaml, when pkg2 is installed, dune notices (with ocamlfind) and resolves your dependency against installed libraries. For Coq, it'd need to do the same, but coqfind is not a thing.

Actually, dune creates a dummy ocamlfind package here. I've had a look at the issue, and it seems that the problem comes from the fact that dune searches for the coq-lithium package locally, and not from its installed version. I suspect that this could be fixed by filtering all members of the (theories ...) stanza that are part of other packages.

view this post on Zulip Rodolphe Lepigre (Feb 17 2022 at 08:50):

(I mean, when building a single package.)

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 08:55):

Does that dummy ocamlfind package lists which theories are included?

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 08:57):

because that could indeed help (even if Emilio might have wanted to do a cleaner fix)

view this post on Zulip Rodolphe Lepigre (Feb 17 2022 at 08:57):

No it does not, but my hope was that changing (theories coq-lithium) into (libraries coq-lithium) would help. But it does not.

view this post on Zulip Rodolphe Lepigre (Feb 17 2022 at 09:00):

But really, dune should be able to detect that the coq-lithium package (providing the lithium theory) is installed, and thus do not look for it locally.

view this post on Zulip MackieLoeffel (Feb 17 2022 at 09:03):

Indeed, that sounds like be the best solution.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):

I will get back to you folks, but indeed, if you check where the libraries are scanned, we don't cross "scopes"

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):

a scope is something with a dune-project root

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):

the way we do things now, each scope gets its independent databse

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):

for ocaml, there is a fallback database

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):

so all libraries are in the scope-db

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:18):

but in the fallback database, only _public_ libs are

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:18):

there is a tree here

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:18):

See two prototypes here https://github.com/ejgallego/dune/tree/coq+compose_interscope and https://github.com/ejgallego/dune/tree/coq+compose_interscope2

view this post on Zulip Emilio Jesús Gallego Arias (Feb 17 2022 at 17:18):

main trick is actually ordering of initialation


Last updated: Feb 04 2023 at 02:03 UTC