leantar failed

Stream: mathlib4

[Adam Topaz]

I just got the following error trying to get the cache for mathlib:

$ lake exe cache get
Attempting to download 3223 file(s)
Downloaded: 3223 file(s) [attempted 3223/3223 = 100%] (100% success)
Decompressing 4161 file(s)
/home/adam/.cache/mathlib/d7befb75e607fc04.ltar: failed to fill whole buffer
uncaught exception: leantar failed with error code 1

Anyone else experience this?

[Adam Topaz]

Ok, I tired lake exe cache get in a fresh copy of mathlib4 and I got essentially the same error as above:

No files to download
Decompressing 4161 file(s)
/home/adam/.cache/mathlib/d7befb75e607fc04.ltar: failed to fill whole buffer
uncaught exception: leantar failed with error code 1

[Mario Carneiro]

try deleting the referenced file and try again

[Adam Topaz]

Thanks Mario. That fixed it.

[Michael Stoll]

See also this thread.