IMPORTANT NOTICE: github and mathlib

Stream: general

[Simon Hudon]

We are in the process of moving mathlib from leanprover to leanprover-community. We will be inviting all the current contributors of mathlib to this new location but only the current maintainers will have write access to the master branch. All other branches will be available to write to. Please look at you inboxes for an invitation (if you currently have access to leanprover-community/mathlib) and update your leanpkg.toml files to point to leanprover-community/mathlib instead of leanprover/mathlib.

[Kenny Lau]

What happened?

[Simon Hudon]

github.com/leanprover and specifically github.com/leanprover/mathlib are owned by Leo and we decided to to move it github.com/leanprover-community so that we can manage the access rights without bothering Leo every time

[Simon Hudon]

Edit: you only need to update leanpkg.toml for your packages that import mathlib

[Kenny Lau]

who are "we"?

[Mario Carneiro]

We've been discussing this in the super secret maintainers club

[Kenny Lau]

I see

[Mario Carneiro]

Leo thinks it would be better to move mathlib away from the leanprover organization, and I think it would be better for him and us

[Mario Carneiro]

Note: the moves have not happened yet, so it's probably a bit early to change your toml files

[Simon Hudon]

We're in touch with Leo and github trying to make it happen. It should happen any minute now.

[Mario Carneiro]

also the important part has to be initiated by leo so it depends on how on the ball he is

[Simon Hudon]

Right now we're waiting on the github team actually. Leo responded very quickly.

[Bryan Gin-ge Chen]

Might be good to add some instructions to the README on this after it drops.

[Mario Carneiro]

Actually, we just discovered that github automatically redirects for moved repositories, so I think we should do nothing re: marking the move

[Mario Carneiro]

My guess is all your remotes will continue to work as normal after the move

[Simon Hudon]

That's correct.

[Simon Hudon]

Leo now completed his side of the operation but we faced more obstacles than expected. Here is the current state of affair:

• what used to be leanprover/mathlib is now leanprover-community/mathlib-2
• what used to be leanprover-community/mathlib is now leanprover-fork/mathlib-backup

Their previous URL also work still. In particular, all the branches that used to be at leanprover-community/mathlib are now at leanprover-fork/mathlib-backup. We will keep using them until they are all merged or deleted. All new branches should be created on leanprover-community/mathlib-2 which will now be the source of all truth. Only maintainers will be allowed to push to leanprover-community/mathlib-2/master however.

[Simon Hudon]

If you used to have write access to leanprover-community/mathlib, you should have received an invitation to contribute to leanprover-community/mathlib-2.

[Simon Hudon]

Any questions?

[Bryan Gin-ge Chen]

Is mathlib-2 the "official" name going forward?

[Simon Hudon]

I'm hoping that it won't be. I asked Leo to rename it to mathlib-2 because github refused the transfer when it was called mathlib. Now that it's called mathlib-2, Leo doesn't have anything else to do to help us with the transfer. I'm getting in touch with the github team to allow us to replace what used to be leanprover-community/mathlib.

[Mario Carneiro]

did the rename to leanprover-community/mathlib-backup not work?

[Simon Hudon]

It worked but left behind a redirect which I couldn’t overwrite

[Mario Carneiro]

I mean where did the lp-fork user come from?

[Simon Hudon]

I created it just for this occasion. I’ll delete it when we’re done with this repo

[Simon Hudon]

Update: I just renamed leanprover-community/mathlib-2 to leanprover-community/mathlib. I think the name was only blocked to transfers.

[Simon Hudon]

Now, leanprover/mathlib and leanprover-community/mathlib both point to the same repo.

[Mario Carneiro]

I see the branch protection for master has CI status checks enabled. I think this is not a good idea, since it takes 45 minutes to run the CI, it's going to really throttle our ability to push stuff

[Mario Carneiro]

at least, I think we need to see if this is going to cause a problem

[Simon Hudon]

I see. We could have a branch “stable” which we make sure always builds this way. How about that?

[Reid Barton]

Or we could call it "lean-3.4.2“

[Simon Hudon]

I like it

[Simon Hudon]

We could also make lean-3.4.2 into a tag which travis pushes when a build on master succeeds

[Bryan Gin-ge Chen]

that will fix the leanpkg issues, right?

[Simon Hudon]

which one do you mean?

[Bryan Gin-ge Chen]

I seem to recall that leanpkg upgrade wouldn't update mathlib if I had lean_version = "3.4.2" in leanpkg.toml. I can try to check after another commit gets pushed to master. I've been using "nightly" in that option so it gives a warning, but then running leanpkg upgrade does keep mathlib up to date.

I thought there was also an issue with leanpkg new and leanpkg add but I can't seem to reproduce it now.

[Simon Hudon]

I think it would fix the first one but I'm not sure about the second one

[Mario Carneiro]

so the move is complete now?

[Simon Hudon]

Mostly. We can already start working only with leanprover-community/mathlib and the only exception is the existing PRs that refer to leanprover-fork/mathlib-backup. Once we're done with those, I think the transfer will be complete.

[Simon Hudon]

People can, at their leisure, move the branches that aren't part of PRs from mathlib-backup to mathlib

[Mario Carneiro]

does this help? https://help.github.com/articles/changing-the-base-branch-of-a-pull-request/

[Simon Hudon]

No, the base is the branch located in lp-community

[Kenny Lau]

why is my build > 15 mins? Is there some issue with the caching?

[Kenny Lau]

Also is #658 working?

[Kenny Lau]

I think this is very confusing. Can someone loop me in as to the current status of affairs?

[Kenny Lau]

before your moves I had a branch leanprover-community/mathlib/submodule-mul

[Mario Carneiro]

AFAICT it's building

[Kenny Lau]

and after your moves I tried pushing to that branch again from git

[Kenny Lau]

and it automatically created a new branch instead of redirecting it to the fork branch

[Kenny Lau]

and that is a problem because #658 listens on the fork branch

[Mario Carneiro]

the new thing is to push your stuff to a branch on mathlib itself, which has the same name as the old community mathlib

[Kenny Lau]

so I need to set up the new upstream manually

[Kenny Lau]

but the pull requests listen on the fork branches...

[Mario Carneiro]

I guess that's a grandfather thing... push to the fork for your old open PRs, create lc/mathlib branches in the future

[Kenny Lau]

AFAICT it's building

yes, but I don't see any evidence of caching

[Mario Carneiro]

who knows, I wouldn't worry about it unless it happens every time

[Kenny Lau]

I think the caches on the old leanprover-community/mathlib haven't been moved to leanprover-fork/mathlib-backup

[Kenny Lau]

that's why there are no caches there

[Mario Carneiro]

it looks like it did download a cache, but we don't have a lot of diagnostic info on what cache data travis is using

[Kenny Lau]

this is a bad sign as we have 25 open PR's, if each of them needs to be built once then we would lose a lot of time

[Mario Carneiro]

only if they push new commits

[Kenny Lau]

also I get a strange "view #658" button when I visit leanprover-community/mathlib/submodule-mul

[Mario Carneiro]

it's not like we can do anything about it... the caches are very brittle. If they don't work, regenerate them. If those don't work we have a problem

[Kenny Lau]

does this suggest that somehow it is connected to the other branch?

[Mario Carneiro]

it is the same commit

[Mario Carneiro]

oh, https://travis-ci.org/leanprover/mathlib is a 404

[Mario Carneiro]

I guess travis can't handle the move as smoothly as github

[Mario Carneiro]

could be related to the loss of cache

[Kenny Lau]

yep

[Kenny Lau]

anyway can you review #658? :P

[Johan Commelin]

I just learned that the "maintainers elected in Amsterdam now have commit rights". I'm very sorry for not having been able to attend this discussion in Amsterdam. Out of curiosity, is this list of maintainers documented somewhere?

[Patrick Massot]

mathlib readme

[Patrick Massot]

I'm also sorry I missed that. I would have volunteered for documentation maintainership

[Patrick Massot]

Inspired by this successful change of ownership, we decided to redo properly the move of perfectoid spaces from Kevin's account to leanprover-community. So I pulled back all commits to the old repository and deleted the new one. Now I need someone with correct rights (@Simon Hudon ?) to grant Kevin the right to create a repository in leanprover-community, so that he can transfer properly (with redirections, without loosing watchers and stars etc.)

[Johan Commelin]

mathlib readme

Aah, thanks. Hadn't seen that yet. So @Johannes Hölzl isn't mentioned in that list, but he's the person doing almost all merges right now? :grinning:

[Simon Hudon]

@Johannes Hölzl is moving to the dark side of computer science: he's leaving academia to go work in a place called real world (never heard of it before). He still has rights but we won't be assigning him any work

[Simon Hudon]

@Patrick Massot @Kevin Buzzard : I just extended Kevin an invitation so that he can move his repo

[Johannes Hölzl]

@Simon Hudon is right, I don't think I will have time to work on mathlib in the future. I added the list of maintainers and deliberately put not myself on it.