How to limit the number of concurrent tasks?

Stream: lean4

[Kaiyu Yang]

Hi,

I want to run ~3000 independent tasks in parallel. I tried launching all of them using IO.asTask, but they ate up all CPUs on the cluster. So I'd like to limit the number of concurrent tasks. I tried lean --threads XXX. It works, but is there a way to control it in the program instead of in the command line? Thank you!

[Scott Morrison]

You can alternatively set it via the environment variable LEAN_NUM_THREADS, but there does not appear to be any way to change it once Lean has started up.

[Kaiyu Yang]

Thanks!