Zulip Chat Archive

Stream: general

Topic: More excessive memory errors

Bolton Bailey (Jul 10 2021 at 21:47):

After adding some lemmas to #8002 outside the bertrand.lean file, I am once again experiencing error messages of the following form

invalid import: data.option.defs
excessive memory consumption detected at 'whnf' (potential solution: increase memory consumption threshold)

This time, though, the usual tricks aren't working to fix it. I've restarted the Lean Server and VSCode itself. I've also tried `leanproject get-mathlib-cache and I get

(base) 17:36:46 mathlib #=# leanproject get-mathlib-cache
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/4b915b68f6f49d8eb078175cf4cc2b6b6501c28f.tar.xz to /Users/boltonbailey/.mathlib/4b915b68f6f49d8eb078175cf4cc2b6b6501c28f.tar.xz
Failed to fetch mathlib oleans

Any ideas on how to get Lean working again?

Kevin Buzzard (Jul 10 2021 at 21:49):

You have an uncompiled mathlib. You can fix it by compiling mathlib yourself or by getting CI to compile it for you. If you edit a file in mathlib then someone has to compile it again.

Bryan Gin-ge Chen (Jul 10 2021 at 21:50):

leanproject get mathlib-cache won't work until the build for that commit finishes; you can check the progress here. Based on the current queue it might be a few hours before it finishes.

Kevin Buzzard (Jul 10 2021 at 21:52):

You could try leanproject get-m --rev=HEAD~1

Bolton Bailey (Jul 10 2021 at 22:00):

leanproject get-m --rev=HEAD~1 also says failed to fetch mathlib oleans. Is this some wizardry that goes back through the branch to find a commit with an olean cache?

Bolton Bailey (Jul 10 2021 at 22:00):

leanproject get-m --rev=HEAD~2 is working

Kevin Buzzard (Jul 10 2021 at 22:09):

Yes that's right. If you're happy with the command line then you can git log to see the most recent commits on your branch, and leanproject get-mathlib-cache will only work for a commit which has been pushed to github and which CI has compiled. The --rev trick says "try the last but n commit" but of course the problem with this is that all files which you edited since that commit, and all the files they depend on, will still need to be compiled at your end. You can just compile manually with lean --make src and if you have some kind of feeling for the import hierarchy you'll be able to see how long it might take to finish. Compiling from scratch can take a couple of hours on a modest machine if you've edited a file high up in the hierarchy.

Bolton Bailey (Jul 10 2021 at 22:12):

Unfortunately, I still get the excessive memory with HEAD~2. How do I compile from scratch?

Bolton Bailey (Jul 10 2021 at 22:13):

Oh you answered that nvm

Kevin Buzzard (Jul 10 2021 at 22:13):

if you want to get CI to do it then push and wait. If you want to do it yourself then lean --make src and wait

Bolton Bailey (Jul 10 2021 at 22:13):

Cool, I'll start compiling, thanks for your help.

Kevin Buzzard (Jul 10 2021 at 22:14):

In the old days we had to do this ourselves all the time! However, in the old days mathlib was a lot smaller :-)

Last updated: Dec 20 2023 at 11:08 UTC