leantar uses only one core?

Stream: lean4

[Jireh Loreaux]

Twice now, with a few week span in-between where this did not happen, leantar takes forever to decompress the cached files. My system is otherwise idle, and it's only using one core. For context, it just took me over 4 minutes to unpack the cache, whereas it normally takes ~7 seconds on my machine. Has anyone else experienced this?

[Kim Morrison]

@Jireh Loreaux, I've been investigating the performance of leantar with different numbers of threads at #mathlib4 > lake exe cache get very slow @ 💬 . Assistance getting some more benchmarking on different machines (as described in that thread) would be great. So far I don't have any guesses about your problem, although I do think I've observed it too!)

[Kevin Buzzard]

Jireh I'm sure you're well aware of this but the speed of the "Decompressing X file(s)" step is highly dependent on disc r/w speed, so maybe your drive is failing or something?