github authentication failed?

Stream: general

[Mario Carneiro]

I'm getting this on leanproject up:

Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/e25e569c426195e7c088721e682001a8469a47b6.tar.gz to /home/mario/.mathlib/e25e569c426195e7c088721e682001a8469a47b6.tar.gz
Looking for GitHub mathlib oleans
Info: No github 'user'/'password' or 'oauthtoken' keys found in git config, we will use GitHub with no authentication.
You can create an OAuth token at https://github.com/settings/tokens/new (no scopes are required).
Failed to fetch mathlib oleans

It worked fine yesterday. Is this just me or is github / azure service affected in some way?

[Yury G. Kudryashov]

What is your leanproject version?

[Yury G. Kudryashov]

It looks for tar.gz, it should look for tar.xz

[Mario Carneiro]

is there a command for that?

[Mario Carneiro]

that's probably the issue

[Patrick Massot]

leanproject --version should tell you your version (unless it's very old). But you can upgrade anyway, probably with pip install -U mathlibtools

[Yury G. Kudryashov]

And pip should know the versions of all installed python packages

[Scott Morrison]

I got an email recently from github warning me that I'd accessed the github api recently with a password, and that this was going to be deprecated soon. Perhaps you got hit by this?

[Mario Carneiro]

My leanproject was too old for --version indeed. I updated and github is working again

[Yury G. Kudryashov]

Azure is working. AFAIK, we don't use github storage anymore.

[Mario Carneiro]

hm, even my old version seemed to be of two minds about that:

Trying to download https://oleanstorage.azureedge.net/...
Looking for GitHub mathlib oleans

[Scott Morrison]

My understanding of this is that when it fails to find anything on azureedge.net, to doesn't say anything about that, but just falls back to looking on GitHub.

[Rob Lewis]

As of a few days ago, every archive should be available as a tar.xz on Azure. If that lookup fails nothing else will succeed. But obviously old versions of leanproject don't know that.

[Filippo A. E. Nuccio]

I have the same problem as Mario: after updating pip and then doing pip install -U mathlibtools, it still seems that the oleans are being searched on github (and I can't download them)

[Filippo A. E. Nuccio]

This is the message I get
Looking for local mathlib oleans Looking for remote mathlib oleans Trying to download https://oleanstorage.azureedge.net/mathlib/0d833b6dd48266af586db500fc37fac5c02a08de.tar.xzáto C:\Users\faenu\.mathlib\0d833b6dd48266af586db500fc37fac5c02a08de.tar.xz Trying to download https://oleanstorage.azureedge.net/mathlib/0d833b6dd48266af586db500fc37fac5c02a08de.tar.gzáto C:\Users\faenu\.mathlib\0d833b6dd48266af586db500fc37fac5c02a08de.tar.gz Trying to download https://oleanstorage.azureedge.net/mathlib/0d833b6dd48266af586db500fc37fac5c02a08de.tar.bz2áto C:\Users\faenu\.mathlib\0d833b6dd48266af586db500fc37fac5c02a08de.tar.bz2 Looking for GitHub mathlib oleans 403 {"message": "API rate limit exceeded for 78.241.31.206. (But here's the good news: Authenticated requests get a higher rate limit. Check out the documentation for more details.)", "documentation_url": "https://developer.github.com/v3/#rate-limiting"} Info: No github section found in 'git config', we will use GitHub with no authentication

[Filippo A. E. Nuccio]

And this happens every time I open VS Code after a week or so while I haven't been using it: it starts compiling the whole library, takes a couple of hours and can't update...

[Johan Commelin]

Oooh, that doesn't sound good

[Johan Commelin]

you're on a mac right?

[Filippo A. E. Nuccio]

Nope, Win

[Johan Commelin]

Aah, ok

[Johan Commelin]

Hmmm, I don't know anything about Win

[Johan Commelin]

@Mario Carneiro did you ever get this problem sorted out?

[Filippo A. E. Nuccio]

it seems to be related to by mathlib folder: I have just tried to open the lftcm2020 folder (which I hadn't opened for a month or so) and it compiles istantaneously

[Gabriel Ebner]

This just means that there are no precompiled oleans available on azure. We're currently phasing out the github api fetcher.

[Gabriel Ebner]

mathlib-tools#76

[Johan Commelin]

@Filippo A. E. Nuccio are you running leanproject up in mathlib? Or leanproject get-mathlib-cache?

[Filippo A. E. Nuccio]

yes, and I get the above error message

[Gabriel Ebner]

0d833b6dd48266af586db500fc37fac5c02a08de is not a revision in the mathlib repository.

[Filippo A. E. Nuccio]

@Gabriel Ebner Unfortunately I don't understand what you are saying (I don't know what "to phase" means)

[Filippo A. E. Nuccio]

What do you suggest that I do?

[Gabriel Ebner]

We are no longer going to use the github part.

[Gabriel Ebner]

Can you paste the output of git log -n2?

[Filippo A. E. Nuccio]

$ git log -n2
commit 0d833b6dd48266af586db500fc37fac5c02a08de (HEAD -> Vierkantor-dedekind-domain, origin/Vierkantor-dedekind-domain)
Merge: c5f7ea052 bffc04e65
Author: faenuccio <filippo.nuccio@univ-st-etienne.fr>
Date: Fri Aug 28 16:24:47 2020 +0000

Merge branch 'Vierkantor-dedekind-domain' of https://github.com/leanprover-community/mathlib into Vierkantor-dedekind-domain

commit bffc04e656101392d71ef56ec737a117eeb6090e
Author: Vierkantor <vierkantor@vierkantor.com>
Date: Thu Aug 27 07:48:44 2020 +0000

Trace in a simple field extension

[Bryan Gin-ge Chen]

There are no oleans for this commit in Azure or anywhere else, so you'll either have to build mathlib yourself or push to a branch in the mathlib repo and wait for the CI to build and then try leanproject get-cache again.

[Gabriel Ebner]

@Filippo A. E. Nuccio You should probably work on a branch in the mathlib repo.

[Filippo A. E. Nuccio]

It is in mathlib, I guess.

[Filippo A. E. Nuccio]

and I get the same issue if I try to work on the master branch

[Patrick Massot]

There is no magic going on here, you can get oleans only for things that got compiled on GitHub.

[Patrick Massot]

Is your master at a commit that is in the main repository?

[Patrick Massot]

Can you git checkout master and git log?

[Patrick Massot]

and tell us what the top commit hash

[Filippo A. E. Nuccio]

commit a08fb2f74e1767bd6338504c4ee29a0fe1866a48

[Patrick Massot]

And what if you now try leanproject get-cache?

[Filippo A. E. Nuccio]

ah, now it works.

[Patrick Massot]

And how did you expect it to work for a commit that is only on your computer?

[Patrick Massot]

GitHub is not allowed to spy on your computer to build things for you.

[Filippo A. E. Nuccio]

I did not expect it to work, I simply did not know I was on a local commit

[Filippo A. E. Nuccio]

But Vierkantor-dedekind-domain is a branch on mathlib, right?

[Patrick Massot]

This is probably lack on git understanding then (what is a merge commit, what happens when you git pull etc).

[Patrick Massot]

Yes, but this is not where you were.

[Patrick Massot]

You did a merge commit in between, look at the output you pasted.

[Filippo A. E. Nuccio]

Right

[Patrick Massot]

commit 0d833b6dd48266af586db500fc37fac5c02a08de (HEAD -> Vierkantor-dedekind-domain, origin/Vierkantor-dedekind-domain)
Merge: c5f7ea052 bffc04e65
Author: faenuccio <filippo.nuccio@univ-st-etienne.fr>
Date:   Fri Aug 28 16:24:47 2020 +0000

    Merge branch 'Vierkantor-dedekind-domain' of https://github.com/leanprover-community/mathlib into Vierkantor-dedekind-domain

[Patrick Massot]

That commit is only on your computer.

[Filippo A. E. Nuccio]

It is certainly a lack of understanding, but I had begun with a git pull, thinking this would have sync my local commit with the remote one. Is this wrong?

[Patrick Massot]

Yes, it's wrong.

[Patrick Massot]

Because you had local modifications, that needed to be combined with remote advances.

[Filippo A. E. Nuccio]

Ah, and the merge comes from there.

[Patrick Massot]

Yes.

[Patrick Massot]

How is your branch called?

[Filippo A. E. Nuccio]

Vierkantor dedekind-domain

[Patrick Massot]

I'll tell you what you should have done

[Filippo A. E. Nuccio]

thanks

[Patrick Massot]

Oh, you were working on a branch tracking Anne's branch?

[Filippo A. E. Nuccio]

yes

[Patrick Massot]

Ok

[Patrick Massot]

At the time when you typed git pull, you should have typed git pull --rebase. Then leanproject is not as helpful as it could be if I had more time. You would have need to have a look at the last commit from upstream, bffc04e6561013 in your case. git checkout bffc04e6561013, leanproject get-cache, git checkout dedekind-domain, leanproject build.

[Patrick Massot]

This would have given you oleans for bffc04e65 and hopefully the build wouldn't have been long (unless you modified files close to the roots).

[Filippo A. E. Nuccio]

Ok, I'll do this the next time. One last question: what's the difference between get-cache and get-mathlib-cache?

[Patrick Massot]

When editing mathlib there is no difference. When working on a project depending on mathlib, get-cache will get cache for the current project (that has to be local cache, created using mk-cache, not remote cache).

[Filippo A. E. Nuccio]

ah, so for me is the same. Ok, many thanks.