Too long to compile

Stream: general

[Ashvni Narayanan]

I just switched to a new branch, and the file I have opened isn't compiling. When I run leanproject get-cache, I get the following message:

 $leanproject get-cache
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/fff73c8b9cb802c27088e239f56f340e4021bb46.tar.xz to C:\Users\ashvn\.mathlib\fff73c8b9cb802c27088e239f56f340e4021bb46.tar.xz
Trying to download https://oleanstorage.azureedge.net/mathlib/fff73c8b9cb802c27088e239f56f340e4021bb46.tar.gz to C:\Users\ashvn\.mathlib\fff73c8b9cb802c27088e239f56f340e4021bb46.tar.gz
Trying to download https://oleanstorage.azureedge.net/mathlib/fff73c8b9cb802c27088e239f56f340e4021bb46.tar.bz2 to C:\Users\ashvn\.mathlib\fff73c8b9cb802c27088e239f56f340e4021bb46.tar.bz2
Looking for GitHub mathlib oleans
Info: No github section found in 'git config', we will use GitHub with no authentication
403 {"message": "API rate limit exceeded for 31.52.252.91. (But here's the good news: Authenticated requests get a higher rate limit. Check out the documentation for more details.)", "documentation_url": "https://docs.github.com/rest/overview/resources-in-the-rest-api#rate-limiting"}

Any help is appreciated, thank you!

[Patrick Massot]

Do you have any reason to believe that our olean cache in the cloud has oleans for this branch?

[Eric Wieser]

That looks like an old version of mathlib tools?

[Patrick Massot]

Yes, I think we no longer try the GitHub API anyway.

[Alena Gusakov]

I found that doing

git checkout master
git pull origin master
leanproject get-cache
git checkout my-branch
git pull origin master

seems to make it work (sorry I realize this is a few days late)

[Yakov Pechersky]

What's the last git pull origin master for? Also this should work on the latest release of mathlibtools:

leanproject get-c --rev master

so you don't have to checkout and pull master, etc