Stream: Coq Platform devs & users

Topic: Meaning of `-jobs`?


view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 20:33):

Which parallelism level is configured by -jobs, and how safe is -jobs=16? The help takes pain to distinguish:

- parallel build of (independent) opam packages
- parallel build inside the make of each opam package

So I'd guess that --jobs is about "parallel make jobs". But what's the opam-level parallelism, is it the same as usual? The help doesn't say.
The help also says:

With 32 GB of RAM a parallel package build with 16 make jobs is recommended.

but surely probably you're not suggesting 16*16 = 256 jobs?

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 21:12):

I now see/recall that the "opam-level parallelism" seems somewhat hardcoded — we talked about this recently — but the help text remains confusing.

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 21:25):

Okay, the numbers are multiplying — $ ps -eo pid,cputime,rss,args | egrep 'coqc' | wc -l shows 40-60 processes. Finally a workload making my fans spin up!

$ opam var jobs
16

view this post on Zulip Michael Soegtrop (Dec 03 2021 at 08:52):

Yes, the numbers are multiplying. The recommendations I give in Coq Platform are based on tests, but I thought about reducing the 16 to 8.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 11:50):

It did work exactly according to your tests, I just didn't expect this much overcommitting to be fine. And as you noted, it's not on some intel laptops...

view this post on Zulip Michael Soegtrop (Dec 03 2021 at 12:22):

Btw.: I test this on a 8 core / 16 thread Ubuntu VM without swap, so if my test passes, it shouldn't swap.

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 13:02):

No swapping, never seen it over 32GB :-). The OS scheduler just did better than I expected with so many threads!


Last updated: Jan 29 2023 at 18:03 UTC