lake mathlib cache download on LSP

Stream: lean4

[Siddharth Bhat]

A fresh install of SciLean is failing with:

➜  SciLean git:(master) ✗ lake exe cache get
info: downloading component 'lean'
179.1 MiB / 179.1 MiB (100 %)   2.1 MiB/s ETA:   0 s
info: installing component 'lean'
info: mathlib: URL has changed; deleting './lake-packages/mathlib' and cloning again
info: cloning https://github.com/leanprover-community/mathlib4 to ./lake-packages/mathlib
info: std: URL has changed; deleting './lake-packages/std' and cloning again
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: Qq: URL has changed; deleting './lake-packages/Qq' and cloning again
info: cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
info: aesop: URL has changed; deleting './lake-packages/aesop' and cloning again
info: cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
info: proofwidgets: URL has changed; deleting './lake-packages/proofwidgets' and cloning again
info: cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
info: Downloading proofwidgets/v0.0.13/linux-64.tar.gz
info: Unpacking proofwidgets/v0.0.13/linux-64.tar.gz
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
leantar is too old; downloading more recent version
Attempting to download 3661 file(s)
Downloaded: 3657 file(s) [attempted 3657/3661 = 99%]

Downloaded: 3661 file(s) [attempted 3661/3661 = 100%] (100% success)
Decompressing 3661 file(s)
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error { kind: UnexpectedEof, message: "failed to fill whole buffer" }', /project/src/ltar.rs:57:34
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
u

---

Note that scilean is using the toolchian from the latest mathlib.

The error went away when I re-ran lake exe cache get. Let me reproduce this with RUST_BACKTRACE=1 to understand what's going on.