update-mathlib, and branches

Stream: general

[Scott Morrison]

Am I correct in understanding that we can't use update-mathlib in a project the depends on a branch of mathlib, because travis doesn't post archived oleans for branches?

[Scott Morrison]

If that's the case, I would really like to fix this.

[Scott Morrison]

In particular, I want to be able to try something out in the lean-perfectoid-spaces repository, based on the presheaf branch of mathlib. This branch makes lots of edits to existing files in mathlib, so there's no option to just copy and paste the relevant files into lean-perfectoid-spaces. It seems the only options are: everything waits until the presheaf PR is merged, or give up update-mathlib (and thus not be able to convince Kevin to try things out :-).

[Simon Hudon]

You're right, update-mathlib is only useful with master. That's out of concern for disk space on GitHub

[Scott Morrison]

Okay! Now I remember we discussed this before, and the proposed solution was that I provide the disk space.

[Scott Morrison]

If we were going to do this, my preferred method would be that I pull olean archives, rather than having travis directly push them to me.

[Scott Morrison]

There could still be a webhook (that's a fancy name for making an http request, right? :-) for travis to initiate the pull, I guess.

[Simon Hudon]

I'm not sure about what you're thinking of. Why would Travis need to pull an archive?

[Scott Morrison]

Sorry, I was thinking the following:
1) When travis finished building a non-master branch, it pushes the olean cache to somewhere on Github
2) It then calls some webhook running on my server etc https://tqft.net/update-olean-caches
3) My server then grabs the new archive file full of olean files
4) When people run update-mathlib or cache-olean --fetch on non-master branches, it checks my server
5) We periodically clean out the non-master branches stored on Github

[Scott Morrison]

Alternatively, we just do 1) and 5), and see if there's enough space on Github. :-)

[Scott Morrison]

I'm aware this may be getting too complicated.

[Simon Hudon]

It may be easier if we get Travis to push the archives to your server directly in the end. But as an approximation, we can get started with just pushing a nightly build for every commit

[Scott Morrison]

The thing I was trying to avoid was having to give travis the ability to hack my server. :-)

[Scott Morrison]

Other alternatives might be to have travis push to amazon S3. (I could certainly pay this this.)

[Simon Hudon]

Maybe we can pool some money for that

[Scott Morrison]

I already have a process set up to pay for storage of various research data on amazon. It's trivial to include something like this.

[Simon Hudon]

Cool! Already, the Travis build has github credentials encoded into it but I secured them.

[Scott Morrison]

oh, okay

[Scott Morrison]

I'm actually pretty relaxed about my server. :-) If you know how to give credentials to travis in a reasonable way, I can just give you ssh keys or something.

[Simon Hudon]

But amazon S3 sounds like a good idea. If you give me access, I can get started with that

[Scott Morrison]

Ok! I will remember how to add authorisation to a bucket.

[Kevin Buzzard]

PS I don't mind building mathlib; but I wouldn't like to be going around saying "the perfectoid project builds, except we need a branch of mathlib". These mathlib maintainers sometimes make you change your PR's, and then you have to fix a bunch of stuff :P

[Scott Morrison]

I'm not sure this is entirely fair -- it's not like a branch of mathlib is inherently more dangerous than code outside of mathlib entirely! :-) In any case, these PRs seem to be working through the system, and hopefully after those two I can avoid needing to change mathlib files.

[Kevin Buzzard]

I guess what I mean is "well, we never did this before, it looks new and scary to me"

[Kevin Buzzard]

It's fear of branches.

[Scott Morrison]

I'll just experiment in a branch for a moment.

[Kevin Buzzard]

But actually I did make a branch of the perfectoid project recently, and after figuring out what the hell was going on with the olean files I did manage to pull off a sane workflow.

[Scott Morrison]

@Simon Hudon, I've been trying to understand the amazon docs, and things seem to have got more complicated since I last used it... I'm struggling to work out how to just hand you a token that gives read+write access to a specific bucket.

[Scott Morrison]

I've certainly done this in the past, but long in the past.

[Simon Hudon]

I'm not clear on how it works. I'll have a look when I wake up

[Simon Hudon]

Here is something that I found in the travis documentation:

https://docs.travis-ci.com/user/deployment/codedeploy/#s3-deployment-or-github-deployment

[Simon Hudon]

There's an option for automatically deploying to s3

[Simon Hudon]

and this might help too: https://aws.amazon.com/blogs/security/wheres-my-secret-access-key/

[Simon Hudon]

@Scott Morrison Once you find your secret access key, we'll set it up in a travis encrypted environment variable. If you want to send it to me encrypted, I can give you my PGP key