Open letter to maintainers

Stream: mathlib4

[David Loeffler]

Dear Mathlib maintainers:

I would like to register a protest about how this "PRs from forks" business has been handled.

• As far as I'm aware, there was no discussion with the community ahead of time, nor any attempt to make a case to the community about why this decision was in everyone's best interests; just a sudden point-blank order "you will now do X".
• There was no clear guidance or documentation given about how the new PR workflow is supposed to work. As others have pointed out, for many Mathlib contributors (such as myself), Mathlib is the only GitHub project they have experience of contributing to; so "we're switching to something closer to the usual github workflow" conveys no information at all.
• The PR migration script appears not to have been sufficiently tested; multiple users have reported problems with it (and these appear to be multiple different problems, not just multiple reports of the same issue).
• The announcement was very unclear about the time-frame for removing write access to existing PRs. One of the maintainers expressed surprise that the discussion thread had jumped from "new PR's should be made from forks" to "existing PR's should be migrated to forks"; but when the maintainers have posted in the announcement thread that "we will be removing write access to the repository from most users", without any indication of the timeframe, what else did you expect to happen? (If you had written something like "we will start removing write access in a month's time" or whatever, it would have been much less disruptive.)
• I haven't yet managed to get the PR migration script to work, so I'm not sure what it's supposed to be doing; but from what I can glean from its source code, it looks like it doesn't copy across the comment history on PR's. If so, the loss of the history of previous review comments, and the changes that are made in response, will make it needlessly harder for migrated PR's to be reviewed.

I feel this has been a regrettable departure from the normally very harmonious way that the mathlib community is run, and I hope it is not a sign of how things will be in the future.

Yours, David Loeffler

[Kenny Lau]

I agree with the points that don't have to do with the migration script. (mainly because I've not yet run the script)

[Kim Morrison]

Thanks for your appreciation for the huge work that this took (both by volunteers, and by paid employees of the FRO supporting Mathlib), even if you can't understand at this point why this change was essential and urgent. :-)

The suggestion to try copying the comment history across is a reasonable one. Does anyone have capacity to attempt that? Obviously it couldn't be done on a comment-by-comment basis, but perhaps a single comment containing a "dialogue" version of the comments could be constructed.

[Kim Morrison]

#25892 attempts to copy comments across while migrating PRs.

[Kim Morrison]

#25890 improves windows compatibility

[Kim Morrison]

If some non-git experts could suggest changes or improvements to https://github.com/leanprover-community/leanprover-community.github.io/pull/643, that would be very helpful. We will link to this page from the community homepage, as well as create a #git linkifier.

[Michael Rothgang]

This answers all gut questions I had about git workflows in the new model. Thanks for writing this!

[Filippo A. E. Nuccio]

I find that guide to be very much linux oriented (in particular, almost everything is done from the command line). I would suggest something for Win users, but where? Separate file, below that one, other?

[Robin Carlier]

I was also thinking of writing a similar guide, more geared towars explaining the basics of what git is, git vocabulary (branch, commit, remotes, etc.) rather than "the list of commands to run", and I was thinking it could be part of the GitHub matlib "wiki" section. Would that still be welcome even if @Kim Morrison's guide makes it to the website?

[Kim Morrison]

Yes! Very welcome on either the wiki (we can link to it from the community website), or just as a section on the file I wrote.

[David Loeffler]

Definitely room for both IMHO

[Kim Morrison]

Filippo A. E. Nuccio said:

I find that guide to be very much linux oriented (in particular, almost everything is done from the command line). I would suggest something for Win users, but where? Separate file, below that one, other?

The problem here is that once you say you don't want command line instructions, you are committed to using some particular GUI, and there are a million choices, and the instructions will be different for each.

[Kim Morrison]

If someone can just pick one, I will write instructions for it.

[David Loeffler]

I'm afraid there isn't just a single command-line interface in the world either.

[Kevin Buzzard]

But they're much more similar than the gui ecosystem!

[Chris Birkbeck]

Kim Morrison said:

If someone can just pick one, I will write instructions for it.

GitHub desktop? I find it quite useful and know other people in the Lean community also use this. But have no idea if it's the most popular, but feels like the most official one to me at least (and it's on both Mac and PC).

[David Loeffler]

(Sorry, my remark came without context, it was intended to be read as a follow-up to an observation I just posted on the "git guide" pull-request pointing out that it included chunks of shell code written in bash that would likely not work under either zsh or the Windows shell.)

[Robin Carlier]

It’s been ages since I last used VSCode, but it has a basic git interface iirc? If we’re focusing on people "just following the instructions" perhaps we could assume VSCode as an editor and focus the "gui"-oriented stuff with VSCode GUI?

[David Loeffler]

Kim Morrison said:

The problem here is that once you say you don't want command line instructions, you are committed to using some particular GUI, and there are a million choices, and the instructions will be different for each.

This is why I think Robin Carlier's earlier proposal is important: rather than focussing exclusively on one particular interface, to prioritize explaining the mental model – what steps need to be done in what order and the vocabularity that is used to describe them. Then users can refer to the docs of whatever interface they prefer in order to find out how to execute those steps.

[Filippo A. E. Nuccio]

But I think we're missing the point of what to do with a fellow mathematician who has never written a single command line. Should they change their habit even before trying opening a single PR?

[David Loeffler]

I'd advocate for offering instructions using the built-in Git client in VSCode.

[David Loeffler]

Kim Morrison said:

#25892 attempts to copy comments across while migrating PRs.

I have posted some feedback on this in the other thread (#mathlib4 > Feedback on scripts/migrate_to_fork.py )

[Marc Huisinga]

FWIW, I find the UI of GitHub Desktop to be much more intuitive than the UI of the Git integration built into VS Code for all basic Git operations, so if you are looking for something that is both easy to use and nicely integrated with GitHub, it's GitHub Desktop. I find the VS Code one to be pretty painful to use.
The main limitation of GitHub Desktop is that it won't work for you if you aren't working locally, e.g. in something like Gitpod.

However, there are a couple of operations that I still find myself reaching to the command line for, most of which is caused by preferring rebasing over merging (so your experience might vary if you prefer merging):

1. Hard-resetting to a remote branch when there was a force-push on the remote branch by someone else.
2. Using rebase --onto when I have a PR that is based on another PR that was now merged, and I want to move the changes of the stacked PR to be based on master.
3. Managing more remotes than upstream and origin (I don't need to do this often).

1 and 2 are limitations of the VS Code integration as well, while 3 isn't. The VS Code integration has some other limitations, though, like not being able to squash commits. Some of these limitations can probably be lifted with extra extensions like the Git Graph or GitLens ones, but I find those UIs to be really painful as well.

[David Loeffler]

You’re not really the target audience for a getting-started guide, Marc. The great advantage of VSCode’s built -in client is that we can safely assume users have it on their machine already.

[David Loeffler]

I’ve often heard from mathematician colleagues that they made an attempt to try out Lean but lost interest because the installation process was too long / too complicated/ involved downloading too much stuff. So minimizing the number of packages a user needs to install should be a priority.

[David Loeffler]

preferring rebasing over merging (so your experience might vary if you prefer merging)

FWIW, I don't have a preference in this regard, because I haven't the faintest idea what the difference between them is; and I am unhappy with the implication that this is, or should be, essential knowledge for a Mathlib contributor.

The Lean community contains both programmers, and mathematicians; the latter, by and large, do not regard details of how to use git as obvious or self-explanatory. The last 48 hours or so have given the distinct impression that those leading this community have either forgotten that the non-programmers exist, or do not value their contributions.

[Marc Huisinga]

That's true. I'm just saying that I believe that the UI of GitHub Desktop might be more intuitive than the one in VS Code, even for beginners. At least I found the former to be usable and the latter to be really hard to use when I didn't know much about Git, since the VS Code UI is just a thin wrapper over the command-line UI and doesn't really put the most common operations front-and-center. So IMO there's a trade-off here: The installation gets more complicated, while using Git becomes easier. Not sure which of these two is preferable :-)

E.g. the notion of "staging" is really intuitive in GitHub Desktop: There's a commit button, and all of your changes will be committed by default. You can unselect some of them using a checkbox if you don't want to commit them. In the VS Code integration, your files aren't staged by default and VS Code will complain when you try to commit without first staging files.

Staging in GitHub Desktop

Staging in VS Code

Similarly, when switching branches while you still have changes on your branch, GitHub Desktop will suggest to either move your changes over to the other branch or stash them on your old branch, while the VS Code integration will always move them over by default, and you need to figure out that stashing is the thing you need to use in its UI to get the other behavior. GitHub Desktop also reminds you that you have stashed changes on your branch when you do.

Stashing in GitHub Desktop

Stashing in VS Code (which of these buttons do I click?)

David Loeffler said:

FWIW, I don't have a preference in this regard, because I haven't the faintest idea what the difference between them is; and I am unhappy with the implication that this is, or should be, essential knowledge for a Mathlib contributor.

I am not suggesting this implication. It isn't essential knowledge. I'm just providing examples where some users may still need to fall back to the command line to outline some of the limitations of these UIs that I've encountered myself. If you don't know what rebasing is, then great - you were not the intended target audience of my post.

[David Loeffler]

If you don't know what rebasing is, then great - you were not the intended target audience of my post.

If so, why did you post your post into a discussion about what UI to prioritize in a guide to first-time git users?

[Marc Huisinga]

David, you're probably right. I'll stop contributing to this discussion and providing information about the options that are available.

[David Loeffler]

My wider point is that there is a huge cultural chasm between what programmers regard as "obvious" and what mathematicians regard as "obvious". Marc and I clearly live on different sides of this chasm. Clearly the Mathlib community needs both groups, but some care is needed in communicating across the divide.

[David Loeffler]

Providing information on available options is clearly valuable, but we need to avoid drowning new users in a flood of unfamiliar concepts, terminology, and tools.

[Kim Morrison]

David, would you be willing to try writing such a guide? It seems like you might be in the sweet spot. I'm sure we can help revise and proofread or indeed explain things if you have trouble working them out?

[David Loeffler]

@Kim I wouldn't know how to even start writing that. I don't know how git is supposed to work, I've literally never used it except for mathlib contributions – and, for the n-th time, I am quite fed up with it being assumed that everyone in the community knows how git works.

[David Loeffler]

I suppose I could write a "Getting started with Git : A guide for mathematicians" note, but I cannot commit to keeping it up-to-date long term, and I am wary of getting into a position where I'm coming under fire from both sides (from newbies who are confused by my instructions and from experts who consider my instructions to be The Wrong Thing).

[Shreyas Srinivas]

Here is a conceptual picture of git: https://eagain.net/articles/git-for-computer-scientists/

[Shreyas Srinivas]

It says “for computer scientists”, basically explains git in terms of labelled directed acyclic graphs

[Shreyas Srinivas]

And a game to learn git : https://ohmygit.org/

[Shreyas Srinivas]

Another : https://learngitbranching.js.org/

[David Loeffler]

Shreyas Srinivas said:

Here is a conceptual picture of git: https://eagain.net/articles/git-for-computer-scientists/

This is a very nice and clear explanation of how a single Git repo works (in isolation), but it says essentially nothing about working with remotes. The thing that has just changed, from a user's perspective, is suddenly having to manage working with multiple remotes (the master mathlib repo and individual user's forks of it).

[Shreyas Srinivas]

I am trying to find resources on remotes which are as visual or mathematical as that one. If I don’t find one, and have a bit of time, I might write it.

Meanwhile, here is a gist : each remote is another git repository in its own right, and the goal of all the commands is to keep the relevant pieces of the history DAG as identical as possible.

More precisely your local clone and a GitHub fork (origin) are both DAGs, which are isomorphic to (a subgraph of) the mathlib4 repo DAG called upstream. The goal is to maintain the isomorphisms between these DAGs, specifically between their subgraphs reachable from the source vertex that is the latest commit on mathlib’s master branch. This needs to be done as you and many others are making changes to their respective DAGs by adding new vertices (called commits)

[David Loeffler]

Thanks for the explanation, Shreyas! When you say "reachable", "source vertex" etc, are we thinking of the orientation of arrows as pointing backwards in time (from each commit to its predecessor) or forwards (from a commit to the later ones building on it)?

[Shreyas Srinivas]

Yeah

[Shreyas Srinivas]

Exactly

[Shreyas Srinivas]

Backwards in time

[David Loeffler]

[deleted]

[Shreyas Srinivas]

Ultimately the chain of commits that begins with the source vertex of the master branch must be identical in all three copies of the DAG

[David Loeffler]

That's a good model, but it doesn't seem to reflect what actually happened when I forked mathlib – it looks like I got all the branches and commits in the upstream repo, not just those which were ancestors of the latest commit on master.

[Shreyas Srinivas]

GitHub provides you the option to copy only the main/master branch

[Shreyas Srinivas]

and that is also why I said that we are maintaining an isomorphism between “subgraphs”, since it doesn’t preclude one from maintaining isomorphisms between larger subgraphs (subgraph-relation-wise larger) or choosing to ignore certain subgraphs (for example your local branches that you may decide not to push)

[David Loeffler]

Shreyas Srinivas said:

GitHub provides you the option to copy only the main/master branch

... but the Mathlib migrate script doesn't, apparently; perhaps it should offer this option, or even make it the default. [Edit: I have posted to suggest this in the "migrate script feedback" thread.] Not important, though; I ran a script to delete all the branches in my fork except master and my own.

Related question: somewhere, there is a mapping being stored from branches in my GitHub fork, to branches in the master mathlib repo, saying "this branch is based off that one". How do I edit this mapping? I know how to change the upstream branches for each branch in my local repo; but that's not what I'm asking here – I'm asking about the mapping between branches in my GH fork of Mathlib and in the master Mathlib, not the mapping between branches in my GH fork and my local repo.

[David Loeffler]

(The motivation for this is to make the button in GitHub, for pulling new commits from upstream into the PR branches in my fork, work properly. At the moment, it looks for new commits in my old PR branches in the master repo, rather than the master branch of the master repo.)

[Shreyas Srinivas]

I do not know of an explicit way to change that mapping out of hand. I have never migrated PRs like this before

[Shreyas Srinivas]

Perhaps someone with more familiarity with Github's interface could help

[David Loeffler]

No worries, and many thanks for all your explanations in this thread!

[Yaël Dillies]

The git command is git branch --set-upstream. I don't know of any way to trigger this command through any UI

[David Loeffler]

@Yael, isn't that for changing the mapping between local branches and origin branches, not between origin branches and upstream branches?

[David Loeffler]

Quote:

I know how to change the upstream branches for each branch in my local repo; but that's not what I'm asking here – I'm asking about the mapping between branches in my GH fork of Mathlib and in the master Mathlib, not the mapping between branches in my GH fork and my local repo.

I think Yael just answered the question I specifically said I was not asking.

[Yaël Dillies]

No, I read really carefully your message that you quote, and I do believe I am answering your question

[David Loeffler]

... would you care to elaborate how?

[Yaël Dillies]

I am going to state a few facts (I am not sure all of them are correct, feel free to point issues):

1. The local repo acts just like any other fork. In the standard mathlib setup until last week, you actually had two forks, the local one and origin, and there was a mapping of branches between them.
2. In the new setup, you will typically interact with three forks: your local one, upstream (aka leanprover-community/mathlib4) and origin (aka loefflerd/mathlib4)
3. git branch --set-upstream works just as well to set the "upstream branch" ( :warning: not necessarily an upstream branch!) of a local branch to a branch from origin or a branch from upstream.
4. Your question is nonsensical, since even if you could "link" a branch from origin to a branch from upstream, you wouldn't be able to push anything to the upstream counterpart since you will soon not have write access anymore.

[Shreyas Srinivas]

I would also surprised if git commands run on the local repo change tracking branches between the origin repo and upstream repo

[Yaël Dillies]

Edited

[Yaël Dillies]

Basically I think you are asking the wrong question. But feel free to explain further what you want to do with this "linking" between the origin and upstream branches.

[David Loeffler]

There's a button in the GitHub web interface for each branch in my fork repo, which says "Sync fork". Perhaps you can explain to whichever github dev put it there that its existence is apparently nonsensical.

[David Loeffler]

I'm trying to change which fork on upstream that button triggers pulling from.

[Yaël Dillies]

I must say I have never witnessed that button on any other branch than master. Can you send a screenshot of this button on a non-master branch?

[Shreyas Srinivas]

So point 4 is a bit more nuanced than your messages suggest so far. I can see why David is asking this question.

[Markus Himmel]

David Loeffler said:

There's a button in the GitHub web interface for each branch in my fork repo, which says "Sync fork".

Do you have reason to believe that this isn't just based on branch names? So if you look at a branch named branch on your fork, it will offer you to sync with the branch named branch on the upstream, if such a branch exists?

[Yaël Dillies]

Shreyas Srinivas said:

So point 4 is a bit more nuanced than your messages

I was expecting David to want to push changes through this link, not to pull them (what branches could one want to pull commits from if not master? nightly-testing maybe?)

[Edward van de Meent]

indeed, according to the github docs about this button, it seems it basically syncs the git history from the upstream repo and fast-forward merges upstream/main into origin/main. however, it's a not a main branch only

[Shreyas Srinivas]

David is asking a reasonable question because I just explained git as a distributed version control system with multiple independent copies of a repository

[David Loeffler]

Screenshot 2025-06-15 at 16.33.25.png

[Shreyas Srinivas]

So David is justified in asking why he can't control the repo copy which is his github fork to point some branch there to an upstream branch

[Yaël Dillies]

What if you rename the branch? Does the button still appear?

[Yaël Dillies]

I genuinely do not know where this button is coming from, but it's most likely a name-based github-only feature

[Shreyas Srinivas]

The answer is that github, the currently Microsoft owned service, is separate from git. It allows users to manage repositories such as upstream mathlib4 and the forks we make through a limited interface to produce some workflows. It doesn't seem to let you point a branch from your fork to the corresponding branch in upstream mathlib4 as far as I can tell. This is a github design choice, that other service providers also replicate.

EDIT : @David Loeffler I hope I guessed correctly

[Edward van de Meent]

strangely, they do let you do this when you create a new branch

[Edward van de Meent]

i.e. when you create a branch from an upstream branch via the GH interface, it will trace it

[David Loeffler]

The context is that this branch is not behind the upstream DL_top_sine_curve branch, but it is > 300 commits behind the upstream master branch and I am asking if there is a one-step way to update it with those commits.

It seems there isn't a way to do this, which is fine. But I am not terribly impressed by being told with great conviction that my question is nonsensical.

[Shreyas Srinivas]

If you take github's offer to make a pull request from DL_top_sine_curve and make a pull request to the upstream mathlib4's master branch, there is an option that will show up in the pull request to merge master into your PR

[Shreyas Srinivas]

There is no guarantee that this will not produce a merge conflict however

[David Loeffler]

If you take github's offer to make a pull request from DL_top_sine_curve and make a pull request to the upstream mathlib4's master branch, there is an option that will show up in the pull request to merge master into your PR

I have done this and I do not see such an option (unless it was part of the PR creation step, in which case I may have overlooked it there)

[Shreyas Srinivas]

My bad. I think it only shows up for me in repositories where I am a maintainer

[Shreyas Srinivas]

Or I am the PR author

[Shreyas Srinivas]

David : Do you see the update branch option as in the screenshot (the colours might be different but this is the box at the bottom of the PR page that tells you whether you have a merge conflict or not, just above the squash and merge button. See example:

image.png

[David Loeffler]

I just see a big warning sign "Merging is blocked: You're not authorized to push to this branch".

[Shreyas Srinivas]

Could you screenshot the corresponding part of your webpage and paste it here? If not, then :

1. If there are no complaints about a merge conflict, your PR can be safely merged as is.
2. If there is an update brranch button, then clicking on that should incorporate those 300 commits in the mathlib4 master branch that you don't have.

[David Loeffler]

Screenshot 2025-06-15 at 16.57.14.png

[Shreyas Srinivas]

I don't see a merge conflict, so your PR can be safely merged (modulo CI checks) for now

[Shreyas Srinivas]

According to the github doc page The "update branch" button only shows up when all of the following are true:

• There are no merge conflicts between the pull request branch and the base branch.
• The pull request branch is not up to date with the base branch.
• The base branch requires branches to be up to date before merging or the setting to always suggest updating branches is enabled.```

[Shreyas Srinivas]

Maybe one of the mathlib maintainers can tell us whether condition 3 holds or not, but that is the first thing to check.

[David Loeffler]

1. If there are no complaints about a merge conflict, your PR can be safely merged as is.

This isn't quite true, I think [edit to clarify: this just depends how you define "safely"]; the check only verifies that git is capable of auto-merging the code, not that the merged code actually compiles without errors. This is why I want to merge master in my PR: so I can let CI run on the merged codebase, and then fix any fallout. And I was hoping this this could be done in one click, without having to use my own local repo as a middle-man between the two repos on GitHub. As I said, if it isn't possible, then I'm totally fine with that.

According to the github doc page The "update branch" button only shows up when all of the following are true:

Is your screenshot from some other repo, not mathlib? I've never seen such a button in mathlib, so perhaps the mathlib repo has this configuration set differently.

[Shreyas Srinivas]

Yes the screenshot is from iris-lean equational theories. And yes, by “safety”, I was referring to the absence of merge conflicts. Of course the CI must do its duty.

[Shreyas Srinivas]

David Loeffler said:

Is your screenshot from some other repo, not mathlib? I've never seen such a button in mathlib, so perhaps the mathlib repo has this configuration set differently.

This is why I suggested that condition 3 is the first thing to check. I always get the option to “update branch” on my projects if my PR is not up to date with the main branch.

[Shreyas Srinivas]

Only maintainers can do that

[Shreyas Srinivas]

Specifically this condition

• The base branch requires branches to be up to date before merging or the setting to always suggest updating branches is enabled.

[David Loeffler]

Shreyas Srinivas said:

Yes the screenshot is from iris-lean. And yes, by “safety”, I was referring to the absence of merge conflicts. Of course the CI must do its duty.

It’d be nice if we could have CI run periodically (every few days?) on all open PRs that are git-mergeable against current master, and post a warning if the result of the merge doesn’t pass the tests. But this is orthogonal to the current discussion.

[Shreyas Srinivas]

You don’t need CI for git-mergeability. If the maintainers turn on this switch I quoted in my last message, GitHub will show you the panel in my screenshot with an indication of merge conflicts if any.

[Shreyas Srinivas]

You need CI to be sure that mathlib itself builds according to lean, and docs are generated and so on.

[Jz Pan]

David Loeffler said:

This is why I want to merge master in my PR: so I can let CI run on the merged codebase, and then fix any fallout. And I was hoping this this could be done in one click, without having to use my own local repo as a middle-man between the two repos on GitHub. As I said, if it isn't possible, then I'm totally fine with that.

I don't think it's possible without your local copy of master up-to-date.

So the step for my personal setup is:

1. make your local copy of master up-to-date. (In my personal setup, it's 3 steps: (i) click "Sync fork" button on the github master webpage of my own fork of mathlib; (ii) git checkout master if it's not already working on master branch; (iii) git pull origin master which downloads newest changes of master branch to local. NOTE THAT this step is different if you use the recommended setup discussed here. In this case, ask git experts in this thread.)
2. working on my branch again: git checkout my_branch
3. git gui which will launch a default GUI of git where there is an option to merge (menu Merge > Local Merge... then choose master in the list box, then click Merge button).
4. Assume that there are no merge conflicts. Then you can click Push button in the git GUI (the last button of 5 buttons in a column), there will be a confirmation dialog, and click Push again. In this way your local edits and merges will be uploaded to your own fork of mathlib on github.

[Jz Pan]

(deleted)

[Shreyas Srinivas]

Jz Pan said:

David Loeffler said:

This is why I want to merge master in my PR: so I can let CI run on the merged codebase, and then fix any fallout. And I was hoping this this could be done in one click, without having to use my own local repo as a middle-man between the two repos on GitHub. As I said, if it isn't possible, then I'm totally fine with that.

I don't think it's possible without your local copy of master up-to-date.

So the step is:

1. make your local copy of master up-to-date. (In my personal setup, it's 3 steps: (i) click "Sync fork" button on the github master webpage of my own fork of mathlib; (ii) git checkout master if it's not already working on master branch; (iii) git pull origin master which downloads newest changes of master branch to local. NOTE THAT this step is different if you use the recommended setup discussed here. In this case, ask git experts in this thread.)
2. working on my branch again: git checkout my_branch
3. git gui which will launch a default GUI of git where there is an option to merge (menu Merge > Local Merge... then choose master in the list box, then click Merge button).
4. Assume that there are no merge conflicts. Then you can click Push button in the git GUI (the last button of 5 buttons in a column), there will be a confirmation dialog, and click Push again. In this way your local edits and merges will be uploaded to your own fork of mathlib on github.

This is not true. If mathlib maintainers enable the feature that I quoted above from GitHub docs, you get the update branch button

[Shreyas Srinivas]

As long as there is no merge conflict it will merge master into your PR

[David Loeffler]

@Jz Pan This seems ... more complicated than I expected. Wouldn't something like git fetch; git merge origin/master work (without having to switch branches on the local repo)?

[Julian Berman]

• make your local copy of master up-to-date. (In my personal setup, it's 3 steps: (i) click "Sync fork" button on the github master webpage of my own fork of mathlib; (ii) git checkout master if it's not already working on master branch; (iii) git pull origin master which downloads newest changes of master branch to local. NOTE THAT this step is different if you use the recommended setup discussed here. In this case, ask git experts in this thread.)
• working on my branch again: git checkout my_branch
git gui which will launch a default GUI of git where there is an option to merge (menu Merge > Local Merge... then choose master in the list box, then click Merge button).

I'm not following this thread, but will point out you don't ever really need to update your master branch if that's not what you're working on at the time -- specifically in this 3 step workflow the more "direct" way to merge upstream's master is the two step git fetch upstream && git merge upstream/master (replace upstream with whatever you or the script calls the leanprover-community remote) all while staying on your my_branch -- it's always in some sense "safer" to merge remote branches than local ones, though this is an expert..

And now I see David knows this already :) so yes David you're right.

[David Loeffler]

I'm glad, because I prefer to avoid switching branches on my local repo if I can help it. The problem is that this invalidates all the build output in the local directory (which takes forever to recompile, and a nontrivial time even to un-pack from cache).

[David Loeffler]

David Loeffler said:

(The motivation for this is to make the button in GitHub, for pulling new commits from upstream into the PR branches in my fork, work properly. At the moment, it looks for new commits in my old PR branches in the master repo, rather than the master branch of the master repo.)

Quite by chance I found out how to solve this problem (and the solution is face-palmingly simple). GitHub matches up branches in the fork to branches in the main mathlib repo based on branch name; but it defaults to master if no upstream branch with that name exists. So the solution was just to delete my old branches in the main mathlib repo, and now everything works exactly as I had wanted: the "Sync fork" button pulls the latest mathlib master into my fork PR branch with a single click.