promising-coq icon indicating copy to clipboard operation
promising-coq copied to clipboard

build.sh spawns too many jobs

Open Janno opened this issue 8 years ago • 1 comments

Currently, make is called with -j, which will spawn as many jobs as there are parallel targets at any given time. On systems with (only) 4 CPUs, this leads to unnecessary contention from the ~8 jobs running simultaneously. Additionally, the memory usage far exceeds my modest 8GB of RAM.

I don't quite know how to make an optional -jN parameter work well with your build.sh setup. In any case, I think it would be safer to not use -j by default.

Janno avatar Mar 13 '17 17:03 Janno

It would be better for build.sh to accept the num_jobs parameter, e.g. ./build.sh 3 spawns three parallel jobs. It will not be super-hard, though I don't have domain knowledge on shell scripting.. In the mean time you can copy-and-paste build.sh into build-single.sh and then edit it ;)

jeehoonkang avatar Mar 14 '17 01:03 jeehoonkang