Zulip Chat Archive

Stream: mathlib4

Topic: leantar cache

Matthew Ballard (Jul 17 2023 at 22:59):

I am getting

lake exe cache get!
...
Downloaded: 8 file(s) [attempted 3579/3579 = 100%] (0% success)

on a fresh ~~pull~~ clone of mathlib4

Adam Topaz (Jul 17 2023 at 23:02):

Works for for me, but on a fresh copy of ml4.

Matthew Ballard (Jul 17 2023 at 23:03):

Sorry, unclear. Same conditions as me

Adam Topaz (Jul 17 2023 at 23:03):

oh wait, not it doesn't

Adam Topaz (Jul 17 2023 at 23:04):

it started off fine, but something happened.

Adam Topaz (Jul 17 2023 at 23:05):

$ lake exe cache get!
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
info: cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
info: Downloading proofwidgets/v0.0.11/linux-64.tar.gz
info: Unpacking proofwidgets/v0.0.11/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: [4/9] Compiling Cache.Requests
info: [4/9] Building Cache.Main
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 3579 file(s)
Downloaded: 8 file(s) [attempted 3579/3579 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 8 file(s)
unpacked in 2 ms