cache-olean and authentication

Stream: general

[Scott Morrison]

cache-olean is always telling me "Info: No github section found in 'git config', we will use GitHub with no authentication", and then infuriatingly that "API rate limit exceeded for 98.248.251.76. (But here's the good news: Authenticated requests get a higher rate limit. Check out the documentation for more details.)", and I'm condemned to recompiling a branch yet again.

[Scott Morrison]

Neither of those messages give me the least clue how to set up github authentication.

[Scott Morrison]

Can we fix this, so cache-olean itself points to some useful piece of instruction?

[Scott Morrison]

Perhaps as a first step to this, can someone tell me what I'm meant to do?

[Mario Carneiro]

fwiw I see the same message

[Scott Morrison]

What does one put in a "github section"?

[Alex J. Best]

In my .git/config file I have a line
[github] oauthtoken = BLAHBLAH

[Alex J. Best]

IIRC I did some sleuthing to end up with this, so this may not be the perfect thing but seemed to work. I set up a token on https://github.com/settings/tokens/

[Rob Lewis]

Note that this will be irrelevant once #2032 and the related scripts land.

[Patrick Massot]

Is there any reason to delay merging this PR?

[Patrick Massot]

There are things to discuss of course (how long we keep things), but it's not blocking, right?

[Rob Lewis]

It can probably be merged as is. Point (2) of my last message will cause occasional CI failures, but not on master and only if you're doing something weird. (1) will be easier to address when the scripts are working, so we can do both at the same time.

[Scott Morrison]

The generate new token page has a big list of different "scopes" you can select. By default none are set --- does anyone know which one is necessary for cache-olean?

[Bryan Gin-ge Chen]

I think public_repo should work, but I haven't tested it with update-mathlib specifically.