MackieLoeffel (Feb 17 2022 at 07:19): 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?
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
are these Coq packages? Compositional builds don't work for Coq
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.
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.
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
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?
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.)
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)].
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.
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.
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
MackieLoeffel (Feb 17 2022 at 08:25):I see, thanks for the explanation!
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
coqfindis 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.
Rodolphe Lepigre (Feb 17 2022 at 08:50):(I mean, when building a single package.)
Paolo Giarrusso (Feb 17 2022 at 08:55):Does that dummy ocamlfind package lists which theories are included?
Paolo Giarrusso (Feb 17 2022 at 08:57):because that could indeed help (even if Emilio might have wanted to do a cleaner fix)
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.
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.
MackieLoeffel (Feb 17 2022 at 09:03):Indeed, that sounds like be the best solution.
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"
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):a scope is something with a dune-project root
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):the way we do things now, each scope gets its independent databse
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):for ocaml, there is a fallback database
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:17):so all libraries are in the scope-db
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:18):but in the fallback database, only _public_ libs are
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:18):there is a tree here
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
Emilio Jesús Gallego Arias (Feb 17 2022 at 17:18):main trick is actually ordering of initialation
Last updated: Jun 04 2023 at 22:30 UTC