promising-coq
promising-coq copied to clipboard
build.sh spawns too many jobs
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.