Improve readme about cache

Stream: mathlib4

[Jakub Nowak]

Hi!

I was building mathlib, and I've recently learned that the build shouldn't take few hours, thanks to the cache. The cache got somehow broken on my machine. The steps from "Downloading cached build files" section of readme fixed it for me. The readme does even mention "(Skipping this step means the next step will be very slow.)".
My problem was that I just assumed that a few hours for such a big project is considered fast.
I might be just the single case that had this problem, so maybe there's no need to change anything. But I would like to propose changing the readme. Maybe something like this?

• To obtain precompiled olean files, run lake exe cache get.
• To build mathlib4 run lake build. (This should take just a few minutes on unmodified mathlib. If it tries to compile every file it means cache isn't working.)

[Michael Rothgang]

Good point; I like making this more specific.

[Michael Rothgang]

One complication is that "very fast" and "very slow" depend a lot on my computer. (The computers in CI (i.e., which produce the cache) build all of mathlib is 30, 45 minutes, for example.)

[Michael Rothgang]

Describing the successful case is exactly what I would do also.

[Michael Rothgang]

Maybe you can shorten "a few minutes" to "a minute a most"? I don't know if people consider 10 minutes still "a few".

[Jakub Nowak]

"This shouldn't take longer than a minute" then?

[Jakub Nowak]

Though, it might take a longer than a minute if you're on slow HDD maybe?

[Ben Eltschig]

The decompressing step alone usually takes a couple of minutes for me

[Kevin Buzzard]

Do you have a huge ~/.cache/mathlib directory and if so does deleting it help? The decompressing step can take a while if your drive has slow read/write speed

[Jakub Nowak]

Ben Eltschig said:

The decompressing step alone usually takes a couple of minutes for me

Ah, but the "This shouldn't take longer than a minute" refers to lake build on unmodified mathlib, not lake exe cache get. Yeah for me it can take longer than a minute too.

[Ben Eltschig]

MrQubo said:

Ben Eltschig said:

The decompressing step alone usually takes a couple of minutes for me

Ah, but the "This shouldn't take longer than a minute" refers to lake build on unmodified mathlib, not lake exe cache get. Yeah for me it can take longer than a minute too.

Right, sorry - I misread that somehow.

Kevin Buzzard said:

Do you have a huge ~/.cache/mathlib directory and if so does deleting it help? The decompressing step can take a while if your drive has slow read/write speed

About 10 gigabytes apparently. I would be surprised if deleting that helps with decompression speed, but I guess it's still good to know that that folder is there to free some space from time to time. Thanks :sweat_smile: