Stream: Dune devs & users

Topic: Dune concurrency setting


view this post on Zulip Théo Zimmermann (Mar 21 2023 at 13:37):

How does one limit the number of jobs Dune is allowed to run in parallel? The documentation talks about a (concurrency parameter in the config file, but it doesn't seem to actually exist (at least, not as of 3.6, even if it was documented in 3.0): https://dune.readthedocs.io/en/stable/dune-files.html#config

view this post on Zulip Ali Caglayan (Mar 21 2023 at 14:04):

That should be jobs

view this post on Zulip Ali Caglayan (Mar 21 2023 at 14:04):

I think it was renamed.

view this post on Zulip Théo Zimmermann (Mar 21 2023 at 15:12):

Thanks, this works! Any idea when it was renamed? It's really strange that the (lang dune doesn't seem to matter here.

view this post on Zulip Paolo Giarrusso (Mar 21 2023 at 21:16):

BTW -j /--jobs is also a command-line option

view this post on Zulip Ali Caglayan (Mar 22 2023 at 17:05):

lang dune in the config file is really only for parsing the file itself rather than guarding any configuration. Otherwise it would be a nightmare to run with older verisons of Dune.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2023 at 17:09):

Yes not sure the config file is properly versioned, if so that'd be a bug. However that change could have been part of 2.x to 3.x so in that case the breakage was "allowed"

view this post on Zulip Ali Caglayan (Mar 22 2023 at 19:06):

So mystery solved: There was no renaming only incorrect documentaiton. We had the config options only in a man page before and they were recently written into the dune doc. It seems that this is nothing more than a typo. Will be fixed.


Last updated: May 25 2024 at 21:01 UTC