Another weird cache logic

Stream: mathlib4

[Sébastien Gouëzel]

I am using lake exe cache get! to avoid the slowness coming from my curl version. I just got

PS C:\Users\Sebastien\Desktop\mathlib4SG> lake exe cache get!
Using cache from origin: sgouezel/mathlib4
Attempting to download 6878 file(s) from leanprover-community/mathlib4 cache
Downloaded: 6561 file(s) [attempted 6878/6878 = 100%] (95% success)
Attempting to download 6878 file(s) from sgouezel/mathlib4 cache
Downloaded: 6665 file(s) [attempted 6878/6878 = 100%] (96% success)

So it found a bunch of files in the leanprover-community/mathlib4, and then it redownloaded all these files from the fork cache. I'm not sure that's intented!

(Still a clear win compared to lake exe cache get, with a 100x speedup :-)

[Matthew Ballard]

Sounds like it is get!ting twice

[Etienne Marion]

This happened to me too.