Cache: adapt message after deleting corrupted files

Stream: mathlib4

[Floris van Doorn]

I just had the interaction with lake exe cache get below, on a flaky internet connection. I killed the first command, and even though the second command says Completed successfully!, this did not result in a working cache. If the cache finds any corrupted files, it should tell the user "run lake exe cache get again to get the cache for the remaining files".

Floris@Dell-E MINGW64 ~/projects/mathlib ((a8ea88b6bdf...))
$ lake exe cache get
info: plausible: checking out revision '1603151ac0db4e822908e18094f16acc250acaff'
info: importGraph: checking out revision 'e25fe66cf13e902ba550533ef681cc35a9f18dc2'
info: proofwidgets: checking out revision '6980f6ca164de593cb77cd03d8eac549cc444156'
info: aesop: checking out revision 'c3a19fa17982c5c1413fea335f371869b8b12e1d'
info: Qq: checking out revision 'e1d2994e0acdee2f0c03c9d84d28a5df34aa0020'
info: batteries: checking out revision '5e6a77528fb6cace1f0adf2563e4e1bc1da541ae'
info: Cli: checking out revision 'a0abd472348dd725adbb26732e79b26e7e220913'
✔ [2/12] Built Cache.Lean
✔ [3/12] Built Cache.IO
✔ [4/12] Built Cache.Lean:c.o
✔ [5/12] Built Cache.Hashing
✔ [6/12] Built Cache.IO:c.o
✔ [7/12] Built Cache.Hashing:c.o
✔ [8/12] Built Cache.Requests
✔ [9/12] Built Cache.Main
✔ [10/12] Built Cache.Requests:c.o
✔ [11/12] Built Cache.Main:c.o
✔ [12/12] Built cache
Mathlib repository: leanprover-community/mathlib4
Attempting to download 6503 file(s) from leanprover-community/mathlib4 cache
Downloaded: 6497 file(s) [attempted 6497/6503 = 99%]

Floris@Dell-E MINGW64 ~/projects/mathlib ((a8ea88b6bdf...))
$ lake exe cache get
Mathlib repository: leanprover-community/mathlib4
Attempting to download 4 file(s) from leanprover-community/mathlib4 cache
Downloaded: 4 file(s) [attempted 4/4 = 100%] (100% success)
C:\Users\Floris\.cache\mathlib\4f871e23c54f53bd.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\4b514c407eface50.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\eb470b1ef886832b.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\3870995e1d5528c2.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\16a12f50b94709d9.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\1a7f36fa29e5cd87.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\99eb289c37f6dbaf.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\517faf331baeb36b.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\d707f89b536159bc.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\802ba76a6ae0cdd9.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\f85136b8c5b06fc9.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\a6d55cfefd885ae6.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\41454da78259b9a3.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\b4bf85f633cabdd0.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\d2daa1a65254f488.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\26f68089c03c3c67.ltar: removing corrupted file
C:\Users\Floris\.cache\mathlib\ac7a494c9b708a1a.ltar: removing corrupted file
Decompressing 6853 file(s)
Unpacked in 66635 ms
Completed successfully!

[Mario Carneiro]

A cache that downloads some files is still "working". The cache upstream could be incomplete, or there are errors in the file so only half of the library actually got built. So it's not obvious how to differentiate between "as good as you are likely to get" and "there was an interruption and trying again will have better results". I would actually argue that if trying again will improve matters then cache should just try again on its own