More excessive memory errors

Stream: general

[Bolton Bailey]

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]

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]

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]

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

[Bolton Bailey]

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]

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

[Kevin Buzzard]

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]

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

[Bolton Bailey]

Oh you answered that nvm

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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