Zulip Chat Archive

Stream: general

Topic: Too long to compile


Ashvni Narayanan (Jan 19 2021 at 15:05):

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 (Jan 19 2021 at 15:07):

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

Eric Wieser (Jan 19 2021 at 15:08):

That looks like an old version of mathlib tools?

Patrick Massot (Jan 19 2021 at 15:09):

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

Alena Gusakov (Jan 27 2021 at 04:57):

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 (Jan 27 2021 at 05:07):

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


Last updated: Dec 20 2023 at 11:08 UTC