all future PRs should be made from forks

Stream: mathlib4

[Kim Morrison]

We've built a new CI setup for Mathlib, that removes the need for contributors to make PRs from branches pushed directly to the leanprover-community/mathlib4 repository, and instead allows making PRs from forks (i.e. per the usual practice for any git repository).

[Kim Morrison]

We will shortly begin removing write access to the repository from contributors.

[Kim Morrison]

Regardless of whether you still have write access, please do not open further PRs from branches on the main repository: instead open them from branches on your own fork.

[Kim Morrison]

We have provided a migration tool to assist in moving an existing PR to your own fork. You will need to merge master into your branch, and then run scripts/migrate_to_fork.py.

[Kim Morrison]

(Note that once we begin removing write access, if you have an old PR you will not be able to push more commits to it until you migrate it.)

[Kim Morrison]

@channel Please note the announcement above: all new PRS must be made from forks.

[Yakov Pechersky]

May I suggest to have documentation for users on how to do pulls/merges/cherry picks across forks? Sometimes I might want to base a PR on another branch that someone else wrote. Or even just cherry pick another branch's commit. It's possible to do in fork land, requires adding new remotes. But others might not be as familiar with this.

[Niels Voss]

Can this be posted in the announcement channel as well?

[Kim Morrison]

Yakov Pechersky said:

May I suggest to have documentation for users on how to do pulls/merges/cherry picks across forks? Sometimes I might want to base a PR on another branch that someone else wrote. Or even just cherry pick another branch's commit. It's possible to do in fork land, requires adding new remotes. But others might not be as familiar with this.

I'm not sure that there's anything to write here that is Mathlib specific, and there are plenty of good git tutorials (and all the AIs can do this stuff very well by now). If anyone would like to write something specifically addressed to users of Mathlib, we can certainly link to it!

[Thomas Murrills]

Won’t this make collaboration a lot more difficult? How are multiple people supposed to collaborate on a PR?

[Kim Morrison]

The owner of the fork the PR is being made from can give out write access to collaborators there.

Alternatively, one can make PRs to the PR branch.

[Bolton Bailey]

Needing to grant permission seems like it could be a lot more friction. I have a lot of please-adopt PRs but I do not receive emails from github and it seems possible that if someone wanted to contact me to be added, I might not notice for a while.

[Thomas Murrills]

Hmm, I’m not sure making PRs to a PR branch is really feasible in practice—there’s a lot of admin involved there.

But the alternative—moving between entirely different repos/forks to switch from working on a personal PR to working on a collaborative effort, and remembering which repo is associated with which collaboration—maybe seems worse? :sweat_smile: (Maybe there are benefits I’m not thinking of, though? Separate windows in VS code can be a pro or a con…)

I trust there’s a necessary reason for this, of course. But I wonder if we can make collaboration nicer for mathematicians (who might not be so git-savvy) in the future somehow, either with tooling or something else.

[Tanner Duve]

will PRs that are currently under review be merged directly to the main repo? Or should I migrate it?

[Kim Morrison]

You should migrate it please, if you anticipate needing to push any further commits to the branch.

[Kim Morrison]

If you think it will be merged as is it's probably fine to leave for now.

[Johan Commelin]

Bolton Bailey said:

Needing to grant permission seems like it could be a lot more friction. I have a lot of please-adopt PRs but I do not receive emails from github and it seems possible that if someone wanted to contact me to be added, I might not notice for a while.

In case of those please-adopt PRs, the person who wants to adopt the PR can pull your branch to their fork, and continue the rest of the work from their fork. I imagine they would then open a new PR, linking to your please-adopt PR.

[Kim Morrison]

In fact, they can use the migrate-to-fork.py script for exactly this purpose!

[Yakov Pechersky]

One possible unintended (negative) side effect that will increase noise is -- currently, it is very useful when a PR (let's say 9876) or issue refers to another PR by mentioning #12345 in a git commit or github comment. That mention appears on the 12345 github page as a breadcrumb, very useful to have this informative link.

Then, once 9876 is merged to master, the bors driven commit leaves another breadcrumb on 12345. Then all community contributors merge upstream master into their master. Each of those merge commits will leave a breadcrumb on 12345 as well.

[Chris Henson]

For variety, I'll express my opinion of welcoming this change. I don't think that for collaboration it is too onerous to add people to a repo (or just make PRs in the fork as Kim suggests). In return, it seems that we get a much more limited set of those with write access, a more standard process with less friction for new contributors, and I assume some benefits in partially decentralizing CI. I'm sure this took effort, thanks for your work!

[Yakov Pechersky]

Would there be some way of configuring Mathlib issues and PRs in github to not show fork breadcrumbs?

[Kim Morrison]

@Yakov Pechersky could you link to such a breadcrumb? So far I don't understand what you mean.

[(deleted)]

I trust there’s a necessary reason for this, of course.

There definitely is a valid reason. While I haven't seen anyone deleting all the branches in Mathlib this is bound to happen.

[Yakov Pechersky]

I'm in mobile right now, so my screenshot is of the mobile app. By breadcrumb I mean the "referenced this" entries in the conversation flow. 042598ad-9fca-4085-b50c-87a726424b33.png

[Kim Morrison]

Okay, if you see breadcrumbs appearing inappropriately in irrelevant places, please post a link!

[Thomas Murrills]

(For the record, let me be clear and also applaud the work done here in making Mathlib more secure! I certainly don’t mean to naysay it just by worrying about changing collaboration workflows and such. :) )

[Damiano Testa]

As with all change, something is lost and something is gained.

With this change, I think that aligning with well-tested and established workflows, not having to rely on asking for permissions to propose a change and managing your own version of mathlib while developing a PR are all big advantages that outweigh the negatives.

[Jz Pan]

Do I need to close my current PRs and reopen new one? Seems that the source branch in a PR can't be edited.

[Johan Commelin]

Kim Morrison said:

We have provided a migration tool to assist in moving an existing PR to your own fork. You will need to merge master into your branch, and then run scripts/migrate_to_fork.py.

@Jz Pan :up:

[Jz Pan]

I've read that script. But I'm on Windows and don't have the dependency installed (e.g. gh command line tool). Since currently I have only one open PR so I'd rather like to do it manually.

Do the following steps correct?

1. Fork mathlib
2. In my computer, change the remote to my fork and push my working branches to my fork
3. close my current PRs and reopen new one
4. that's all?

[Jz Pan]

(deleted)

[Johan Commelin]

Yup, that's the gist of it!

[Jihoon Hyun]

Then will all (contributed) branches be removed from Mathlib? If so, it should be nice to announce that also, to make sure to notice everyone who needs backup.

[Johan Commelin]

I don't think we need to rush that.

[Wrenna Robson]

This is a cool change. Will it change anything about CI from a point of view of mathlib caching and that.

[Kim Morrison]

It should be working. There are now isolated caches for each fork, plus a central cache that is only updated when changes hit master.

[Kim Morrison]

(I should say: this change was a huge effort, with many people helping! Thanks to @Johan Commelin, @Mac Malone, @Sebastian Ullrich (this has been a significant priority for the FRO this quarter), as well as @Bryan Gin-ge Chen, @Damiano Testa, @Matthew Ballard, and @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 for making it happen, and to many others for testing and advice.)

[Kim Morrison]

(and ... :drum: there's more goodies, including caching for all downstream projects, in the pipeline. :-)

[Robin Carlier]

Kim Morrison said:

(and ... :drum: there's more goodies, including caching for all downstream projects, in the pipeline. :-)

By this, do you mean that downstream projects can host and maintain cache server for them, or that some downstream projects will be cached on FROs server, or both?

[Kim Morrison]

TBD, I think.

[Robin Carlier]

Some things I noticed with the migration script:

• draft PRs are reopened as non-draft PRs when migrated.
• for PRs depending on others, the migrated PRs uses the old numbers for dependent PRs and have to be manually updated with the new dependency, but this is probably hard to tackle, and ultimately not too bad.

[Robin Carlier]

It also looks like dependabot consider that a closed PR is a merged PR, and so removes the "blocked-by-other-PR" tag when a pr gets migrated. Perhaps the bot should check that the pr gets closed and merged by bors?

[Niels Voss]

Will all the branches be preserved? There's probably a substantial amount of work that never got PR'd and might be lost if the branches were deleted

[Matthew Ballard]

Niels Voss said:

Will all the branches be preserved? There's probably a substantial amount of work that never got PR'd and might be lost if the branches were deleted

Using the GitHub web interface, all branches will get copied to the fork if you uncheck the little box that says copy only the default branch (see eg https://github.blog/changelog/2022-07-27-you-can-now-fork-a-repo-and-copy-only-the-default-branch/)

[Matthew Ballard]

Re: migration script, we expect there will be some edge cases. The same holds the full suite existing CI. Please complain loudly about things that don’t work as expected (or better yet propose fixes).

[Matthew Ballard]

Kim Morrison said:

(I should say: this change was a huge effort, with many people helping! Thanks to Johan Commelin, Mac Malone, Sebastian Ullrich (this has been a significant priority for the FRO this quarter), as well as Bryan Gin-ge Chen, Damiano Testa, Matthew Ballard, and 𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 for making it happen, and to many others for testing and advice.)

Says atlas as they hold up the world ;) Thanks @Kim Morrison!

[Robin Carlier]

Matthew, the link you gave says that the default is precisely the inverse: by default, only master gets copied.
But if yes if you uncheck that checkbox, you get all branches.

[Matthew Ballard]

I think you need to opt in for this

[Matthew Ballard]

Oh no, you need to opt out for this! Using gh this is not the case

[Antoine Chambert-Loir]

Ultra-naïve question: how does one fork mathlib?

[Christian Merten]

Here: https://github.com/leanprover-community/mathlib4/fork

[Robin Carlier]

there is also a "fork" button on the right of mathlib's name on the repo main page.

[Antoine Chambert-Loir]

Is there a naming rule for the branches we create by forking?

[Ruben Van de Velde]

No

[Matthew Ballard]

At least two options that I know of:

1. gh repo fork leanprover-community/mathlib4
2. GitHub web interface: click on the little fork icon
   

[Matthew Ballard]

You can also do it more manually but unless you need to I wouldn’t recommend it

[Matthew Ballard]

The migration script includes the creation of a fork.

[Robin Carlier]

Anyways, a big thank for the migration script! without it, migrating 30PRs would have been a very very massive pain!

[Matthew Ballard]

Did you do all 30 already?

[Sébastien Gouëzel]

I've created my fork and the first branches in it. As far as I can tell, CI does not run on the branches. Do I understand correctly that, for CI to run, I should create a PR to mathlib? Side question: if the branch is for experimentation, and will never become a true PR, should I mark it as WIP, or should we have another label for that?

[Robin Carlier]

Matthew Ballard said:

Did you do all 30 already?

yup

[Robin Carlier]

(I did not count fixing the CI errors induced by merging master on some old PRs in the "migration", though, this will definitely take more time)

[Matthew Ballard]

Sébastien Gouëzel said:

I've created my fork and the first branches in it. As far as I can tell, CI does not run on the branches. Do I understand correctly that, for CI to run, I should create a PR to mathlib? Side question: if the branch is for experimentation, and will never become a true PR, should I mark it as WIP, or should we have another label for that?

I think the answer depends on which CI workflow you are talking about. I’ve had the main build step go through on pushes to branches on my fork.

Side question: this is for PR you just making for extra CI goodness? I did that in the previous setup quite a bit (eg bench) and just marked it draft.

[Jeremy Tan]

Running the migration scripts on my end now. First fork PR is #25770

[Jeremy Tan]

Is it OK?

[Emily Riehl]

I have a whole bunch of open PRs, only one of which (#25646) has a chance of being merged as is. I'm also not as experienced with standard git workflows (having never pushed to anything from a fork). I interact with github from the website (creating and managing repositories) and from the command line (frequently running the basic commands but with no advanced skills).

After creating my fork (which I haven't yet done) and migrating all my PRs, I'd like to delete the local clone of mathlib (directly from the main repository, not from a fork) and replace it with a local version of my fork. But I'm not quite sure about the correct order of operations.

Is this the correct workflow:

1. First I need to fork mathlib (eg using the web interface).
2. Then I need to migrate each open PR. Can I run the script mentioned above without having a local clone yet of my fork?
3. After doing this am I safe to delete my local clone of mathlib and replace it with a local clone of the fork?
4. Having done all of this how do I keep my fork up to date with the main mathlib?
5. Having done all of this how do I invite all of the contributors to my PRs to give them continued access. Each one has a different contributor subset. Should I just add all these people to my fork? Or do I need different forks for each collaborative PR? If the latter, how do people manage all of this? (Eg at the end of the year, will I end up with dozens of mathlib forks that I'm managing? If so, is there a way to have offline access to these without cluttering up everything?)

Perhaps relevant to the last question: I tend to prefer alternatives that are a bit simpler, even if less optimal from a security POV.

Apologies for the naive questions and thanks in advance.

[Sébastien Gouëzel]

Matthew Ballard said:

I think the answer depends on which CI workflow you are talking about. I’ve had the main build step go through on pushes to branches on my fork.

I meant the main build steps. On https://github.com/sgouezel/mathlib4/branches, I don't see any CI output in the check status, for instance. Should I maybe activate github actions or whatever?

[Sébastien Gouëzel]

(and it doesn't mention PR numbers, although I've opened PRs for all the three branches. I'm definitely doing something wrong here...)

[Robin Carlier]

@Emily Riehl : you don’t need to re-clone the fork. You can keep you local mathlib folder and the migration script will update its remotes (the things that tell git where to push/pull stuff) to have "origin" point to your github fork, and "upstream" point to mathlib.

[Robin Carlier]

So your local clone of mathlib will "become" the local clone of you fork

[Robin Carlier]

Similarly for collaboration, you can have as many remotes as you want in your mathlib local folder, all pointing to different forks if you want!

[Matthew Ballard]

Sébastien Gouëzel said:

(and it doesn't mention PR numbers, although I've opened PRs for all the three branches. I'm definitely doing something wrong here...)

Sorry for being dense, but what should mention the PR numbers

[Sébastien Gouëzel]

Matthew Ballard said:

Sorry for being dense, but what should mention the PR numbers

Sorry for not being clear. When I look at my branches on leanprover-community/mathlib (https://github.com/leanprover-community/mathlib4/branches), the "pull request" column shows the number of the PR I've opened for a given branch, and I can click on it to go to the PR. On my fork, (https://github.com/sgouezel/mathlib4/branches), the "pull request" column is empty, even though I've opened PRs for all these branches.

[Emily Riehl]

@Robin Carlier's answer to my question above makes me realize I don't understand the migration script. Where and when do I run it?

Should I create a fork first before running it, or run it first? If I have multiple open PRs, do I run this multiple times (after checking out each branch separately) or do I just run this once? Is the script creating separate forks for each one or moving them all to branches of a single new fork? What else do I need to know?

[Matthew Ballard]

Sébastien Gouëzel said:

Matthew Ballard said:

Sorry for being dense, but what should mention the PR numbers

Sorry for not being clear. When I look at my branches on leanprover-community/mathlib (https://github.com/leanprover-community/mathlib4/branches), the "pull request" column shows the number of the PR I've opened for a given branch, and I can click on it to go to the PR. On my fork, (https://github.com/sgouezel/mathlib4/branches), the "pull request" column is empty, even though I've opened PRs for all these branches.

I don’t see this either on mine. So I guess this is broken at the moment. Not sure if by design or some other reasons. Thanks for pointing it out

[Matthew Ballard]

Also, if people happen to be in the same room with me (or same building) right now, it will probably be more efficient to talk in person.

[Jeremy Tan]

Matthew Ballard said:

Also, if people happen to be in the same room with me (or same building) right now, it will probably be more efficient to talk in person.

Sorry, I'm not at Big Proof

[Kenny Lau]

sorry if this has been answered before, there are 100 messages here; will the CI stuff automatically come with the fork, or will we have to set it up ourselves?

[Matthew Ballard]

The essential CI should run on your fork but you may need to enable actions for the repository.

[Kim Morrison]

Emily Riehl said:

Is this the correct workflow:

1. First I need to fork mathlib (eg using the web interface).
2. Then I need to migrate each open PR. Can I run the script mentioned above without having a local clone yet of my fork?
3. After doing this am I safe to delete my local clone of mathlib and replace it with a local clone of the fork?
4. Having done all of this how do I keep my fork up to date with the main mathlib?
5. Having done all of this how do I invite all of the contributors to my PRs to give them continued access. Each one has a different contributor subset. Should I just add all these people to my fork? Or do I need different forks for each collaborative PR? If the latter, how do people manage all of this? (Eg at the end of the year, will I end up with dozens of mathlib forks that I'm managing? If so, is there a way to have offline access to these without cluttering up everything?)

Perhaps relevant to the last question: I tend to prefer alternatives that are a bit simpler, even if less optimal from a security POV.

Sorry if this is repeating answers elsewhere, I just want to make sure these points are all addressed in one place. @Emily Riehl

₁ You may create a fork before running migrate_to_fork.py, but don't need to --- on the first run the script will do this for you.
₂ You run the script by checking out each branch in turn, merging master (so the script is present), and running script/migrate_to_fork.py

* (Note that you can do this for branches with an associated PR, or for branches that don't yet have a PR.)
* (Also, if you have reason to not want to merge master, it's also fine to just copy the script off master.)
₃ Yes, if you've done this for every local branch, it should be safe, but also completely unnecessary. All that's happen after the script (with default settings) is that now the remote named upstream points to leanprover-community/mathlib4 while the remote named origin points to username/mathlib4.
₄ There are many solutions to keeping up to date. My suggestion would be to not keep up to date, and instead set your local copy of master to track the upstream remote, and just completely ignore the master branch in your fork:

git checkout master
git checkout -b master upstream/master

₅ If you go to https://github.com/emilyriehl/mathlib4/settings/access, you can give people access to your fork. I would recommend just adding anyone you regularly collaborate with there. There is only need for a single fork.

[Emily Riehl]

Kim Morrison said:

₄ There are many solutions to keeping up to date. My suggestion would be to not keep up to date, and instead set your local copy of master to track the upstream remote, and just completely ignore the master branch in your fork:

git checkout master
git checkout -b master upstream/master

This second command failed for me with the error

fatal: 'upstream/master' is not a commit and a branch 'master' cannot be created from it

Would you explain what it is trying to do?

[Riccardo Brasca]

I think you need first of all

git fetch upstream

[Emily Riehl]

Now there's a new error:

fatal: a branch named 'master' already exists

But I also don't understand what this command is trying to do.

[Riccardo Brasca]

git branch --set-upstream-to=upstream/master

should work

[Sébastien Gouëzel]

Another (very minor) annoyance with the new CI: when a build is queued, the build step doesn't show anything (while before it used to show something like "queued, waiting for an available runner").
queued.png

[Matthew Ballard]

Did that build eventually start?

[Robin Carlier]

It just occurred to me, is there a PSA issue about this or something about this change on GitHub? Or in the README.md? Some people with open PRs might not be following closely the zulip chat and might get confused

[Matthew Ballard]

The webpage needs updating

[Johan Commelin]

Note that this topic started out as "all future PRs should be made from forks", and it seems to have diverged into "all open PRs should migrate to forks".
While it is good to stress test the migration script, I don't think we need to rush migrating 1000 open PRs to forks in 24hrs or so.

[Robin Carlier]

The README.md as well.

[Sébastien Gouëzel]

Matthew Ballard said:

Did that build eventually start?

Yes, it did, after more than one hour, and completed fine. (The queue is currently very long, probably because of everyone moving the PRs to forks, and three four runners being offline)

[Matthew Ballard]

I think Github CI controls this information and there is no knob we can turn to get the old behavior back for a fork. Is there any info on the main repo?

[Kenny Lau]

Johan Commelin said:

Note that this topic started out as "all future PRs should be made from forks", and it seems to have diverged into "all open PRs should migrate to forks".
While it is good to stress test the migration script, I don't think we need to rush migrating 1000 open PRs to forks in 24hrs or so.

I think the issue here is that if we don't migrate, then we can't add on existing branches
(I agree tho that if it is a finished PR then there's no need to do it now)

[Sébastien Gouëzel]

Another data point: I have activated actions on my fork, but for branches which are not PRed to mathlib CI starts, but it skips all the steps. Any idea what I might be doing wrong?
skip.png

[Edward van de Meent]

Kim Morrison said:

channel Please note the announcement above: all new PRS must be made from forks.

i would really like to know why this decision has been made, particularly since it seems to have been made without any mention of open discussion in the community or at least on zulip? If mathlib is to be a community project, surely the community should have a say in, or at least be informed about ongoing decision making about the project? To me this news comes like a bolt from the blue...

[Johan Commelin]

I'll respond to that in a DM

[Sébastien Gouëzel]

Sébastien Gouëzel said:

Another data point: I have activated actions on my fork, but for branches which are not PRed to mathlib CI starts, but it skips all the steps. Any idea what I might be doing wrong?

Looks like it's not specific to my setup. For instance, https://github.com/mattrobball/mathlib4/actions shows that all actions are also skipped there.

[Johan Commelin]

I think CI will only run on PRs.

[Johan Commelin]

If you want CI for some branch, then I think it's best to create a WIP/draft PR

[Sébastien Gouëzel]

That's what I had understood, but Matthew told me the following:

Matthew Ballard said:

The essential CI should run on your fork but you may need to enable actions for the repository.

[Matthew Ballard]

I thought I had observed this. Though the sample set might have just been PRed branches

[Matthew Ballard]

Robin Carlier said:

The README.md as well.

#25810

[Eric Wieser]

Should we split messages about moving existing PRs to a new thread?

[Matthew Ballard]

Matthew Ballard said:

The webpage needs updating

This is in process at https://github.com/leanprover-community/leanprover-community.github.io/pull/638 (linkifier…?)

[Bryan Gin-ge Chen]

Matthew Ballard said:

This is in process at https://github.com/leanprover-community/leanprover-community.github.io/pull/638 (linkifier…?)

Per your suggestion, I've merged, but there are still various things that need to be fixed.

[Bryan Gin-ge Chen]

Sébastien Gouëzel said:

That's what I had understood, but Matthew told me the following:
Matthew Ballard said:

The essential CI should run on your fork but you may need to enable actions for the repository.

CI will run on PRs from forks even if GitHub actions isn't enabled in the fork (I just tested by disabling actions in my fork and submitting a PR); in fact, I think if you enable actions in your fork you might get CI errors from workflows that aren't designed to be run in forks (though the last ones I'm aware of should be disabled in #25813).

[Joe Taber]

As for managing merges and cherry picks from multiple users, maybe using Github Merge Queues could help. Though maybe you'd want to save this for later, it seems reasonable to limit a project to one big development workflow transition at a time. :smile:

[Sébastien Gouëzel]

Another small issue in the new PR management (not sure it's by design or not): when a PR is merged from a fork, the branch is not deleted automatically.

[Notification Bot]

A message was moved from this topic to #mathlib4 > Feedback on scripts/migrate_to_fork.py by Eric Wieser.

[Eric Wieser]

Kenny Lau said:

I think the issue here is that if we don't migrate, then we can't add on existing branches
(I agree tho that if it is a finished PR then there's no need to do it now)

We are explicitly not at this moment removing write access for everyone. At some unspecified date in the future, you will need to migrate open PRs to forks, and you are welcome to choose to do so before this date (especially for unreviewed PRs). There should be no technical restriction preventing you from pushing new commits to existing branches.

What changed is that there now is a technical restriction that prevents creating any new branches.

[Bryan Gin-ge Chen]

Sébastien Gouëzel said:

Another small issue in the new PR management (not sure it's by design or not): when a PR is merged from a fork, the branch is not deleted automatically.

bors does this auto-deletion for us now, but it doesn't have permission to delete branches in the forked repos. There's also a repo setting to auto-delete but I suspect this also won't work for branches in forks.

[Shreyas Srinivas]

@Emily Riehl : About keeping your fork up to date. GitHub provides a button to do this with the text “Sync fork”. When you create a fork of mathlib, I suggest never pushing to its master branch. As before, create a fresh new branch for every PR.

[Shreyas Srinivas]

As long as you keep the master branch free from any commits of your own, the sync fork feature will bring the master branch of your fork up to date with the main repository

[Thomas Murrills]

Could we possibly write down somewhere a ‘standard’ process for setting the correct upstream & remotes, syncing regularly, etc. which would be suitable for slightly git-averse mathematicians (like myself)?

E.g., I’m not looking forward to switching to a browser window, clicking the “sync fork” button (currently how I do it for fork-model repos), running git fetch, etc., all to merge master…which is what I would have done by default.

[Jireh Loreaux]

You can generally do everything you want through the GitHub cli (e.g., gh repo sync etc.)

[Shreyas Srinivas]

you don’t have to do much. Just go to your fork on GitHub and if it is behind the main repository, GitHub will point that out and suggest that you sync fork

[Shreyas Srinivas]

My main suggestion is to keep the master branch of your fork clean. Not push anything to it.

[Thomas Murrills]

Shreyas Srinivas said:

you don’t have to do much. Just go to your fork on GitHub and if it is behind the main repository, GitHub will point that out and suggest that you sync fork

Which it almost always will be, so if I wasn’t pointed to gh in this thread, I’d be opening a browser window all the time now, right?

[Shreyas Srinivas]

True. But I think the web interface is safer for anyone who doesn’t want to get deep into git technicalities

[Jireh Loreaux]

gh is relatively user friendly. It's the porcelain's porcelain.

[Thomas Murrills]

I’m hoping we can come up with a smoother interface for mathematicians than either “always go to github.com” or “learn git technicalities” :) I’m betting that there’s a simple set of instructions and commands to be aware of that would make this smooth for most people, and which could be written down somewhere.

[Jireh Loreaux]

personally, I disagree with this. I've been advocating to mathematicians for years before I ever started using Lean that they should be writing their LaTeX papers using git (or some other version control).

[Damiano Testa]

I like gh, it works well.

[Damiano Testa]

In terms of not modifying master of your own fork, I think that is also important. In fact, you can set up git-hooks that warn/prevent you from directly committing changes to master.

[Thomas Murrills]

Jireh Loreaux said:

gh is relatively user friendly. It's the porcelain's porcelain.

I’m sure you’re right, but I wouldn’t be using it if I weren’t pointed to it in this thread as a thing which has these capabilities (how would I know?), and so would probably be causing myself a lot more friction regularly than necessary. :)

[Robin Carlier]

"Mathematicians can learn complicated math, they can learn git"

[Joscha Mennicken]

Another fairly user-friendly UI-based alternative might be GitHub Desktop

[Thomas Murrills]

Jireh Loreaux said:

personally, I disagree with this. I've been advocating to mathematicians for years before I ever started using Lean that they should be writing their LaTeX papers using git (or some other version control).

I just don’t think “you should also learn git technicalities beyond the pull/push/etc. basics” ought to be another hurdle in the way of contributing to Mathlib.

[Thomas Murrills]

Also, I just want to be clear; surely you don’t also disagree with writing useful instructions down somewhere, right?

[Jireh Loreaux]

Thomas, what other technicalities are you talking about? You just git pull upstream master, git switch -c my_new_branch, git add files, git commit, git push origin my_new_branch. (where upstream = leanprover-community/mathlib4 and origin = user/mathlib4)

[Aaron Liu]

Damiano Testa said:

In terms of not modifying master of your own fork, I think that is also important. In fact, you can set up git-hooks that warn/prevent you from directly committing changes to master.

I accidentally pushed to master on my own fork, had to rip it out with two rebases and a force-push.

[Jireh Loreaux]

Thomas Murrills said:

surely you don’t also disagree with writing useful instructions down somewhere, right?

Sure (I don't disagree), if necessary.

[Damiano Testa]

Aaron Liu said:

Damiano Testa said:

In terms of not modifying master of your own fork, I think that is also important. In fact, you can set up git-hooks that warn/prevent you from directly committing changes to master.

I accidentally pushed to master on my own fork, had to rip it out with two rebases and a force-push.

Right, I think that it should be almost the default that you should not be allowed to push to master -- ever!

[Aaron Liu]

I think it should not be made easy, but it should also not be made hard. There should be some safeguards that you can turn off.

[Thomas Murrills]

Jireh Loreaux said:

Thomas, what other technicalities are you talking about? You just git pull upstream master, git switch -c my_new_branch, git add files, git commit, git push origin my_new_branch. (where upstream = leanprover-community/mathlib4 and origin = user/mathlib4)

How does that accomplish the “sync fork” functionality of the GitHub web interface?

And look at the extra steps @Emily Riehl needed to take earlier in this thread to get set up (which I expect I might need to take as well, and will be referring to this thread as guidance for how to do so!)

[Yakov Pechersky]

Kim Morrison said:

Okay, if you see breadcrumbs appearing inappropriately in irrelevant places, please post a link!

Here's an example from #21736
image.png

This happened because the PR description for #21738 mentioned "In #21736 ...". The PR description becomes the commit message of the squashed commit. This left a breadcrumb of "mathlib-bors (bot) pushed a commit that referenced this pull request".

Then, all other users merge master (likely fast-forward merge), which added the same commits to their fork, with the same message, also leaving breadcrumbs.

This wasn't so bad here, because first #21736 was merged, and then #21738 (and #25546, another example). But in my example above, one could imagine a currently in-progress PR 12345 that merged PR 9876 referenced like "Pulled results out of #12345". And then the conversation for #12345 will get N breadcrumbs in the middle, where N is the number of forks that are actively merging (ff) master.

[Yakov Pechersky]

I support a fork-PR workflow. I am trying to make people aware ahead of time of this communication obstacle that forks will place in our github views, which can make reviewing more cumbersome. Perhaps someone at Github knows how to turn off fork-breadcrumbs for conversations of a repo.

[Jireh Loreaux]

How does that accomplish the “sync fork” functionality of the GitHub web interface?

It doesn't technically sync your fork, but techinically it's not strictly necessary. You could sync the master branch on your fork with git pull upstream master, git push origin master if you're on master in your local repo.

You should think of it like this: there are three repos in play: upstream, origin, local. You can pull from upstream, but not push to it, only PR to it. So when you pull upstream master, you are syncing your local repository with upstream. Then you can push origin master to sync your origin to your local repo.

On GitHub, you have a button that allows you to do this in one go: upstream to origin (syncing your fork, this may pull other branches and tags, I'm not sure). Then gh also gives you access to some of these web features.

[Thomas Browning]

Jireh Loreaux said:

Thomas, what other technicalities are you talking about? You just git pull upstream master, git switch -c my_new_branch, git add files, git commit, git push origin my_new_branch. (where upstream = leanprover-community/mathlib4 and origin = user/mathlib4)

Just want to point out that to mathematicians unfamiliar with git, even this sequence of commands might seem completely mystifying and could be helpful to write down to lower the barrier to entry.

[Joscha Mennicken]

How important is keeping the fork's master up-to-date in the first place? Keeping your local master up-to-date with upstream seems sufficient, unless there's some sort of interaction with CI in forks?

[Robin Carlier]

I don't mind having a go at writing a "git for the formalizing mathematician" entry in the mathlib4 wiki but this might wait this weekend/start of next week.

[Thomas Murrills]

Joscha Mennicken said:

How important is keeping the fork's master up-to-date in the first place? Keeping your local master up-to-date with upstream seems sufficient, unless there's some sort of interaction with CI in forks?

I’m wondering this too; for example, does VS code allow you to look at the upstream master branch without switching repos, when you want to see how things work on master? Or is it now necessary to run a command to sync, whereas previously you could just click the down arrow to pull the new commits? (Not at my computer at the moment.)

(When on master, VS code also unhelpfully indicates that your local master is up to date with origin/master by default, which can give the false appearance that you’re synced up even when your origin is not synced to upstream; I could imagine this causing confusion.)

[Thomas Murrills]

I’m also not sure if upstreams are set up by default or not; I seem to remember having to do it myself with other forks? At the very least we’ve seen some nontrivial upstream-related setup earlier in this thread, so I expect there is guidance to give here…

[Jireh Loreaux]

You can git fetch remote to see what is on a remote without pulling it into your current branch.

[Thomas Murrills]

Can I switch to it in vs code the same way I can switch to other branches?

[Jireh Loreaux]

sure

[Thomas Murrills]

But, I have to run the command first? …Hang on, let me just get to my computer instead of asking. :)

[Jireh Loreaux]

Yes, you need to git fetch first, unless VS Code is doing auto-fetching for you.

[Yakov Pechersky]

Locally, you'll have master, upstream/master, and origin/master

[Yakov Pechersky]

VS code also unhelpfully indicates that your local master is up to date with origin/master by default

Yes, that's true, but Github view of your fork will display it. There's probably a fork-related VSCode plugin that can help show the difference between upstream and origin

[Thomas Murrills]

If there is, we should direct people to it! (I do want to emphasize that I’m not looking for solutions for myself, but trying to anticipate what might cause confusion among newcomers.)

Generally, when you don’t even know where to look to get the functionality you want, you can still get by—you just find worse ways to get things done at significant cost, often running into footguns along the way.

(E.g. for someone who wants to merge master: sync your fork on GitHub, fetch, pull the updated origin, then run git merge master—either because you don’t even know about upstreams in the first place or they’re not set up correctly.)

Imo we ought to prevent that as much as we can, and I’m surprised to meet resistance here! :) Ultimately, I think it’s very easy to ignore the simple barrier of unfamiliarity when you’re on the ‘familiar’ side of it…

[Robin Carlier]

Thomas Murrills said:

(When on master, VS code also unhelpfully indicates that your local master is up to date with origin/master by default, which can give the false appearance that you’re synced up even when your origin is not synced to upstream; I could imagine this causing confusion.)

Is the issue here that the local master branch tracks the origin/master branch instead of upstream/master?

[Yakov Pechersky]

That's right

[Thomas Murrills]

So, immediately, on a fresh fork, when I try to switch to upstream/master in VS code, I get the same fatal error as Emily Riehl (namely that a branch named master already exists).

[Thomas Murrills]

Riccardo Brasca said:

git branch --set-upstream-to=upstream/master

should work

Does that mean that everyone should run this when setting up?

[Robin Carlier]

The thing is not to switch to that branch, but to make the local one track the upstream one. The command Riccardo gave is supposed to achieve this.

[Robin Carlier]

It's probably a good idea to tell everyone to run a similar command.

[Thomas Murrills]

Ok, I see. Just curious, does the wording of that command mean that the “upstream” of my local master branch used to be origin/master (i.e. these are two different applications of the word “upstream”)?

[Robin Carlier]

Yes, I guess renaming the second remote to "upstream" is not the less confusing choice :sweat_smile:

[Robin Carlier]

One of them is "upstream" in the git sense, the second is "upstream" as in "the remote named upstream" and could have been "foo" if you renamed that remote "foo"

[Joscha Mennicken]

I wonder if a "repair" script would make sense that you can run in a mathlib git repo and that would set up or reset remotes to common, fixed names, configure tracking branches, create a fork if necessary; to move the repo to a recommended base state from which people can have a common workflow. The migration script already does something along those lines, but in a more limited and less robust way.

[Thomas Murrills]

That would be great, imo—plus ideally a bit of explanation somewhere as to how the resulting environment is now set up, so that you’re not blindly following commands and know where to look if you need more information.

(This is aligned with the sort of vibe I was going for in proposing a “standard” set of instructions for mathematicians—sensible defaults and a structure for a typical workflow, so that you’re not ad-hoccing your way through git in a possibly suboptimal way.)

[Joscha Mennicken]

It would also make slightly less common but useful settings available, e.g. master tracking upstream but with a branch.master.pushRemote = origin so that if you git pull, it pulls from upstream but if you git push, it pushes to origin.

[Joscha Mennicken]

On the other hand, collaborating with other people on their own forks while having your own fork will remain tricky and require you to have some idea of how git actually works.

[Yakov Pechersky]

Yes, that pushRemote suggestion is critical, because otherwise, you usually push to the branch that one tracks.

[Thomas Murrills]

Earlier it was suggested that you probably do not want to ever push to your own master branch; would preventing pushing to origin/master be possible? Or does that have issues?

[Thomas Murrills]

Or, wait—I suppose pushing to origin/master after pulling from upstream/master would just keep everything up to date.

[Thomas Murrills]

Maybe it’s that you do not ever want to commit to master yourself, or something like that?

[Joscha Mennicken]

Yes, a git pull && git push on master would just update origin/master. You could prevent local commits to master using a pre-commit hook, I believe.

[Sebastian Ullrich]

There is no need to ever touch origin/master or master. You can click on the branch name in VS Code, select "Create branch from...", and directly select upstream/master there.

[Thomas Murrills]

Often you want to quickly look at how things are working interactively on master, and if you try to switch to upstream/master, you get an error unless you’ve set the upstreams correctly. (You could just create a new branch each time you want to do this, but then you clutter things up with “junk branches”.)

I also think, just practically, that a lot of people will at some point or other choose the wrong master. If we can remove a demand of the form “just always do it this way”, I think we should.

[Thomas Murrills]

That said, I’m certainly in favor of guiding people to do this as something that could be convenient for them, just not in favor of never touching local master. :)

[Joscha Mennicken]

Thomas Murrills said:

if you try to switch to upstream/master, you get an error

Well, git switch upstream/master tells you to use --detach which works fine, but gets you into detached head state, which seems confusing for inexperienced users.

[Shreyas Srinivas]

You can usually name your remotes anything, including potato and tomato. The names “origin” and “upstream” are conventions. Usually if you fork a repository and work with a clone of the fork, your fork is the “origin” of your local repository. The original source repository of the fork is upstream.

[Shreyas Srinivas]

(This is in response to Thomas Murrills confusion about usage of upstream)

[Thomas Murrills]

Makes sense (brb, will be naming my upstreams “potato” now)—I was mostly surprised to learn that “upstream” apparently also describes a general relationship between repos/branches(?) in --set-upstream-to! :)

[Thomas Murrills]

Joscha Mennicken said:

On the other hand, collaborating with other people on their own forks while having your own fork will remain tricky and require you to have some idea of how git actually works.

On this note, I’m trying to think ahead and wonder if it will make more sense to have multiple cloned repos and so multiple VS code windows, or if there’s a good way to work on multiple repos in the same window by configuring the right remotes. (Mainly wondering whether the second option is even feasible.)

[Joscha Mennicken]

The workflow I'd expect for someone familiar with git is a single local repo with one remote per fork you are collaborating on, and one remote for the upstream repo. When pushing a branch, you specify the remote you want to push to, or you can set a per-branch default using git branch --set-upstream-to <remote>.

[Thomas Murrills]

Okay, I see! Ooh, the per-branch default is interesting. (I’m hoping that the VS code buttons will “listen” to that.) I feel a tiny script which sets things like this up might go a long way to making collaboration almost as smooth as it was before. :)

[Jireh Loreaux]

VS Code will definitely listen to it. All it does is read your git config file. Look inside the .git folder. It's pretty easy to understand.

[Riccardo Brasca]

I'am not following the whole discussion, but I think a guide for mathematicians is absolutely needed. It's important to understand that people had their mental model of how git/github worked, based on having used only for mathlib. So now there two completely new notions:

• fork (probably easy to explain)
• remote (this is trickier, since the mental model "my computer is a copy of the thing online, I only have to make sure the two are in sync" in no longer enough)

[Riccardo Brasca]

I guess that people are much happier to spend 5 minutes to update their mental model and understand what's going on than memorizing 5 commands (and forgetting them 3 days later)

[Thomas Murrills]

I agree that it’s useful and necessary to update the mental model! Maybe you’re considering this implicitly, I actually don’t anticipate that understanding the basic interplay between local/origin/upstream will be the only (or maybe even main) source of friction. (For example, I already knew, conceptually, what Jireh explained (much) earlier about origin/upstream/local repos and the interplay between them.)

The source of friction I’m concerned about is (1) not knowing fully what capabilities are present in which tools in the first place (2) therefore not knowing what capabilities I “should” be using to solve a given problem (since this relies on being aware of all capabilities). (Not knowing which precise commands to execute is indeed mostly a detail.)

That is, it’s the fact that unfamiliarity with the full space of things that can be done leads to not knowing what should be done in simple cases. (E.g. how do I update my copy? how do I work on someone else’s fork? is it possible for this branch to reflect that branch somehow? All of these have multiple reasonable attempts at answers from a newcomer, some of which are very inefficient, or lead to inscrutable errors, etc.)

When you’re familiar with tools, what they can and can’t do and how to hold them is so obvious that it seems the only problem is learning each actual use of them. I claim the issue is prior to usage per se, but comes after the mental model of the thing you’re using the tools on. It’s about having a sufficient mental model of the possible manipulations each tool makes available. (And maybe just as importantly, what they don’t.)

But instead of saying that everyone should learn the full scope of git’s power out of the gate, I think we can isolate the understanding-of-capabilities necessary for the simple cases encountered in typical workflows from people who are very familiar with git (as in this thread! :) ), and then provide that to newcomers somehow.

(Note: I’m in favor of both automating things and explaining to people what was automated, so that understanding is actually gained!)

[Alex Meiburg]

I would say there are enough different conventions that exist that, when googling for tips on how to do things in git(hub), I've definitely frequently been lead astray and made things worse. When the philosophy is "these are the four commands you run", then as soon as you diverge from that recipe, it becomes a mess.

(And it does happen that you'll need to diverge from the simplest recipe ... like, you saved+committed your files on the wrong branch. Or you need to merge some nontrivial conflicts.)

For instance: Some orgs/companies expect everyone to merge master. Some expect rebasing and never merge. Some have policies that commits must be squashed. Someone wants to PR your branch, or you need to pull in someone else's branch from their cloned repo to build on their stuff for the new feature you're doing. Plenty of guides will say "just copy+paste this" but no one can agree if it's main or master.

There are many many ways for things to go off the rails!

[Alex Meiburg]

Never mind issues where people give gh commands to run but they write git, or other outright errors

[Thomas Murrills]

Good point! I don’t know if you were implying I was advocating for a “these are the four commands you run” philosophy, but either way, I do agree with that criticism of it!

To make my approach more explicit (and distinct): I’m advocating for giving mathematicians working on Mathlib some starting state where things have been set up nicely (and ideally an understanding of that state), plus the awareness of capabilities that are probably relevant to them. (And by “awareness of capabilities”, I don’t just mean “run this when this”, but communicating “you can change your situation from this (which works this way) to that (which works that way)”)

We can then at least avoid people starting out by googling those sorts of maybe-not-useful tips to solve their problems that might get them in difficult situations from the get-go (and hopefully the basic understanding provided gives them a springboard to figuring out the inevitable issues you mention, instead of leaving them adrift).

[Thomas Murrills]

Here’s an example that clarifies the place I’m coming from re: awareness of capabilities:

Let’s say I tell a newcomer “run git branch --set-upstream-to=upstream”. I may think I’m just telling them “how to use git to set upstreams”, but really (ideally, with a bit more explanation), I’m also telling them

1. that there even exists a state where master “tracks” upstream (and possibly the concept of tracking)
2. that git is a tool which can get you to that state

and implicitly

3. that this is an appropriate solution to the problem at hand, which satisfies nice properties and will probably not break in unexpected ways

none of which they knew before, and all of which are what’s really important to them.

This is the information I think it’s important for newcomers to know; otherwise the ocean of possibilities is overwhelming, and the newcomer will potentially hack together a path to a different state which achieves their goals, but in a brittle and inconvenient manner.

[Jz Pan]

Well, my personal setup completely eliminated upstream on my local computer, and there is only origin which points to my fork of mathlib. The sync of my fork with the actual mathlib is completely done by github web interface "sync fork" button.

IMHO this gives less confusions, since the local workflow is completely unchanged (and no mental models needs to be updated).

[Kim Morrison]

Thomas Murrills said:

How does that accomplish the “sync fork” functionality of the GitHub web interface?

@Thomas Murrills, the point is that you don't ever need to "sync fork". That's simply a red herring. Don't do it unless you want to!

(Sorry, replying while mid-thread, this may have already been addressed.)

[Ching-Tsun Chou]

Why not just have a cheatsheet so that those who do not want to think about these issues can just follow instructions? If nonstandard issues arise, one can always ask questions on Zulip.

[Thomas Murrills]

Jz Pan said:

Well, my personal setup completely eliminated upstream on my local computer, and there is only origin which points to my fork of mathlib. The sync of my fork with the actual mathlib is completely done by github web interface "sync fork" button.

IMHO this gives less confusions, since the local workflow is completely unchanged (and no mental models needs to be updated).

I think your response to this new situation is perfectly reasonable, and is exactly the sort of thing I'm worried about! :) This is how I approached a fork model too at first, and I can guarantee it's how many others will as well: we know how to click "sync fork", we understand the basics of what a fork is vs. the original repo and the local copy, and we'll default to leveraging that knowledge as quickly as possible. But doing this means opening a browser window, navigating to your fork, and clicking that button each time you want to merge or view master, when things could be smoother.

The fact that the prevailing advice here (from those familiar with the tools) is actually "don't bother clicking sync fork" is a great example of the gap I'm pointing out.

A lot of people (including myself) will simply set things up in a way that uses the tools immediately available to them, like a "sync fork" button, even if it involves more friction than something they don't know about yet—because unless your goal is to learn git, you're just going to reach for what you already know. Without guidance or support to the contrary, this course of action actually makes sense in the short term, when beelining for what you're actually here for. But with guidance and support for smoothing things out, we can give people a better experience.

[Nailin Guan]

I have a a problem that might be a bit silly: when trying to run scripts/migrate_to_fork.py
First, there is this error : UnicodeDecodeError: 'gbk' codec can't decode byte 0x93 in position 15: illegal multibyte sequence
Then it show

✗ GitHub CLI token lacks required 'repo' scope.
Please re-authenticate with required scopes:
  gh auth login --scopes 'repo,workflow'

I run gh auth login --scopes 'repo,workflow but it still show this error. Can anyone help?

[Joscha Mennicken]

UnicodeDecodeError is a Python error, but gh is written in go, so this seems like an error in migrate_to_fork.py. Can you share the full error traceback including the line numbers? Also, this should probably be in #mathlib4 > Feedback on scripts/migrate_to_fork.py

[Kevin Buzzard]

Note the update at #announce > Mathlib PRs should be made from a fork @ 💬

[Jeremy Ravenel]

There were recent complaints about how the maintainers of Mathlib handle objections from people making PRs and also a resignation letter.

The previous policy featured master branch privledges and this policy does not feature master branch privledges.

[Kevin Buzzard]

Just to be clear -- Chris Hughes' resignation occurred a long time ago and the fact that a discussion has resurfaced about it now is completely unrelated to the discussion about changing the PR workflow.

There was also a complaint about the PR workflow change from David Loeffler (in the form of an open letter to the maintainers) and the script doing the updates (which he had been frustrated by) now is hopefully fixed. The issue was branches with names which only differed in capitalization and was OS-specific; we had not caught it in testing. If you are still having problems then please update mathlib and they should be fixed.

Yes, the previous policy featured master branch privileges which are now being removed so that we conform to the usual github workflow.

[Jeremy Ravenel]

Thanks for clarifying for me.

[Artie Khovanov]

The migration tool worked perfectly for me, instructions were very clear

[Arthur Paulino]

This is a great move! It's not only more secure but it also scales much better :clap:

(maybe it scales better because it's more secure)

[Weiyi Wang]

what are "master branch privileges"?

[Shreyas Srinivas]

Kevin Buzzard said:

There was also a complaint about the PR workflow change from David Loeffler (in the form of an open letter to the maintainers) and the script doing the updates (which he had been frustrated by) now is hopefully fixed. The issue was branches with names which only differed in capitalization and was OS-specific; we had not caught it in testing. If you are still having problems then please update mathlib and they should be fixed.

As I recall, the issue was also about

1. The suddenness of the change, instead of a gradual transition to allow people to learn and adapt the new workflow.
2. The sparse instructions surrounding git and github workflows which break the mental model of git that mathlib-only users of git had.

EDIT: Both these appear to have been addresssed to the best possible extent.

[Shreyas Srinivas]

Weiyi Wang said:

what are "master branch privileges"?

It's a slightly incorrect way of describing the situation where contributors were being given write privileges to non-master branches of mathlib. Only maintainers have ever been able to write to the master branch for as long as I can remember.

[David Ang]

Hi all, is there a list of instructions to follow for scripts/migrate_to_fork.py? I'm just blindly running the script and ran into this error

[Robin Carlier]

there has to be something funny in the fact that this problem seems to be because of emojis.

[Robin Carlier]

Can you try editing the script on your end, removing every emojis, and try again?

[Julian Berman]

You probably also could try setting PYTHONUTF8=1 and seeing if that works without editing.

[David Ang]

How do you add that setting?

[Julian Berman]

Are you in powershell or some unix-y (WSL?) shell

[David Ang]

I'm in Git Bash

[Julian Berman]

If the latter, run PYTHONUTF8=1 python scripts/migrate_to_fork.py. If the former, I think set is the powershell command

[Julian Berman]

OK yeah try just adding it to the front

[David Ang]

Julian Berman said:

OK yeah try just adding it to the front

Thanks, this works! Now I have another error - and after restarting the terminal it tells me it doesn't have pseudo terminal support? I'm happy to use powershell as well but I don't know what you mean by set being the command

[David Ang]

Seems like powershell is happy with the emojis...

[Weiyi Wang]

as a software developer I generally get better unicode support from powershell than git bash (mingw). Perhaps we should add this note to the guide?

[David Ang]

It seems like the script has done a bunch of stuff, but my PRs are still there and nothing is migrated

[David Ang]

Weiyi Wang said:

as a software developer I generally get better unicode support from powershell than git bash (mingw). Perhaps we should add this note to the guide?

Could you give me a link to the guide? I've been trying to find it.

[Joscha Mennicken]

There's this guide, but it's not been merged yet: https://github.com/leanprover-community/leanprover-community.github.io/pull/643

[David Ang]

I'm still unsure what I need to do to get my PRs migrated after running the script :(

[Robin Carlier]

David, did you manage to get the gh auth login to work? the script can’t do anything without that.

[David Ang]

Robin Carlier said:

David, did you manage to get the gh auth login to work? the script can’t do anything without that.

Yes, powershell goes through that but Git Bash doesn't

[David Ang]

This is the output (after step 4, I think)

[Robin Carlier]

My guess is that this is the output of the git fetch --prune? normally, the script continues many more steps, it’s weird that it stops right after step 4... Can you show what git remote -v gives you?

[David Ang]

Robin Carlier said:

My guess is that this is the output of the git fetch --prune? normally, the script continues many more steps, it’s weird that it stops right after step 4... Can you show what git remote -v gives you?

I changed remote manually to my own fork before running the script, so git remote -v gives me the links to my fork (both fetch and push)

[David Ang]

I don't actually know if this is step 4, because step 4 is the last thing I see before the entire page gets congested with this output

[Robin Carlier]

but do you have leanprover-community/mathlib4 as a remote named upstream?

[David Ang]

I guess not?

[Robin Carlier]

ok, that might be the issue. Can you run git remote add upstream "https://github.com/leanprover-community/mathlib4.git"?

[Robin Carlier]

once it’s done, you might want to try running git fetch --all --prune before running the script, the script does it but let’s be extra extra sure.

[David Ang]

Robin Carlier said:

once it’s done, you might want to try running git fetch --all --prune before running the script, the script does it but let’s be extra extra sure.

It could not fetch origin?

[Robin Carlier]

git fetch upstream --prune?

[David Ang]

Robin Carlier said:

git fetch upstream --prune?

This doesn't seem to do anything, and running the script after this gives the same error that it could not fetch origin

[David Ang]

I don't quite understand why we're pruning things from origin/upstream? I thought we're trying to move PRs

[Robin Carlier]

The pruning has to do with the fact that some branches had name differing only by case that were causing trouble down the line, so this was added as a step in the script to make sure these bad branches (now deleted in the main repo) do not appear. But I’m confused as to why it doesn’t let you fetch from your fork...
As a last resort, you can try deleting line 331 (that fetch step) in the script and try.

[David Ang]

Right, that now moves me to the next step, and it tells me I have to move to individual branches to migrate them manually? Can this not be done from master?

[David Ang]

In particular I have really old branches that won't play well if I try to merge master to get script/migration_to_fork.py...

[Robin Carlier]

No, for each PR you want to migrate, you need to switch to the branch and run the script.
I guess you can copy-paste only the script in old branches.

[David Ang]

Seems like that works for at least one PR! Thanks! I'll try to do my remaining PRs and report back if anything goes awry...

[David Ang]

Note that the PR labels seem to have disappeared :(

[Robin Carlier]

I’m still a bit concerned that you can’t fetch from your fork, because at some point you’ll definitely need to do that.

[David Ang]

Yeah, I have to manually erase that line for the script to work...

[Shreyas Srinivas]

You might have a better experience with the windows terminal. I think you can also open a git bash terminal inside it, although it has been over a year since I tried anything lean related on windows (about the Unicode error)

[Robin Carlier]

And you’ll need to fetch not necessarily in the migration but in everyday workflow, if e.g you accept a suggestion made via github UI in one of your PR, and want to code on top of that, or if you collaborate with someone pushing on one of your branches.

Perhaps at this point if you don’t have too many local only branches it could be worth trying re-setting up your local repo from scratch?
I tried adding your fork as a remote and fetching and it works, so there has to be something wrong in your local repo.

[David Ang]

I have a bit too many local only branches, unfortunately.

Note that I've also lost all PR comments, but maybe that's expected to happen.

[Michael Rothgang]

David Ang said:

I have a bit too many local only branches, unfortunately.

Note that I've also lost all PR comments, but maybe that's expected to happen.

IIUC, newer versions of the script preserve these. In other words: make sure your master branch is up to date before running the script, to get the latest bug-fixes.

[David Ang]

Michael Rothgang said:

David Ang said:

I have a bit too many local only branches, unfortunately.

Note that I've also lost all PR comments, but maybe that's expected to happen.

IIUC, newer versions of the script preserve these. In other words: make sure your master branch is up to date before running the script, to get the latest bug-fixes.

I am up-to-date with master; the comments seem to have been squished into one comment! I didn't notice that at the start...

[Kim Morrison]

Yes, the squishing of comments is expected behaviour. There's no way to copy comments preserving the authorship.

[Eric Wieser]

(at least, not without using "GitHub Enterprise importer", which is what Python used to copy issue comments from bpo to GitHub)

[Wrenna Robson]

Think I have finished my migration.

[Wrenna Robson]

(deleted)

[Julian Berman]

Eric Wieser said:

(at least, not without using "GitHub Enterprise importer", which is what Python used to copy issue comments from bpo to GitHub)

Even that isn't perfect of course, all my comments on bpo got imported and I even happen to have the same username on both bpo and GitHub, but the comments on GitHub have this weird phantom Julian as the username on the comment and clicking on the username takes you to nowhere. (The reason is almost certainly due to email mismatch and if I added my old bpo email to my GitHub profile maybe things would work. Or maybe not. Copying is hard!)

[Matthias Köppe]

Julian Berman said:

the comments on GitHub have this weird phantom Julian as the username on the comment and clicking on the username takes you to nowhere.

These placeholders are called mannequin accounts in GitHub parlance, and they can be reclaimed by actual users (with the help of the repo owners), see https://docs.github.com/en/migrations/using-github-enterprise-importer/completing-your-migration-with-github-enterprise-importer/reclaiming-mannequins-for-github-enterprise-importer

[Matthias Köppe]

Eric Wieser said:

(at least, not without using "GitHub Enterprise importer", which is what Python used to copy issue comments from bpo to GitHub)

Yes, either that or a contact at GitHub who runs the import of the migration archives for you. The folks at the GItHub open source program were most helpful in doing that when we migrated SageMath development to GitHub in 2022–23.

[Eric Wieser]

My guess is that GitHub cares much more about helping projects transition to GitHub than within GitHub

[Bryan Gin-ge Chen]

I'm going to have dinner and then do some final editing of (a guide to git for new contributors) https://github.com/leanprover-community/leanprover-community.github.io/pull/643 and then merge; if anyone has any last-minute comments, please leave a review in the next ~3 hours or so!

[Bryan Gin-ge Chen]

Thanks everyone for the additional comments! The guide to git for new contributors is now live here and is linked to from the website sidebar, as well as from the previous "pull request lifecycle" page.

I tried to incorporate the remaining suggestions while I did some reorganization / editing of my own, and I've no doubt missed some issues and introduced new errors. I'd appreciate if folks could read through the pages and comment here or open PRs to fix / improve them!

[Sébastien Gouëzel]

Do we really want the line git fetch upstream? There are a zillion of branches upstream, not sure it's worth fetching them all.

[Johan Commelin]

Maybe git fetch upstream master is enough?

[Markus Himmel]

The git pull in the "Keep Your Master Branch Up to Date" step will also fetch all branches of upstream, so if the git fetch is changed to git fetch upstream master, then we should also change from git pull to git pull upstream master.

[Kim Morrison]

My preference is to keep things simple in the instructions, even if that means git is doing more work (e.g. pulling zillions of branches).

[Johan Commelin]

Fair enough

[Joscha Mennicken]

Looking at the instructions, I think there are a few more places where gh can be used instead of the manual commands. For example, instead of forking via the web ui and then cloning using gh repo clone ..., you can just run gh repo fork leanprover-community/mathlib4 --clone --default-branch-only. It will create a fork if there is none, or use an existing fork if present, and then clone the fork, setting up upstream and origin as expected. Also, I believe you can run gh repo fork ... inside an existing git repo instead of doing step 3 option B manually.

[Bryan Gin-ge Chen]

A PR adding more uses of gh would be appreciated!

[Anthony Fernandes]

An other way to avoid fetching the entire mathlib repo would be to change step 3.A.2 to git remote add -t master upstream https://github.com/leanprover-community/mathlib4.git. This way everyday commands remain the same (i.e. simply git pull/git fetch upstream), however gh don't seems to be able to setup this with gh repo clone so it requires one more step for people choosing step 2.A.1

[Filippo A. E. Nuccio]

Bryan Gin-ge Chen said:

A PR adding more uses of gh would be appreciated!

But installing gh for windows is not completely obvious.

[Yaël Dillies]

@Artie Khovanov seems to have lost privileges to run !bench (cf #26123). Is this expected?

[Joscha Mennicken]

I believe at the moment you need write permissions to use !bench. Maybe bench-after-CI can be used as a workaround? (For future reference, the GitHub API endpoint used to determine permissions)

[Artie Khovanov]

@Joscha Mennicken please could you say a bit more about the workaround? I'm afraid I don't understand. Is !bench-after-CI a command?

[Joscha Mennicken]

There is a bench-after-CI label that causes some bot to trigger the !bench command after CI succeeds, and I assume the bot still has the required permissions for the bench command. I'm not sure though what happens when the label is added while CI is already green.

[Bryan Gin-ge Chen]

Filippo A. E. Nuccio said:

Bryan Gin-ge Chen said:

A PR adding more uses of gh would be appreciated!

But installing gh for windows is not completely obvious.

I wasn't aware of this! Are the instructions on the gh website that we link to not sufficient? (I have a windows machine but I haven't attempted to make PRs to mathlib4 from it yet so I could try some testing, but probably not in the next few days)

[Filippo A. E. Nuccio]

Bryan Gin-ge Chen said:

Filippo A. E. Nuccio said:

Bryan Gin-ge Chen said:

A PR adding more uses of gh would be appreciated!

But installing gh for windows is not completely obvious.

I wasn't aware of this! Are the instructions on the gh website that we link to not sufficient? (I have a windows machine but I haven't attempted to make PRs to mathlib4 from it yet so I could try some testing, but probably not in the next few days)

Well, let's say that they are OK for people willing to open terminal on Win, and they are not that many.

[Bryan Gin-ge Chen]

I see. Unfortunately the entire guide assumes that users are willing to open the terminal. If there is something reasonable to link to get people started with the terminal that might be good to put in at the start of the guide.

[Artie Khovanov]

@Joscha Mennicken just tried, didn't work :frown:
#26162 (could a maintainer run bench? :pleading:)

[Kyle Miller]

I haven't been able to bench anything either -- I think the speed center is down right now :-(

[Joscha Mennicken]

The speed center only allows !bench for contributors with write access, so it makes sense that it stopped working after the fork migration.

[Artie Khovanov]

OK well I guess my PRs are blocked on this lol

[Kyle Miller]

@Joscha Mennicken I have write access

[Kyle Miller]

Oh, no, apparently I don't. Edit: I do. There are too many places to look to see if you have write access...

[Joscha Mennicken]

The bot uses the permission field of gh api repos/leanprover-community/mathlib4/collaborators/<your username>/permission, which isn't as granular as the actual permissions.

[Kyle Miller]

Thanks, I have admin, so it ought to work.

[Joscha Mennicken]

In that case, I have absolutely no idea.

[Joscha Mennicken]

Oh, maybe the bench bot itself no longer has the required permissions to check for other people's permissions? :D

[Artie Khovanov]

The bench bot works now. Manual command still doesn't. Bit silly but workable!

[Raghuram]

Posting here because I'm guessing it's related.

Running lake exe cache get in a lake project created today results in the following warning:

Warning: Some Mathlib ecosystem tools assume that the git remote for leanprover-community/mathlib4 is named upstream. You have named it origin instead. We recommend changing the name to upstream. Moreover, origin should point to your own fork of the mathlib4 repository. You can set this up with git remote add upstream https://github.com/leanprover-community/mathlib4.git.

git remote -v in .lake/packages/mathlib shows

origin  https://github.com/leanprover-community/mathlib4 (fetch)
origin  https://github.com/leanprover-community/mathlib4 (push)

so I'm guessing this is because lake update clones mathlib with the default remote name origin and some other part of lake or mathlib, which was written for the migration to forking, notices this and complains.

[Alex Meiburg]

I get the following error:

=== Step 4: Setting up git remotes ===
✓ Upstream remote already configured correctly
✓ Origin remote (fork) already configured correctly

Current branch:

=== Step 5: Pushing branch '' to fork ===
✗ Command failed: git push -u origin
✗ Error: fatal: invalid refspec ''

The first branch I ran this with ran fine. The second one, didn't.

[Alex Meiburg]

Never mind, I got it to work. git checkout [branch name] didn't work for this branch, I needed the git checkout --track [branch name].

It seems to be (sample size: 4) that the additional --track option is needed iff the branch name has a / character in it.

[Thomas Murrills]

I noticed that in my git config, VS code has inserted

branch.master.vscode-merge-base=origin/master

If I'm trying to ignore origin/master as per the instructions, do I want this? Or do I want ...=upstream/master? I'm having trouble finding documentation for what exactly it means.

[Johan Commelin]

I don't know exactly what that setting does, but upstream/master would be my guess, yes

[Chris Birkbeck]

So I'm having trouble with my PR #26006 which was made using the script. Its saying merge conflict, but I ran git merge origin/master (after pulling master) and it never gave me the "resolve merge issues" thing where I can fix the merge problems. I must be doing something wrong, but I can't seem to figure it out.

[Chris Birkbeck]

I also did the sync fork thing on my fork of mathlib, but that also didnt seem to fix the problem.

[Weiyi Wang]

I assume origin is your fork and upstream is the main repo (which are what the script recommends), could you try git fetch upstream then git merge upstream/master?

[Chris Birkbeck]

so it says:

git merge upstream/master
Already up to date.

[Aaron Liu]

Are you on the right branch?

[Chris Birkbeck]

oh but now when I ran get merge origin/master it now gave me the merge conflicts to fix, so that did work I guess

[Chris Birkbeck]

thanks!

[Chris Birkbeck]

Aaron Liu said:

Are you on the right branch?

I think I was...

[Ruben Van de Velde]

Something seems to have worked, yeah :)

[Joscha Mennicken]

This may have been caused by out-of-date remotes (upstream/origin). When in doubt, just run git fetch --all to update all remotes.

[Chris Birkbeck]

it might be worth adding some instructions about this to: https://leanprover-community.github.io/contribute/git.html in case others get these merge issues. Since it doesn't mention get merge origin/master which I don't know I would know (and fail) to do unless I'd done it before.

[Weiyi Wang]

A random observation: #25739 says CI is "2 workflows awaiting approval". Would this happen to all future new contributors from a fork, and requires maintainers to click some buttons?

[Ruben Van de Velde]

Looks like I have that power, so I clicked the button

[Weiyi Wang]

Thanks! I think thin will be a reoccurring thing, as I saw this in #26518 again. I think github will always ask maintainer for approval when running CI against new contributor's PR from fork (so nobody can just PR a bitcoin miner and get it running in our CI), but similar to how people needed to ask for permission, now they need to ask for the approval

[Bryan Gin-ge Chen]

For what it's worth, the "main" CI jobs do not require approval; I think the only jobs that require approval are mostly jobs for automatically labeling the PR or making automatic style suggestions.

[Weiyi Wang]

That's interesting... what makes them different?

[Bryan Gin-ge Chen]

I think the workflows triggered on the pull_request event require maintainer permission. (There may be some others as well)

[Emily Riehl]

A few months ago I ran the script mentioned above on my laptop to migrate my open PRs to a fork. Now I'm back on my office desktop and I realized I was trying to work with local copies of an old (pre-migration) PR, which explained why all the recent commit history was missing!

So I've just:
(i) deleted my local copy of mathlib4
(ii) replaced it with a clone of my mathlib4 fork
(iii) ran git branch --set-upstream-to=upstream/master which I think means my master branch will track the original mathlib master branch; I know I'm not supposed to edit my fork's master branch

But now when I try to checkout my PR, I get an error:

eriehl@mather-mstu-m2 mathlib4 % gh pr checkout 25780
GraphQL: Could not resolve to a PullRequest with the number of 25780. (repository.pullRequest)

Have I set this up incorrectly?

[Joscha Mennicken]

Did you maybe miss the step where you add the original mathlib4 repo as remote named upstream? git remote add upstream https://github.com/leanprover-community/mathlib4.git

[Robin Carlier]

Probably that gh is configured to follow the repository to be your fork and not the main repo, so it's looking at pr #25780 on your fork which of course does not exist
Can you run gh repo set-default leanprover-community/mathlib4 and then try again?

[Joscha Mennicken]

You could also try running ./scripts/githelper.py fix (or python scripts/githelper.py fix), which should (re-)set your repo to a known-good state. I'd be curious if it works correctly.

[Emily Riehl]

@Joscha Mennicken this gave me:

Step 5: Check remotes of branch 'master'.
WARNING: Branch 'master' should have pushRemote 'origin'.
Update pushRemote of 'master'? [Y/n]:

How should I respond?

[Joscha Mennicken]

Either is fine. Use n if you want to keep your repo as-is.

[Emily Riehl]

After implementing @Robin Carlier's suggestion I was able to pull the PR. But now I have no idea whether I've set anything up correctly or not.

[Emily Riehl]

I'm never going to push anything from master, is that the reason why it doesn't matter?

[Joscha Mennicken]

Yes. With the setup suggested by the script, any pushes to master would push to your fork, even though pulls would still fetch from the original mathlib4. This setup might be more confusing than useful.

[Emily Riehl]

Okay, thanks for the help both of you.

[Joscha Mennicken]

Now I'm left wondering if the script would've fixed it all by itself (which is the reason it exists in the first place). I guess I thought of it too late :D

[Emily Riehl]

I maybe should have tried that? I never quite understood what the script was for. In any case, since I'd already moved my PRs, it didn't occur to me to try.

[Joscha Mennicken]

The githelper fix command is meant for cases just like this, where a git repo may be set up incorrectly and you want to fix it in-place.

[Bryan Gin-ge Chen]

(I think we still need to add something about the githelper script to the instructions on our website.)

[Emily Riehl]

Good idea. This is the first I'm hearing about that script which indeed sounds very useful!

[Emily Riehl]

I'm having a new issue and I'm wondering if it's related. I'm trying to add a new import to a file in the PR I just mentioned and I'm getting an error

object file '/Users/eriehl/Math/Formalization/mathlib4/.lake/build/lib/lean/Mathlib/CategoryTheory/Category/Cat/CartesianClosed.olean' of module Mathlib.CategoryTheory.Category.Cat.CartesianClosed does not exist

This file is in mathlib so is it an issue with my local set up?

[Aaron Liu]

try reloading everything

[Emily Riehl]

A partial rebuild eventually fixed it. Thanks.