New contribution model: PRs from forks

Stream: mathlib4

[Johan Commelin]

Dear Mathlib community, cc @channel

With this message we want to announce the final step in the transition to the new contribution model. All future PRs will be made from personal forks.
We realize that this transition has been a bumpy ride, and we apologize for that.

In this new setting:

• by default, all community members who had "write" access now have "triage" access (to add/remove labels on PRs)
• currently members of the reviewer and maintainer teams still have "write" access; in the near future, many of them (including most maintainers) will also reduce their access to "triage"
• the CI team will retain "write" access

For more information on how to create PRs from forks, please see the Git Guide for Mathlib4 Contributors.

For more information on how to migrate existing PRs to PRs from forks, please see the page Mathlib4 wiki > Migration to PRs from forks.

Best regards,
the Mathlib maintainers

[Mauricio Collares]

Congratulations! This is a lot better from a security standpoint. Now that it is done, can it be revealed if this was a preventive measure or done in response to a malicious actor (or someone reporting a vulnerability)?

[Johan Commelin]

The previous model was not secure nor sustainable as we grow the number of contributors. This was a preventive measure. We have seen no indication of any attempted exploits but believed it prudent to take action sooner rather than later. The new model is well-tested for large scale active collaboration.

[Ruben Van de Velde]

Sorry if I missed this - What's the way to get oleans without opening a pr now?

[Johan Commelin]

This is indeed a change. Please feel free to open a draft PR in that scenario.

[Calle Sönne]

Have the new permissions changes also affected reviewing as a non-reviewer? E.g. I reviewed #25971 today, and the approval sign is no longer green, and more importantly, I can't see a small "approved" text in the list of PRs that involve me. If so, should there be a new approved tag non-reviewers to use?

[Yaël Dillies]

I believe so

[Calle Sönne]

Then in my opinion there should be an approved by non-reviewertag or something similar. Otherwise its quite hard to get an overview over which of the reviews I am involved with that I already looked at.

[Yaël Dillies]

Maybe you should be made a reviewer? :innocent:

[Anatole Dedecker]

I agree that this distinction in the GitHub UI is annoying (although I see where it's coming from of course), and I agree that replacing this with a tag would be nice.

[Kenny Lau]

I think it's actually good personally for me, so that I can make it clear that I'm not an official reviewer, and my "approvals" should be taken less seriously.

[Junyan Xu]

So now if I want to review a PR locally (not in Gitpod/codespace) I'll need to add the author's fork as a remote. The git command is nontrivial to type. Can we add a VS Code command in the palette or a lake command to minimize typing / memorization?

[Yaël Dillies]

Kenny Lau said:

I think it's actually good personally for me, so that I can make it clear that I'm not an official reviewer, and my "approvals" should be taken less seriously.

This distinction is already made by the lack of maintainer-merge label when you approve a PR

[Matthew Ballard]

gh pr checkout XXXXX in the main repository should work

[Johan Commelin]

Junyan Xu said:

So now if I want to review a PR locally (not in Gitpod/codespace) I'll need to add the author's fork as a remote. The git command is nontrivial to type. Can we add a VS Code command in the palette or a lake command to minimize typing / memorization?

gh pr checkout 12345 should work, which I think is similar in difficulty to the old approach of git checkout some_branch_name.

[Joscha Mennicken]

You can even do this manually without gh or adding another remote using this command: git fetch upstream pull/12345/head:local_branch_name.

[Matthew Ballard]

Note that you can also do gh pr list --label 't-differential-geometry' to get the number if you forget (like I often do).

[Junyan Xu]

Thanks for the suggestions! I just installed GitHub CLI and hopefully it works once I restart my VS Code (or possibly the PC).

[Théo Zimmermann]

Johan Commelin said:

• currently members of the reviewer and maintainer teams still have "write" access; in the near future, many of them (including most maintainers) will also reduce their access to "triage"

About this: perhaps this is what you want to attain (I haven't followed any of these changes), but note that, last I checked, the triage permission prevents things like closing issues, which can be useful for triage. In the context of the Rocq development, we have a larger pool of contributors with write access than who is actually able to merge PRs. And nobody can push new branches (all PRs are made from forks), except core team members specifically for release branches. All of this is achieved with GitHub new rulesets: https://github.com/rocq-prover/rocq/rules
Maybe you already knew all of this, in this case sorry for the noise, but I wanted to share our experience just in case it is useful.

[Robin Arnez]

I wonder if you could maybe also use these rules to allow write access to lean-pr-testing-nnnn and batteries-pr-testing-nnnn branches for the original PR owner? It's definitely convenient if you can just push fixes there (especially if they are trivial) without needing to actually make an additional mathlib PR

[Kim Morrison]

@Robin Arnez, yes the current set up for lean-pr-testing-NNNN PRs is not viable for the long term, and we need to work out how to fix this. This hasn't been a priority while we fix the problems affecting everyone. Likely we will create a designated fork to host these branches.

[Johan Commelin]

@Théo Zimmermann Thanks for sharing those ideas!

[Notification Bot]

Shubham Kumar 🦀 (he/him) has marked this topic as resolved.