Ali Caglayan (Aug 09 2021 at 16:56): Ali Caglayan (Aug 09 2021 at 16:56):I am unable to pass the number of jobs to Makefile.dune when building the test-suite. It seems to default at about 2. Can/should we fix this easily?
Gaëtan Gilbert (Aug 09 2021 at 17:00):merge https://github.com/coq/coq/pull/14625, then stop using Makefile.dune for the test suite
Gaëtan Gilbert (Aug 09 2021 at 17:00):alternatively setting the env variable NJOBS should work
Ali Caglayan (Aug 09 2021 at 17:06):Nice, NJOBS worked
Notification Bot (Aug 09 2021 at 17:07):Ali Caglayan has marked this topic as resolved.
Ali Caglayan (Aug 09 2021 at 19:16):@Gaëtan Gilbert <s>Acutally, I haven't got your branch to work</s> Nevermind I am being silly
Emilio Jesús Gallego Arias (Aug 11 2021 at 19:37):Gaëtan Gilbert said:
merge https://github.com/coq/coq/pull/14625, then stop using Makefile.dune for the test suite
Actually I don't follow why we want people not to do the test-suite from dune
Emilio Jesús Gallego Arias (Aug 11 2021 at 19:38):what is the problem? has been running fine for a long time, and moreover it is hygienic
Gaëtan Gilbert (Aug 11 2021 at 19:39):because being able to run subsets of it is important, and running through dune means the logs end up in _build and get cleaned if you run another dune command
Emilio Jesús Gallego Arias (Aug 11 2021 at 19:40):Ok, thanks, I guess we should move forward with the port
Théo Zimmermann (Aug 11 2021 at 22:25):Absolutely! I look forward to the Dune port. But until then, I will indeed prefer the non-hygienic, but more incremental test-suite build.
Emilio Jesús Gallego Arias (Aug 12 2021 at 12:30):Tho we could play some trick with promote + allowing a subtarget as to fix this
Last updated: Jun 08 2023 at 04:01 UTC