number of threads for lake build

Stream: lean4

[Floris van Doorn]

Is there a way to specify the number of cores lake build is allowed to use (similar to -j in make)?
Reason: On my office computer, when running lake build on Mathlib, all other programs start to lag/be unresponsive
(This is on Debian GNU/Linux 11 (bullseye), with GUI LXQt)

[Henrik Böving]

$ export LEAN_NUM_THREADS=number
$ lake build

[Floris van Doorn]

Thanks!

[Gavin Zhao]

Is there no command-line flag for this?

[Gavin Zhao]

Also is the existence of LEAN_NUM_THREAD documented somewhere? I couldn't find it in the lake README or the manual.

[Gavin Zhao]

It's pretty common for build tools to have a flag -j or --jobs to specify this on the command-line so I think lake should have it as well.

[Mac Malone]

Lake lacks a -j option because Lean did not (and I believe still does not) provide a way for user programs (like Lake) to lmit the number of threads in its Task thread pool.

[Mac Malone]

While this is something that will hopefully be provided in the future, it has not yet appeared to be major issue and thus a fix has not been priotized.

[Mac Malone]

(and LEAN_NUM_THREADS serves a good-enough fix for the few places this has been issue)

[Bhavik Mehta]

Lean has a -j option, printed by lean --help eg by this: https://github.com/leanprover/lean4/blob/3bab621364f87e8884927361b992a2b26b53c983/src/Lean/Shell.lean#L143

[Mac Malone]

It certainly does! That is because its main function is written in C++.