Paolo Giarrusso (Jul 07 2020 at 08:27): Paolo Giarrusso (Jul 07 2020 at 08:27):(Repost from https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/dune.20and.20parallel.20builds):
Can I run build multiple Coq projects with dune in parallel? IIRC @Emilio Jesús Gallego Arias said somewhere it’s not supported yet, but I’d like to know better...
Addendum: I was thinking of separate projects...
Karl Palmskog (Jul 07 2020 at 08:38):I'm sure Rudi or Emilio can give exact details, but to me, projects can be "separate" (in the sense of having different opam files, etc.) even if they live in the same repo and have a joint dune-project file. I guess you are referring to the case where "separate" means different repositories and dune-project files.
Paolo Giarrusso (Jul 07 2020 at 08:42):Yes — or different checkouts of the same project, or arbitrary combos. I'm basically asking if I can safely launch multiple dune invocations in parallel — even when using caching.
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:17):@Paolo G. Giarrusso you can use indeed dune in parallel as long as it is not under the same root, that is to say, two dune runs cannot share the same target _build directory.
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:17):there are plans to make this safe too
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:17):as indeed it is a bit of a pain sometimes, like I do dune build @check from emacs
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:17):and some other script does dune build
Paolo Giarrusso (Jul 07 2020 at 13:18):Aaah, that makes much more sense, I had misunderstood your warning
Paolo Giarrusso (Jul 07 2020 at 13:18):can you document this? I could also send a PR, but wouldn't know where
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:19):What documentation are you looking at?
Paolo Giarrusso (Jul 07 2020 at 13:20):not sure where I should look
Paolo Giarrusso (Jul 07 2020 at 13:20):hm, I guess in the section on dune of the Coq manual?
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:20):You have the dune manual indeed
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:20):also the Coq manual has a small dune section
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:20):but indeed this seems like something to be documented in the Dune manual itself?
Paolo Giarrusso (Jul 07 2020 at 13:21):if it's for dune in general, sure — I'm clueless :-)
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:21):The bit of documentation may be already there, the dune manual is OK but still needs a bit of work IMO
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:21):https://dune.readthedocs.io/ that's the dune manual
Paolo Giarrusso (Jul 07 2020 at 13:21):I'm interested in using dune at my new job at Bedrock Systems, at least to supplement our build system — but that will probably involve some coordination
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:22):great
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:22):regarding that bit of documentation, maybe you can open an issue on the dune repos
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:22):indeed it doesn't seem documented in the manual?
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:23):Maybe there should be an "invoking" dune talk.
Karl Palmskog (Jul 07 2020 at 13:23):there is already automation for using dune in the templates in coq-community
Karl Palmskog (Jul 07 2020 at 13:23):if you have a meta.yml and set dune: true there, you can autogenerate dune and dune-project with reasonable defaults, and you get the recommended use of dune in the opam file (and dune is recorded as a dependency).
Paolo Giarrusso (Jul 07 2020 at 13:24):https://dune.readthedocs.io/en/stable/search.html?q=parallel&check_keywords=yes&area=default finds nothing
Paolo Giarrusso (Jul 07 2020 at 13:24):I guess https://github.com/ocaml/dune/issues/236 should be listed under https://dune.readthedocs.io/en/latest/known-issues.html
Paolo Giarrusso (Jul 07 2020 at 13:24):also, renamed — I guess jbuilder is the old name for dune
Paolo Giarrusso (Jul 07 2020 at 13:29):Okay, submitted https://github.com/ocaml/dune/pull/3617, hopefully the text isn't too bad but I don't know the right terminology. Thanks a lot!
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:31):Thanks a lot @Paolo G. Giarrusso !
Emilio Jesús Gallego Arias (Jul 07 2020 at 13:32):Karl Palmskog said:
if you have a
meta.ymland setdune: truethere, you can autogenerateduneanddune-projectwith reasonable defaults, and you get the recommended use of dune in the opam file (and dune is recorded as a dependency).
That's great Karl, I will add a pointer to this to the dune documentation.
Last updated: Oct 13 2024 at 01:02 UTC