Zulip Chat Archive
Stream: general
Topic: The cache doesn't work
Yaël Dillies (Dec 22 2023 at 13:11):
The cache for mathlib is currently not working. I thought this was an error that was recently fixed, but the cache on master doesn't work right now (on Ubuntu).
Sébastien Gouëzel (Dec 22 2023 at 13:18):
Did you try lake exe cache get!?
Yaël Dillies (Dec 22 2023 at 13:19):
Ah no! Let me try
Yaël Dillies (Dec 22 2023 at 13:24):
I confirm: it does not work with lake exe cache get!
Mario Carneiro (Dec 22 2023 at 13:27):
what is the first file that is recompiled?
Mario Carneiro (Dec 22 2023 at 13:27):
and assuming it is ProofWidgets.Compat, what is the result of lake exe cache lookup ProofWidgets.Compat
Yaël Dillies (Dec 22 2023 at 13:27):
It's too fast for me to read, but it's [1/...] so I assume everything gets recompiled.
Mario Carneiro (Dec 22 2023 at 13:28):
oh that's new
Mario Carneiro (Dec 22 2023 at 13:28):
just pipe it to a log
Yaël Dillies (Dec 22 2023 at 13:28):
I am trying to nuke lake-packages just to see whether it's not my install being botched.
Mario Carneiro (Dec 22 2023 at 13:29):
hold on a bit, I want to diagnose the issue for others
Yaël Dillies (Dec 22 2023 at 13:29):
Mario Carneiro said:
just pipe it to a log
How does one do that? :sweat_smile:
Mario Carneiro (Dec 22 2023 at 13:29):
lake exe cache get does what
Yaël Dillies (Dec 22 2023 at 13:29):
Don't worry, the issue is still here after nuking
Mario Carneiro (Dec 22 2023 at 13:29):
OS?
Yaël Dillies (Dec 22 2023 at 13:29):
Gitpod, so Ubuntu
Mario Carneiro (Dec 22 2023 at 13:30):
and what is the master commit
Yaël Dillies (Dec 22 2023 at 13:31):
The latest: https://github.com/leanprover-community/mathlib4/commit/98067b25fcb5c00c13b4ac74ab781e2ef6689812
Yaël Dillies (Dec 22 2023 at 13:31):
$ lake exe cache get
Attempting to download 264 file(s)
Downloaded: 264 file(s) [attempted 264/264 = 100%] (100% success)
Decompressing 4050 file(s)
unpacked in 6518 ms
Mario Carneiro (Dec 22 2023 at 13:31):
and then lake build | head -20
Mario Carneiro (Dec 22 2023 at 13:32):
you don't need to let it finish, I just want to see what it starts with
Yaël Dillies (Dec 22 2023 at 13:34):
lake build | head -20 finishes instantly
Mario Carneiro (Dec 22 2023 at 13:34):
what does it print
Yaël Dillies (Dec 22 2023 at 13:34):
Nothing
Mario Carneiro (Dec 22 2023 at 13:34):
nothing?
Mario Carneiro (Dec 22 2023 at 13:34):
in that case it worked...?
Mario Carneiro (Dec 22 2023 at 13:34):
try lake build
Yaël Dillies (Dec 22 2023 at 13:34):
I wonder whether it's not the server that somehow didn't restart between switching branches
Yaël Dillies (Dec 22 2023 at 13:35):
Ahah, I restarted the server and now I get a new error:
failed to read file './.lake/build/lib/Mathlib/Lean/Exception.olean', invalid header
Mario Carneiro (Dec 22 2023 at 13:36):
either the server or the console is using the wrong version
Mario Carneiro (Dec 22 2023 at 13:36):
maybe try restarting again?
Mario Carneiro (Dec 22 2023 at 13:38):
Can you run #eval Lean.versionString in the server in a file with no imports?
Mario Carneiro (Dec 22 2023 at 13:38):
and lean --version on the console
Yaël Dillies (Dec 22 2023 at 13:40):
#eval Lean.versionString -- "4.5.0-rc1"
gitpod /workspace/mathlib4 (master) $ lean --version
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)
Mario Carneiro (Dec 22 2023 at 13:41):
and lake exe cache lookup Mathlib/Lean/Exception.lean
Yaël Dillies (Dec 22 2023 at 13:41):
Mathlib/Lean/Exception.lean: /home/gitpod/.cache/mathlib/ed8fc46412d2d359.ltar
comment: git=mathlib4@3fc009bb61c66914059e00af4c7c3ab08badfa78
Mario Carneiro (Dec 22 2023 at 13:42):
do you have xxd?
Mario Carneiro (Dec 22 2023 at 13:43):
unfortunately it doesn't print the actual lean commit but we can squint at the result of xxd .lake/build/lib/Mathlib/Lean/Exception.olean | head -5
Yaël Dillies (Dec 22 2023 at 13:43):
No idea. I used the standard gitpod configuration from the mathlib4 repo.
Mario Carneiro (Dec 22 2023 at 13:44):
well I already know the answer, that olean was in fact compiled on 4.5.0-rc1
Mario Carneiro (Dec 22 2023 at 13:45):
but import Mathlib.Lean.Exception still fails?
Yaël Dillies (Dec 22 2023 at 13:46):
Indeed, with the same error as previously
Mario Carneiro (Dec 22 2023 at 13:46):
very strange
Mario Carneiro (Dec 22 2023 at 13:46):
#eval Lean.githash?
Mario Carneiro (Dec 22 2023 at 13:47):
for the record this is what the xxd invocation looks like for me, and I'm expecting it to be the same for you
$ xxd .lake/build/lib/Mathlib/Lean/Exception.olean | head -5
00000000: 6f6c 6561 6e01 6236 3134 6666 3164 3132 olean.b614ff1d12
00000010: 6263 3338 6633 3930 3737 6639 6365 3966 bc38f39077f9ce9f
00000020: 3264 3438 6234 3263 3030 3361 6430 0000 2d48b42c003ad0..
00000030: 0000 7880 c74a 0000 18c8 7880 c74a 0000 ..x..J....x..J..
00000040: 0000 0000 0100 00f9 0500 0000 0000 0000 ................
Yaël Dillies (Dec 22 2023 at 13:47):
b614ff1d12bc38f39077f9ce9f2d48b42c003ad0
Mario Carneiro (Dec 22 2023 at 13:47):
and you can see that exact number written in the file I just posted
Mario Carneiro (Dec 22 2023 at 13:48):
what about lake env lean Test.lean where Test.lean has any mathlib imports
Yaël Dillies (Dec 22 2023 at 13:51):
No output for Test.lean containing
import Mathlib.Order.Basic
Yaël Dillies (Dec 22 2023 at 13:51):
The import works though. Let me try again with a later file.
Yaël Dillies (Dec 22 2023 at 13:52):
With
import Mathlib.RingTheory.Artinian
I get
gitpod /workspace/mathlib4 (master) $ lake env lean Test.lean
Test.lean:1:0: error: failed to read file './.lake/build/lib/Mathlib/Lean/Exception.olean', invalid header
Mario Carneiro (Dec 22 2023 at 13:53):
Oh so only some of the files are rejected?
Mario Carneiro (Dec 22 2023 at 13:53):
if you import Mathlib.Lean.Exception does it work
Yaël Dillies (Dec 22 2023 at 13:54):
gitpod /workspace/mathlib4 (master) $ lake env lean Test.lean
Test.lean:1:0: error: failed to read file './.lake/build/lib/Mathlib/Lean/Exception.olean', invalid header
again
Mario Carneiro (Dec 22 2023 at 13:54):
you should try the xxd invocation after all
Mario Carneiro (Dec 22 2023 at 13:54):
you may need to install it if you don't already have it
Yaël Dillies (Dec 22 2023 at 13:56):
:sweat:
gitpod /workspace/mathlib4 (master) $ sudo apt install xxd
Reading package lists... Done
Building dependency tree... Done
Reading state information... Done
The following NEW packages will be installed:
xxd
0 upgraded, 1 newly installed, 0 to remove and 0 not upgraded.
Need to get 54.2 kB of archives.
After this operation, 285 kB of additional disk space will be used.
Ign:1 http://archive.ubuntu.com/ubuntu jammy-updates/main amd64 xxd amd64 2:8.2.3995-1ubuntu2.12
Err:1 http://security.ubuntu.com/ubuntu jammy-updates/main amd64 xxd amd64 2:8.2.3995-1ubuntu2.12
404 Not Found [IP: 91.189.91.83 80]
E: Failed to fetch http://security.ubuntu.com/ubuntu/pool/main/v/vim/xxd_8.2.3995-1ubuntu2.12_amd64.deb 404 Not Found [IP: 91.189.91.83 80]
E: Unable to fetch some archives, maybe run apt-get update or try with --fix-missing?
Mario Carneiro (Dec 22 2023 at 13:56):
what about strings, does this command exist?
Mario Carneiro (Dec 22 2023 at 13:57):
We can kind of use it for the same purpose:
$ strings .lake/build/lib/Mathlib/Lean/Exception.olean | head -5
olean
b614ff1d12bc38f39077f9ce9f2d48b42c003ad0
Init
Lean
successIfFail
Yaël Dillies (Dec 22 2023 at 13:57):
Nope, don't have strings
Kevin Buzzard (Dec 22 2023 at 13:57):
just open the file in a text editor :-)
Mario Carneiro (Dec 22 2023 at 13:57):
okay maybe just open the olean file in vscode
Yaël Dillies (Dec 22 2023 at 14:00):
Where do I find it? I used to know, but things have moved recently.
Mario Carneiro (Dec 22 2023 at 14:00):
I posted the path above
Yaël Dillies (Dec 22 2023 at 14:02):
Mario Carneiro (Dec 22 2023 at 14:03):
you should be able to just paste the path directly into the Ctrl-P menu
Mario Carneiro (Dec 22 2023 at 14:05):
vscode hides it because it's gitignored and a binary file
Yaël Dillies (Dec 22 2023 at 14:05):
oleanb0fe9d6cdca82723134d61f8fe23a8c674f308b7
Yaël Dillies (Dec 22 2023 at 14:05):
is what my clipboard is willing to copy-paste
Mario Carneiro (Dec 22 2023 at 14:06):
okay, that is definitely not the right hash
Mario Carneiro (Dec 22 2023 at 14:06):
that is v4.4.0
Mario Carneiro (Dec 22 2023 at 14:07):
wait, but lake exe cache lookup said it was fine? Try lake exe cache unpack! and see if the number in the olean file changes
Yaël Dillies (Dec 22 2023 at 14:09):
It did!
Joachim Breitner (Dec 22 2023 at 14:09):
Yaël Dillies said:
:sweat:
gitpod /workspace/mathlib4 (master) $ sudo apt install xxd … E: Unable to fetch some archives, maybe run apt-get update or try with --fix-missing?
Usually running apt-get update first (which fetches the package indices) helps indeed.
Mario Carneiro (Dec 22 2023 at 14:09):
What I think happened is that the olean file was old but the olean.hash and .trace files were updated, so both lake and cache think the file is up to date
Yaël Dillies (Dec 22 2023 at 14:10):
Yes, but that got stuck because of missing permissions (which I assume I could have sorted out too)
Mario Carneiro (Dec 22 2023 at 14:10):
I have no idea how that could have happened
Yaël Dillies (Dec 22 2023 at 14:10):
Hash collision?
Mario Carneiro (Dec 22 2023 at 14:11):
unlikely, the hashes are pretty large
Mario Carneiro (Dec 22 2023 at 14:11):
it might have been an interrupted lake or cache process which only wrote some of the files
Yaël Dillies (Dec 22 2023 at 14:12):
It's possible. I was switching branches 2-3 times per minute when that happened
Mario Carneiro (Dec 22 2023 at 14:13):
side note, nuking .lake would have solved this problem
Mario Carneiro (Dec 22 2023 at 14:13):
but at least it was a learning experience :smile:
Yaël Dillies (Dec 22 2023 at 14:13):
Mario Carneiro said:
side note, nuking
.lakewould have solved this problem
But... I did that?
Mario Carneiro (Dec 22 2023 at 14:14):
maybe it got messed up after you did it?
Yaël Dillies (Dec 22 2023 at 14:14):
Well, the first time I nuked the old lake-packages. The second time, I'm pretty sure I nuked .lake/build
Joachim Breitner (Dec 22 2023 at 14:15):
Is there a lock-like protocol for writing these files atomically needed so that concurrent lake build and cache don't step on their toes? Or was that not the problem here?
(If it’s just one file you can do an atomic rename, but with three it’s a bit harder; probably delete one main one, write the others, atomically write the last one.)
Yaël Dillies (Dec 22 2023 at 14:15):
It was definitely messed up before I did it, so if you're covered it must have been messed up twice.
Mario Carneiro (Dec 22 2023 at 14:15):
Yeah I was also thinking about that, possibly you had a v4.4.0 lake process running in the background and started by the old server while you were doing your thing
Mario Carneiro (Dec 22 2023 at 14:16):
and so you ended up with a mixture of files from different versions
Yaël Dillies (Dec 22 2023 at 14:16):
Good point. I restarted the server after nuking .lake
Eric Wieser (Dec 22 2023 at 17:03):
Yaël Dillies said:
:sweat:
gitpod /workspace/mathlib4 (master) $ sudo apt install xxd Reading package lists... Done Building dependency tree... Done Reading state information... Done The following NEW packages will be installed: xxd 0 upgraded, 1 newly installed, 0 to remove and 0 not upgraded. Need to get 54.2 kB of archives. After this operation, 285 kB of additional disk space will be used. Ign:1 http://archive.ubuntu.com/ubuntu jammy-updates/main amd64 xxd amd64 2:8.2.3995-1ubuntu2.12 Err:1 http://security.ubuntu.com/ubuntu jammy-updates/main amd64 xxd amd64 2:8.2.3995-1ubuntu2.12 404 Not Found [IP: 91.189.91.83 80] E: Failed to fetch http://security.ubuntu.com/ubuntu/pool/main/v/vim/xxd_8.2.3995-1ubuntu2.12_amd64.deb 404 Not Found [IP: 91.189.91.83 80] E: Unable to fetch some archives, maybe run apt-get update or try with --fix-missing?
You have to run apt-get update first like it says
Yury G. Kudryashov (Dec 24 2023 at 21:43):
Another issue with cache: when download fails with error like "Recv failure: Connection reset by peer", lake exe cache get doesn't unpack the files it downloaded.
Yaël Dillies (Dec 26 2023 at 13:48):
This happened again, fyi. Same scenario: I switched between branches on different Lean versions, got cache and restarted Lean on a file before restarting the server.
Yaël Dillies (Jan 01 2024 at 16:59):
New problem: lake exe cache get doesn't download anything
Christopher Hoskin (Jan 01 2024 at 18:35):
I've been having this problem all afternoon - even on a clean checkout of master nothing downloads from the cache:
pushd /tmp
/tmp ~/Documents/lean4/mathlib4
git clone git@github.com:leanprover-community/mathlib4.git
Cloning into 'mathlib4'...
remote: Enumerating objects: 250876, done.
remote: Counting objects: 100% (2897/2897), done.
remote: Compressing objects: 100% (1151/1151), done.
remote: Total 250876 (delta 2185), reused 2288 (delta 1733), pack-reused 247979
Receiving objects: 100% (250876/250876), 121.35 MiB | 2.29 MiB/s, done.
Resolving deltas: 100% (198314/198314), done.
cd mathlib4/
lake exe cache get
info: std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
info: Qq: cloning https://github.com/leanprover-community/quote4 to './.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to './.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to './.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to './.lake/packages/Cli'
info: [0/9] Downloading proofwidgets cloud release
info: [0/9] Unpacking proofwidgets cloud release
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: [6/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 1800 file(s)
Downloaded: 0 file(s) [attempted 1800/1800 = 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 2276 file(s)
unpacked in 6085 ms
Chris Birkbeck (Jan 01 2024 at 19:13):
Yep that's the same problem I'm having
Yaël Dillies (Jan 01 2024 at 19:14):
This seems very high priority to me. I can't do any mathlib work right now (well, I can, but that's because I have a Lean compiler in my head) and I suppose no one else can.
Mauricio Collares (Jan 01 2024 at 19:19):
$ lake build
[791/1883] Building Mathlib.Algebra.GroupPower.Order
Mauricio Collares (Jan 01 2024 at 19:22):
Never mind, previous commits have missing files too, let me bisect it
Mauricio Collares (Jan 01 2024 at 19:28):
Bisects to 0d6117a47dd8f9fe074025146a29b195bf0230f1, but there's nothing suspicious in the corresponding staging run log. https://lakecache.blob.core.windows.net/mathlib4/f/b828f223bf7b5621.ltar is just missing, I guess someone with Azure access will need to debug this:
$ lake exe cache lookup Mathlib/Algebra/BigOperators/Order.lean
Mathlib/Algebra/BigOperators/Order.lean: /home/collares/.cache/mathlib/b828f223bf7b5621.ltar
uncaught exception: /home/collares/.cache/mathlib/b828f223bf7b5621.ltar not found
Eric Rodriguez (Jan 02 2024 at 00:11):
this still seems to be the case, btw
Mario Carneiro (Jan 02 2024 at 00:21):
I'm investigating, but I agree that this needs someone to check up with azure, I think it's dropping files for some reason
Mario Carneiro (Jan 02 2024 at 00:25):
And to make matters worse, I think no one in the admin team knows the keys either (@Rob Lewis?)
Mario Carneiro (Jan 02 2024 at 00:26):
The azure keys expire after a year, so I think it might have something to do with the new year...
Mario Carneiro (Jan 02 2024 at 00:56):
Confirmed that the issue is that our azure account has expired. For now, the cache is read only which means all our uploads are failing. I don't think there is a quick fix, we may or may not need to switch providers.
Newell Jensen (Jan 02 2024 at 01:00):
What does the azure account host for those not in the know?
Mario Carneiro (Jan 02 2024 at 01:02):
The thing that lake exe cache get downloads
Mario Carneiro (Jan 02 2024 at 01:03):
blob storage for all the build artifacts of mathlib
Mario Carneiro (Jan 02 2024 at 01:04):
For the time being, I think this means we'll have to do things the old fashioned way and just compile mathlib locally
Newell Jensen (Jan 02 2024 at 01:05):
Mario Carneiro said:
blob storage for all the build artifacts of mathlib
Nothing else? Even so, this breaks everything else that relies on this, which is probably most things like CI etc. right?
Mario Carneiro (Jan 02 2024 at 01:06):
Note that you can still use lake exe cache pack and lake exe cache unpack to sync cache files on your local machine
Mario Carneiro (Jan 02 2024 at 01:06):
CI isn't broken per se, it just has to compile all of mathlib every time now
Mario Carneiro (Jan 02 2024 at 01:06):
or at least the part that hasn't been invalidated yet
Eric Wieser (Jan 02 2024 at 01:54):
Mario Carneiro said:
For the time being, I think this means we'll have to do things the old fashioned way and just compile mathlib locally
As long as the cache can still be read, a short term workaround is to start all new branches against mathlib from last year.
Mario Carneiro (Jan 02 2024 at 01:56):
maybe we should make a tag for that
Yury G. Kudryashov (Jan 02 2024 at 04:50):
What's the last revision with cache?
Mario Carneiro (Jan 02 2024 at 05:11):
https://github.com/leanprover-community/mathlib4/commit/0c9d4118caa615ee8c9592a1da2e3fd79d682cf8
Mario Carneiro (Jan 02 2024 at 05:13):
added as v2024
Eric Wieser (Jan 02 2024 at 10:13):
I get a 403 error if I run lake exe cache get on that commit; maybe this is an unrelated transient issue
Mario Carneiro (Jan 02 2024 at 10:38):
happening to me as well, I don't think that was happening before
Antoine Chambert-Loir (Jan 02 2024 at 10:40):
github also has the 403 error…
Mario Carneiro (Jan 02 2024 at 10:52):
according to logs there hasn't been any azure traffic for the past 30 minutes but it could be a server issue
Jeremy Tan (Jan 02 2024 at 13:46):
What is going on???
Arthur Paulino (Jan 02 2024 at 13:48):
@Gabriel Ebner was the one who helped me with Azure access and keys ~1 year ago so I'm pinging him. Maybe he has some insight
Mario Carneiro (Jan 02 2024 at 13:50):
I double checked azure and I think this 403 thing is permanent, the account is now "disabled" (not "read only") and we're going to have to figure out how to renew or something to get access back
Jeremy Tan (Jan 02 2024 at 13:51):
Who owns the Azure account?
Mario Carneiro (Jan 02 2024 at 13:51):
leanprover-community org
Mario Carneiro (Jan 02 2024 at 13:52):
it was an MS sponsorship (donation)
Jeremy Tan (Jan 02 2024 at 14:39):
I think you should make an announcement thread about this, operating like GitHub status
Eric Rodriguez (Jan 02 2024 at 14:54):
Are the ltars available as a github artifact? For now I think we could make one copy of a reasonably recent one available with some instructions on how to install them
Junyan Xu (Jan 02 2024 at 16:13):
Now all builds are failing at the "get cache" step.
Jeremy Tan (Jan 02 2024 at 23:11):
Junyan Xu said:
Now all builds are failing at the "get cache" step.
That was true as of ~3 hours before you made that post
Rob Lewis (Jan 03 2024 at 02:04):
FYI, we are working on getting this fixed. Stay tuned, hopefully things will be back online tomorrow :fingers_crossed:
Yaël Dillies (Jan 03 2024 at 07:43):
Just mentioning that #9391 should be put back on the queue once CI is fixed.
Michael Stoll (Jan 03 2024 at 10:15):
For easy reference: what is the lake command to build (the olean files of) everything up to a specific file in Mathlib (when working on Mathlib)? I find the output of lake --help build somewhat confusing...
Sebastian Ullrich (Jan 03 2024 at 10:27):
lake build Mathlib.Your.Module. Or open the file in your editor.
Kevin Buzzard (Jan 03 2024 at 11:46):
Does opening the file in your editor now create oleans on your hard drive? (it didn't used to IIRC)
Sebastian Ullrich (Jan 03 2024 at 11:53):
Starting with Lean 4, yes
Sebastian Ullrich (Jan 03 2024 at 11:54):
after the confirmation
Dan Dougherty (Jan 03 2024 at 15:13):
I'm having the same (?) problem...since yesterday. I'm on MacOS. Have had no previous problems with this. When I run lake exe cache get, OR lake update within a project I get 403 errors.
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)
Lake version 5.0.0-b614ff1 (Lean version 4.5.0-rc1)
Yaël Dillies (Jan 03 2024 at 15:13):
We are aware :smile: This will hopefully be resolved today or tomorrow.
Eric Rodriguez (Jan 03 2024 at 15:14):
If there's no resolution by today, I prepared a small work-around too.
Mario Carneiro (Jan 03 2024 at 16:02):
Thanks to the work of @Sebastian Ullrich in #9409 and the pocketbook of the Lean FRO, the mathlib cache has moved from Azure to Cloudflare R2. Old commits will still not work however, and we are still looking into how to re-enable the Azure endpoint so that we don't break all the old caches. You should either update mathlib master, or rebase your mathlib branch onto master to be able to make use of the new cache.
Rob Lewis (Jan 03 2024 at 16:06):
The timeline for old commits returning may be very short -- AFAIK we're just waiting for an Azure support rep to click a button.
Sebastian Ullrich (Jan 03 2024 at 17:11):
Old commits indeed should now work as well again, except for the ones in the last few days not uploaded while the cache was down
Josha Dekker (Jan 03 2024 at 17:40):
What to do with these commits?
Mauricio Collares (Jan 03 2024 at 17:49):
Don't use them :) Current master is fine, so projects depending on mathlib can just run lake update and mathlib branches created in the last couple of days can be rebased (just merging master is also fine).
Josha Dekker (Jan 03 2024 at 18:05):
My PR #9200 was accepted yesterday, but building failed because of the cache issue. Should I make a new commit to this that changes nothing to restart the building process, or will this be dealt with automatically?
Eric Rodriguez (Jan 03 2024 at 18:06):
you'll have to merge master on your PR
Josha Dekker (Jan 03 2024 at 18:08):
okay, will do!
Christopher Hoskin (Jan 03 2024 at 18:13):
Thanks for the work on this. Things are looking better, but I'm still not getting 100% success on the latest HEAD of master:
lake exe cache get
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [4/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 4077 file(s)
Downloaded: 3889 file(s) [attempted 4077/4077 = 100%] (95% 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 3889 file(s)
unpacked in 3101 ms
Is there something else I need to do? I tried:
lake exe cache get!
Attempting to download 4077 file(s)
Downloaded: 3889 file(s) [attempted 4077/4077 = 100%] (95% 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 3889 file(s)
unpacked in 3352 ms
git status
On branch master
Your branch is up to date with 'origin/master'.
nothing to commit, working tree clean
Ruben Van de Velde (Jan 03 2024 at 18:14):
What's the first commit on git log?
Kevin Buzzard (Jan 03 2024 at 18:18):
I just pulled; I'm on e23b08714daf24b36bff71d3387f034cd19c1a38 and I'm seeing the same behaviour:
...
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 3678 file(s)
Downloaded: 3490 file(s) [attempted 3678/3678 = 100%] (94% 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 3889 file(s)
unpacked in 40983 ms
buzzard@ebony:~/lean-projects/mathlib4$ lake build
[3254/4075] Building Mathlib.Analysis.Calculus.FormalMultilinearSeries
[3440/4075] Building Mathlib.RingTheory.AlgebraicIndependent
[3891/4075] Building Mathlib.Analysis.Calculus.ContDiff.Defs
[3891/4075] Building Mathlib.Analysis.Analytic.Basic
[3892/4075] Building Mathlib.FieldTheory.IsAlgClosed.Classification
^C
buzzard@ebony:~/lean-projects/mathlib4$
Mario Carneiro (Jan 03 2024 at 18:19):
I'm preparing a cache reset which should hopefully fix these issues
Mario Carneiro (Jan 03 2024 at 18:20):
I think there are some bad files that were accidentally uploaded during the initial test
Jeremy Tan (Jan 03 2024 at 19:20):
What's the "Lean FRO"?
Kevin Buzzard (Jan 03 2024 at 19:23):
google it :-)
Jeremy Tan (Jan 03 2024 at 19:25):
oh
Bolton Bailey (Jan 03 2024 at 22:26):
"Lean Focused Research Organization" Here is a link https://lean-fro.org/
Eric Wieser (Jan 03 2024 at 22:43):
In #9401, I can't seem to get a cache for the resulting build
Eric Wieser (Jan 03 2024 at 22:44):
(it finds no matching files to download)
Mario Carneiro (Jan 03 2024 at 22:49):
Yeah something still seems to be a bit off with the cache, uploads don't seem to stick or something. Sebastian wrote #9414 to try to improve the "check the cache" step (which is supposed to catch this issue) but I think it might be the end of the day, it's been a long day
Jeremy Tan (Jan 04 2024 at 04:01):
@Mario Carneiro how did you get the Azure cache back?
Mario Carneiro (Jan 04 2024 at 04:01):
We paid up
Jeremy Tan (Jan 04 2024 at 04:03):
Then when you move to Cloudflare for good you're going to cancel the Azure subscription? (And are you close to working out the Cloudflare kinks?)
Mario Carneiro (Jan 04 2024 at 04:18):
Probably not, the Azure links are holding up all our old commits and these show up in various mathlib references on the internet, but the cost should decrease to something negligible if daily activity moves off of it
Mario Carneiro (Jan 04 2024 at 05:09):
I just pushed a partial revert of #9409, so master uses Azure once more, which should fix the intermittent cache failures. We plan to return to Cloudflare once we figure out how to make it not reject some uploads with 400s
Jeremy Tan (Jan 04 2024 at 08:40):
Why is this failing?
https://github.com/leanprover-community/mathlib4/actions/runs/7407203971/job/20153052765
Jeremy Tan (Jan 04 2024 at 08:50):
There's no 403 but there's an uncaught exception; I see the same thing in #9428
Chris Wong (Jan 04 2024 at 09:48):
Jeremy Tan said:
Why is this failing?
https://github.com/leanprover-community/mathlib4/actions/runs/7407203971/job/20153052765
I got the same error as you (locally, macOS Sonoma, curl 8.1.2).
I think it's caused by this change:
https://github.com/leanprover-community/mathlib4/commit/7c0310106360d5bede3c6ce86ef6d369e5efb6f0#r136197383
The error only happens when leantar is out of date, because that's when the script calls curl to install it. That might be why @Mario Carneiro didn't see the problem.
Chris Wong (Jan 04 2024 at 10:03):
#9434 should fix this – someone PTAL :)
Sebastian Ullrich (Jan 04 2024 at 10:17):
It's queued, thanks for the swift help!
Mario Carneiro (Jan 04 2024 at 16:30):
Ah no, the solution is to pass the -s flag there as in the other curl calls
Mario Carneiro (Jan 04 2024 at 16:32):
although it sounds like -sS would be better
Mario Carneiro (Jan 04 2024 at 16:33):
the trouble is that curl is not indicating failures via the exit code like it should in the multi-file situation
Yaël Dillies (Jan 07 2024 at 20:44):
I don't know if anybody else noticed, but all the caches I get before The Great Cache Incident are invalid, making them virtually useless.
Yaël Dillies (Jan 07 2024 at 20:45):
This is mostly a non-problem, but @Terence Tao just mentioned needing them to work on PFR (since my bump to post-Great Cache Incident mathlib is currently stuck).
Mario Carneiro (Jan 07 2024 at 20:49):
Can you elaborate?
Mario Carneiro (Jan 07 2024 at 20:49):
the cache files are present but don't work?
Mario Carneiro (Jan 07 2024 at 20:50):
Some cache files (for commits during the incident) were lost but old cache files should still work
Yaël Dillies (Jan 07 2024 at 20:50):
We're talking about ea70e843f6449df0777fbfebe222d09a083bd844, well before the incident.
Yaël Dillies (Jan 07 2024 at 20:51):
Mario Carneiro said:
the cache files are present but don't work?
Yes, exactly. lake exe cache get runs smoothly, but then I need to rebuild all the files past the first 200 or so.
Mauricio Collares (Jan 07 2024 at 20:52):
Weird, I am working on PFR right now and the cache is working. Maybe lake exe cache get! helps in case you got a poisoned local cache?
Terence Tao (Jan 07 2024 at 20:53):
I actually had this issue with the bump branch which has a more recent Mathlib version.
Yaël Dillies (Jan 07 2024 at 20:53):
I am now confusion.
Mario Carneiro (Jan 07 2024 at 20:53):
also the usual debugging procedure is to use lake exe cache lookup on the first file which is rebuilt
Terence Tao (Jan 07 2024 at 20:55):
This is what happens when I try to update cache from PFR master branch (which has the older version of Mathlib):
PS C:\Users\teort\Dropbox\Lean\pfr> lake exe cache get!
info: mathlib: updating repository '.\.lake/packages\mathlib' to revision 'ea70e843f6449df0777fbfebe222d09a083bd844'
error: > git checkout --detach ea70e843f6449df0777fbfebe222d09a083bd844 # in directory .\.lake/packages\mathlib
error: stderr:
error: Your local changes to the following files would be overwritten by checkout:
Mathlib/RingTheory/Finiteness.lean
Please commit your changes or stash them before you switch branches.
Aborting
error: external command `git` exited with c
Yaël Dillies (Jan 07 2024 at 20:57):
This looks like you touched a file you shouldn't have in your local copy of mathlib within PFR.
Terence Tao (Jan 07 2024 at 20:59):
It does show that file touched in the last hour or so; I don't remember actually messing with it but perhaps it happened by accident. But I can't seem to revert it back at all, git seems to think everything is just fine:
PS C:\Users\teort\Dropbox\Lean\pfr> git pull origin master -r
From https://github.com/teorth/pfr
* branch master -> FETCH_HEAD
Already up to date.
PS C:\Users\teort\Dropbox\Lean\pfr> git reset HEAD --hard
HEAD is now at 0725e2a Merge pull request #170 from llllvvuu/chore/fix_typo_single_fibres
PS C:\Users\teort\Dropbox\Lean\pfr> git stash
No local changes to save
PS C:\Users\teort\Dropbox\Lean\pfr> git pull origin master
From https://github.com/teorth/pfr
* branch master -> FETCH_HEAD
Already up to date.
Terence Tao (Jan 07 2024 at 21:01):
Worst case I just nuke my local folder and start over, so I guess as long as it works for everyone else it's fine
Mario Carneiro (Jan 07 2024 at 21:01):
you have to go into .lake/packages/mathlib and use git reset --hard HEAD because that's another repo
Mario Carneiro (Jan 07 2024 at 21:01):
or just delete .lake
Terence Tao (Jan 07 2024 at 21:10):
OK, it's still building some PFR files but I think I got back to a working copy of the master build (with a successful cache grab). I was in the wrong folder when I tried to grab the cache manually so that helps explain why I had to rebuild Mathlib the last few times.
Arthur Paulino (Jan 07 2024 at 22:26):
About missing files from old commits, in case they are really necessary:
- If it's on
main, someone with pushing rights could dolake exe cache putif they're present locally - If it's on a dangling branch from an unmerged PR, pushing a merging commit (to get the new updates/fixes from
main) to trigger CI should, in theory, force the upload of the rebuilt cache, filling the gaps of missing files
Richard Copley (Jan 18 2024 at 14:35):
Is the cache working now for everyone else, in a repo of mathlib itself? This is what I get:
git clone https://github.com/leanprover-community/mathlib4
cd mathlib4/
curl -L -O https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain
lake update
lake exe cache get
Attempting to download 4141 file(s)
Downloaded: 0 file(s) [attempted 4141/4141 = 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.
No cache files to decompress
Sébastien Gouëzel (Jan 18 2024 at 14:40):
The line lake update is wrong. If you do the same without this line, does it work fine?
Richard Copley (Jan 18 2024 at 14:43):
It does. Thanks!
Kim Morrison (Jan 19 2024 at 02:40):
@Richard Copley, if you were following a document that suggested using lake update, please tell us about it so we can hunt it down and exterminate it. But we already know that lake update is overly tempting, and would like to make it more obscure. :-)
Mario Carneiro (Jan 19 2024 at 02:42):
We could have a post-update hook which fails if you don't set the I_AM_A_MAINTAINER_AND_KNOW_WHAT_I_AM_DOING environment variable, but I think that post-update hooks run too late to prevent the change to the lake manifest
Richard Copley (Jan 19 2024 at 02:54):
Scott Morrison said:
Richard Copley, if you were following a document that suggested using
lake update, please tell us about it so we can hunt it down and exterminate it. But we already know thatlake updateis overly tempting, and would like to make it more obscure. :-)
I have the recipe above in a shell script. If I recall correctly those instructions were on Using Lake (build system), but that was days and days ago :smile:. The script seems to make sense and to work for my projects (assuming I want to update the dependencies to the commits specified in the toplevel lakefile.lean, which usually I do). I was applying it in the wrong situation, but until recently I seem to have got away with that for the most part.
Yaël Dillies (Apr 20 2024 at 15:41):
Is it just me or does the cache not work? I don't have a good repro, but it seems related to the recent update of the vscode extension
Yaël Dillies (Apr 20 2024 at 15:43):
Eg lake exe cache get gets cache for Algebra.AddConstMap, but you still have to rebuild files
Ruben Van de Velde (Apr 20 2024 at 16:07):
Haven't seen it, but also haven't updated the extension that I noticed
Kim Morrison (Apr 20 2024 at 23:10):
Working fine for me.
Yaël Dillies (Apr 23 2024 at 06:53):
It keeps on happening for me!
Yaël Dillies (Apr 23 2024 at 06:54):
Sadly I can't actually try from scratch because I can't delete the .lake folder on Gitpod anymore? :face_with_raised_eyebrow: Is this expected?
Kevin Buzzard (Apr 23 2024 at 07:58):
Is the problem that you accidentally made .lake read-only?
Yaël Dillies (Apr 23 2024 at 07:58):
How would I have done that?
Yaël Dillies (Apr 23 2024 at 07:59):
lake exe cache get! does seem to fix my non-working cache sometimes
Damiano Testa (Apr 23 2024 at 08:28):
I have had something similar, where after lake exe cache get, running lake build starts building somewhere low. I found that after rm -rf .lake/build/lib/Mathlib/*, I can then run lake exe cache get, it downloads nothing and then lake build just works...
Damiano Testa (Apr 23 2024 at 08:28):
Although, if you cannot remove stuff in .lake, this may not be too useful...
Kevin Buzzard (Apr 23 2024 at 10:03):
chmod a-w .lake or something?
Mario Carneiro (Apr 23 2024 at 15:22):
if you cannot add/remove stuff in .lake then neither can cache so this is very likely the problem
Last updated: May 02 2025 at 03:31 UTC