(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...
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
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.
@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
there are plans to make this safe too
as indeed it is a bit of a pain sometimes, like I do
dune build @check from emacs
and some other script does
Aaah, that makes much more sense, I had misunderstood your warning
can you document this? I could also send a PR, but wouldn't know where
What documentation are you looking at?
not sure where I should look
hm, I guess in the section on dune of the Coq manual?
You have the dune manual indeed
also the Coq manual has a small dune section
but indeed this seems like something to be documented in the Dune manual itself?
if it's for dune in general, sure — I'm clueless :-)
The bit of documentation may be already there, the dune manual is OK but still needs a bit of work IMO
https://dune.readthedocs.io/ that's the dune manual
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
regarding that bit of documentation, maybe you can open an issue on the dune repos
indeed it doesn't seem documented in the manual?
Maybe there should be an "invoking" dune talk.
there is already automation for using dune in the templates in coq-community
if you have a
meta.yml and set
dune: true there, you can autogenerate
dune-project with reasonable defaults, and you get the recommended use of dune in the opam file (and dune is recorded as a dependency).
https://dune.readthedocs.io/en/stable/search.html?q=parallel&check_keywords=yes&area=default finds nothing
I guess https://github.com/ocaml/dune/issues/236 should be listed under https://dune.readthedocs.io/en/latest/known-issues.html
also, renamed — I guess
jbuilder is the old name for
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!
Thanks a lot @Paolo G. Giarrusso !
Karl Palmskog said:
if you have a
dune: truethere, you can autogenerate
dune-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: Jun 03 2023 at 17:29 UTC