mathlib nightlies

Stream: general

[Patrick Massot]

Is there any reason why mathlib nightlies are pre-releases and not releases? It makes it harder to fetch them.

[Patrick Massot]

This is done here at the very end of the line.

[Patrick Massot]

@Simon Hudon ?

[Patrick Massot]

Specifically, this choices makes it impossible to use https://developer.github.com/v3/repos/releases/#get-the-latest-release

[Rob Lewis]

No idea. Would changing it require updates to cache-olean/update-mathlib too? I wouldn't be inclined to spend much time changing this. Instead we should figure out the infrastructure to store builds for each commit on our own server.

[Patrick Massot]

No, this would have no impact on existing scripts. They loop through all releases, pre or not.

[Patrick Massot]

Rob, do you have enough admin power to change the latest nightly into an actual release?

[Rob Lewis]

Done, although I'm not sure what difference it makes...

[Patrick Massot]

Awesome! I explained the difference a few messages ago (the one with a GitHub API link)

[Rob Lewis]

Ah, sorry, missed that message.

[Patrick Massot]

No problem.

[Sebastian Ullrich]

I originally set up Lean nightlies as pre-releases because semantically it seemed more appropriate, and elan can't use the API anyway because of the rate limiting.

[Patrick Massot]

Thanks for the explanation. My experience is the API rate limiting is annoying when developing tools, but ok when using them.

[Sebastian Ullrich]

That depends on your expected number of users. It would not scale at all for elan.

[Patrick Massot]

I don't understand what you mean. Each user gets a limit, right?

[Sebastian Ullrich]

Each public IP address gets a (very low) limit, afair. I think we had some issues from users/scripts sharing an IP address.

[Patrick Massot]

I see that IP sharing could an issue in universities.

[Patrick Massot]

Currently I guess this matters only for people working at VU.

[Patrick Massot]

and maybe CMU.

[Gabriel Ebner]

At VU (and TU Wien) every computer has their own public IP so this shouldn't be an issue.

[Rob Lewis]

I disabled the cache-olean githook because I was getting rate limiting errors when switching around a bunch of branches. (Also it was kind of slow.) So it does come up in practice.

[Rob Lewis]

Again, we should probably start hosting these things ourselves pretty soon.

[Johan Commelin]

What do we need of a host for the nightlies?

[Johan Commelin]

The bandwidth won't be that much, right?

[Johan Commelin]

I've got a server running in my basement, I'm fine with hosting stuff.

[Mario Carneiro]

the main problem with basement servers is uptime

[Johan Commelin]

Sure

[Johan Commelin]

Currently I've been up for 250 days in a row...

[Johan Commelin]

But I agree that it is fragile

[Mario Carneiro]

Maybe we can get a mirror setup and crowdsource several basement servers?

[Johan Commelin]

Yup, I guess that would work

[Patrick Massot]

I think Scott also said he could host stuff at some point.

[Patrick Massot]

How could we have a mirror setup? Doesn't it require a server that is always responding?

[Johan Commelin]

But supposedly that would be very lightweight

[Johan Commelin]

You could host a static file with URLs on github.io

[Johan Commelin]

And clients can cache the URLs, if all of them fail, check on github.io what the latest URLs are

[Johan Commelin]

Maybe I should say hostname instead of URL

[Johan Commelin]

And then we manually maintain that list of server hostnames on github.io

[Patrick Massot]

Maybe we could even use torrents.

[Patrick Massot]

But we should let people who know about computers setup all this.

[Rob Lewis]

Buying actual space/bandwidth on Azure/S3/whatever will cost pennies if anything at all. Jasmin said he's happy to use grant money to cover it, if the time cost of getting it reimbursed is less than the monetary cost, which remains to be seen.

[Patrick Massot]

How would that work?

[Rob Lewis]

How would what work?

[Patrick Massot]

Using Azure/S3/whatever.

[Rob Lewis]

We get server space and push olean caches there instead of to a random GitHub repository.

[Rob Lewis]

cache-olean/update-mathlib get pointed there instead of to the nightly repos.

[Patrick Massot]

Sounds easy.

[Rob Lewis]

Indeed.

[Patrick Massot]

What would the url look like?

[Rob Lewis]

Dunno if there's a default. Worst case we buy leanprover-community.info for €10.

[Rob Lewis]

lean.loan?

[Rob Lewis]

I don't want something cheap. I want something we don't need to waste time maintaining. A network of basement servers with a URL cache on GitHub doesn't sound like that.

[Patrick Massot]

See Johan? We need the computer experts to handle that.

[Rob Lewis]

The computer expert is on the case. Everyone hold your breath for 90 minutes. https://github.com/leanprover-community/mathlib/runs/460051728

[Patrick Massot]

RESPONSE Status: 403 This request is not authorized to perform this operation using this permission. :sad:

[Rob Lewis]

Arbitrary file size limit. https://github.com/leanprover-community/mathlib/runs/460227887?check_suite_focus=true

[Patrick Massot]

Are you sure? This message really sounds like a permission issue.

[Gabriel Ebner]

I think what happens is the following: if the file is very small, it's uploaded in one go. If the file is larger, then it is uploaded in two or more parts. For security reasons, we're disallowing write operations (only create is allowed). So appending is disallowed.

[Rob Lewis]

I'm "sure," in that I reproduced and solved it locally with a flag to allow larger files.

[Patrick Massot]

I knew this should be handled by people working in a CS department.

[Patrick Massot]

RESPONSE Status: 403 Server failed to authenticate the request. Make sure the value of Authorization header is formed correctly including the signature.

[Patrick Massot]

I guess this is progress.

[Rob Lewis]

Yes, I'm aware.

[Patrick Massot]

Maybe we need a toy project to test this without waiting 90 minutes between each try.

[Rob Lewis]

download a 21mb mathlib build here

[Rob Lewis]

You were wondering about the url? Nothing could be better than oleanstorage.blob.core.windows.net/mathlib!

[Rob Lewis]

In the 27 hours since this landed, we've accumulated 900mb of olean caches.

[Patrick Massot]

We should probably decide a conservation policy pretty quickly.

[Patrick Massot]

And implement it.

[Rob Lewis]

I don't think there's a huge hurry. The policy I have in mind is to keep branch builds for a month and master builds forever. So we have a month to implement that before it will matter.

[Rob Lewis]

Maybe more helpful: should we try to cancel artifact uploads from non-master branches if another commit is added to that branch before the build finishes?

[Patrick Massot]

Won't we hit the disk quota in one week instead of one month?

[Rob Lewis]

The free account comes with $170 credit. It'll be a while before we burn through that.

[Rob Lewis]

Even if we go over the disk quota.

[Patrick Massot]

Does it start eating up that credit automatically as soon as we go over quota?

[Rob Lewis]

I think we should get the infrastructure working, see what the usage looks like, and then figure out how we're paying long term.

[Rob Lewis]

We'll find out!

[Rob Lewis]

Rob Lewis said:

Maybe more helpful: should we try to cancel artifact uploads from non-master branches if another commit is added to that branch before the build finishes?

This might actually be the most useful move to save space. A lot of very useless archives will be stored by people updating a PR incrementally, like by accepting suggestions from comments. Is there a situation where someone would need to check out those oleans?

[Patrick Massot]

I don't think we would ever use those oleans.

[Gabriel Ebner]

In my current usage I don't need these oleans either. I typically push to a branch, and then do a curl https://oleanstorage.blob.core.windows.net/mathlib/$(git rev-parse HEAD).tar.gz | tar xz once the build is finished. I don't need anything except the oleans for the latest revision. This might be different if multiple people are working on a branch.