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?
merge https://github.com/coq/coq/pull/14625, then stop using Makefile.dune for the test suite
alternatively setting the env variable NJOBS should work
Nice, NJOBS worked
Ali Caglayan has marked this topic as resolved.
@Gaëtan Gilbert <s>Acutally, I haven't got your branch to work</s> Nevermind I am being silly
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
what is the problem? has been running fine for a long time, and moreover it is hygienic
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
Ok, thanks, I guess we should move forward with the port
Absolutely! I look forward to the Dune port. But until then, I will indeed prefer the non-hygienic, but more incremental test-suite build.
Tho we could play some trick with promote + allowing a subtarget as to fix this
Last updated: Nov 29 2023 at 18:01 UTC