leangz error

Stream: mathlib4

[Scott Morrison]

I occasionally get into a state where running lake exe cache get produces:

No files to download
Decompressing 3632 file(s)
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error { kind: UnexpectedEof, message: "failed to fill whole buffer" }', /Users/runner/work/leangz/leangz/src/ltar.rs:57:34
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Running lake exe cache clean, normal behaviour returns!

Could we either have a more helpful error message, or better error recovery?

[Mario Carneiro]

I believe this error means that you have an empty .ltar file in the cache, probably because curl was interrupted before finishing

[Mario Carneiro]

I asked around before and I'm still not sure what the proper behavior is in this case

[Mario Carneiro]

if you give an empty file to tar it also complains

[Mario Carneiro]

oh wait, no this is a different error, one of the contained files was truncated in the middle, i.e. you have the first half of a .ltar file. The cause is probably the same

[Sebastian Ullrich]

Now that we have FS.rename, let's use it to get rid of partial downloads once and for all?