lake build -j?

Stream: lean4

[Julian Berman]

lake build --help doesn't tell me how I configure its level of parallelism. Does it not have a way exposed? Grepping the source code does seem to show it has a notion of how many jobs to run, is this not exposed to the command line?

[Mac Malone]

lean4#4241

[Henrik Böving]

Currently lake just uses as many threads as the runtime has because it makes use of the Task primitive. You can use the env variable LEAN_NUM_THREADS to set that

[Julian Berman]

Aha! Thanks both of you.