Zulip Chat Archive

Stream: mathlib4

Topic: No download from cache


Christopher Hoskin (Jun 08 2025 at 18:46):

Maybe it's just me, but I can't download the latest build from the cache:

git checkout main
git pull
rm -rf .lake/
lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '304c5e2f490d546134c06bf8919e13b175272084'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '6c62474116f525d2814f0157bb468bf3a4f9f120'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'f5e58ef1f58fc0cbd92296d18951f45216309e48'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '632ca63a94f47dbd5694cac3fd991354b82b8f7a'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '76a782b161da3faacc43aa5471bbd2e1d262970a'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '36ce5e17d6ab3c881e0cb1bb727982507e708130'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'e312ab8938d5d8783944ff09613f62c9e0306186'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '4f22c09e7ded721e6ecd3cf59221c4647ca49664'
Mathlib repository: leanprover-community/mathlib4
Attempting to download 3016 file(s) from leanprover-community/mathlib4 cache
Downloaded: 0 file(s) [attempted 3016/3016 = 100%] (0% success)
Decompressing 3744 file(s)
Unpacked in 1586 ms
Completed successfully!

Christopher Hoskin (Jun 08 2025 at 20:08):

Ah, sorry. We use main rather than master at work.... On the correct branch now.


Last updated: Dec 20 2025 at 21:32 UTC