Théo Zimmermann (Mar 21 2023 at 13:37): 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
Ali Caglayan (Mar 21 2023 at 14:04):That should be jobs
Ali Caglayan (Mar 21 2023 at 14:04):I think it was renamed.
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.
Paolo Giarrusso (Mar 21 2023 at 21:16):BTW -j /--jobs is also a command-line option
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.
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"
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: Jun 03 2023 at 18:01 UTC