lake exe cache get slow

Stream: lean4

[Kevin Buzzard]

I haven't touched mathlib in basically a month because of work commitments. Today, on a fast desktop, I checked out a branch of mathlib, did git pull (which produced a ton of output), and then lake exe cache get, which did this:

mathlib$ lake exe cache get
info: downloading component 'lean'
179.8 MiB / 179.8 MiB (100 %)  32.1 MiB/s ETA:   0 s
info: installing component 'lean'
info: std: updating repository './lake-packages/std' to revision '2bb93246d4fd2466a4e8a092015de7d2825e23ef'
info: aesop: URL has changed; deleting './lake-packages/aesop' and cloning again
info: cloning https://github.com/leanprover-community/aesop to ./lake-packages/aesop
info: proofwidgets: URL has changed; deleting './lake-packages/proofwidgets' and cloning again
info: cloning https://github.com/leanprover-community/ProofWidgets4 to ./lake-packages/proofwidgets
info: [0/9] Fetching proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 3860 file(s)
Downloaded: 3860 file(s) [attempted 3860/3860 = 100%] (100% success)
Decompressing 3860 file(s)
unpacked in 105966 ms
mathlib$

Was that nearly-2-minute-wait at the end expected? Everything works fine -- lake build returns instantly, for example. I don't have any clue what is going on behind the scenes here but I thought I'd ask.

[Eric Rodriguez]

how much of that was download? I can confirm that this is pretty much what I see most times I run cache

[Kevin Buzzard]

Oh OK. I didn't ever remember it hitting 100 seconds on this machine but as I say I've not been so active for the last month, and I'm aware that an awful lot has happened :-) I'm just referring to the "unpacked in 100000+ ms" line (which did indeed corresponding with a long wait).

[Mauricio Collares]

This step is disk-bound. Do you have an old hard drive, or perhaps some indexing service working in the background?

[Richard Copley]

Here unpack! takes 41 seconds, or 9 seconds if the destination directory is excluded from antivirus scanning.

[Kevin Buzzard]

Aah, indeed this copy of mathlib is on some random external 1TB drive; I moved my lean 4 projects over to this drive because they were taking up 62 gigs. Thanks Mauricio and Richard! (and sorry that I'm clueless about these matters)