CPU usage

[vadimkantorov]

I'm observing 10% load of a single cpu core (controlled via taskset) when using REPL to verify some lean proofs. Is it expected? Does it mean, I should be able to assign up to 10 REPL processes per core? Or is htop reporting some erroneous metric?

Looking for ways to max out and use all available CPU resources on my machine

Thank you!

[augustepoiroux]

I think it really depends on the tactics used in the lean proofs. Powerful tactics like exact? might use more than 10% of a single cpu core. But I am as clueless as you, so if you run some benchmarks to check this, I am interested in the result.