Spawned >1000 tasks. Have 4 cores, but the program uses 2

Stream: general

[Sofia]

Hello. I have a program which is trying to spawn over a thousand tasks. I have a 4 core laptop with hyperthreading disabled (suspect), but the program only uses 2 cores. The C++ function hardware_concurrency() returns 4, as does nproc. I do not see why Lean's runtime is using only 2 threads.

[Johan Commelin]

Do you invoke lean with the -j flag?

[Sofia]

I'm using lake and built the program, I'm running the program outside of lean itself (I make this clear as I was using #eval !! before noticing I really should be compiling. :P)

So lets go with no?