automatic "needs review" after merging develop branch

[Martin R]

Ii is currently a pain to find pull requests that *really* need review, because, after every minor release, people tend to merge develop (which makes sense), and then some bot changes the label to "needs review", no matter what it was before.

Can somebody please please fix that?

Martin  

[Dima Pasechnik]

Technically speaking, merging a branch into PR might lead to breaking changes.
So it's a grey zone.

I would say, if the branch status says that the base branch is outdated, but "changes can be cleanly merged", there is no pressing need to do this merge. And if you do the merge please at least check that the CI continues to be OK. Often it's safe to turn the positive review status back on after this.

[Martin R]

The problem is that the bot turns tickets from "needs work" to "needs review".

[dim...@gmail.com]

On Mon, Sep 01, 2025 at 04:45:01AM -0700, 'Martin R' via sage-devel wrote:
> The problem is that the bot turns tickets from "needs work" to "needs
> review".

It's not easy to tell a merge which doesn't fix "needs work" from one
that does.

One way to deal with this is to mark long-time "needs work" PRs as
Draft.
(That's a "native" GitHub way to mark PRs which are not ready)

> --
> You received this message because you are subscribed to the Google Groups "sage-devel" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/sage-devel/a86c786d-7c06-48ba-a565-21ebc69b890cn%40googlegroups.com.

[Antonio Rojas]

El lunes, 1 de septiembre de 2025 a las 17:38:35 UTC+2, dim...@gmail.com escribió:

It's not easy to tell a merge which doesn't fix "needs work" from one
that does.

Which is why the bot should never change the status of PR's marked as "needs work". Going from "needs work" to "needs review" should always be a manual step IMO. I am also highly annoyed by this.

[Martin R]

Why should a PR go automagically (!) from needs work to needs review after a merge?

Martin

[Dima Pasechnik]

that's the question for the designer,
Sebastian (@soehms) IIRC.

[Kwankyu Lee]

On Tuesday, September 2, 2025 at 1:09:35 AM UTC+9 axio...@yahoo.de wrote:

Why should a PR go automagically (!) from needs work to needs review after a merge?

We are expected to use the github interface. So to avoid the problem, first "convert to draft".

[Martin R]

PR's should be draft by default.  As a reviewer, I cannot convert to draft.

I agree that it might be better to get rid of the labels `positive review`, `needs review`, `needs work` now.

Martin

[Dima Pasechnik]

On Tue, Sep 2, 2025 at 7:21 AM 'Martin R' via sage-devel
<sage-...@googlegroups.com> wrote:
>
> PR's should be draft by default. As a reviewer, I cannot convert to draft.
>
> I agree that it might be better to get rid of the labels `positive review`, `needs review`, `needs work` now.

how would one know that a draft PR needs review, without a "needs review" label?

>
> Martin
>
> On Tuesday, 2 September 2025 at 03:12:48 UTC+2 Kwankyu Lee wrote:
>>
>> On Tuesday, September 2, 2025 at 1:09:35 AM UTC+9 axio...@yahoo.de wrote:
>>
>> Why should a PR go automagically (!) from needs work to needs review after a merge?
>>
>>
>> We are expected to use the github interface. So to avoid the problem, first "convert to draft".
>

> --
> You received this message because you are subscribed to the Google Groups "sage-devel" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+...@googlegroups.com.

> To view this discussion visit https://groups.google.com/d/msgid/sage-devel/bac3bd30-adc2-42c0-8a0a-b2091ce57ce3n%40googlegroups.com.

[Vincent Macri]

Automatically changing the labels after commits is something done by our GitHub Actions setup (I think we implement this behaviour in https://github.com/sagemath/sage/blob/develop/.github/sync_labels.py).

I think the "correct" (i.e. how GitHub expects you to do it) workflow is that draft PRs are used for PRs that the person making the PR does not think are ready to be merged or be formally reviewed, but is just looking for feedback on something in-progress, or maybe wants to run the CI on their in-progress work (it's difficult to test CI locally). Draft PRs can also be used for a proof-of-concept that the developer wants to share and ask for feedback on before making a more serious attempt later, or to show off half-finished code that they don't expect to finish soon in the hopes that someone else with more time might pick it up and finish it.

GitHub also has features where reviewers can mark something as accepted, needs changes, etc. without setting any labels ("Review changes" in the "Files changed" tab of a PR). But any GitHub user can do this, they don't need any permissions in the SageMath organization (we probably want people to need some permissions to be able to approve a PR, otherwise someone could make two GitHub accounts and bypass the review process by approving their PR from their second account).

On 2025-09-02 6:21 a.m., 'Martin R' via sage-devel wrote:

PR's should be draft by default.  As a reviewer, I cannot convert to draft.

A draft PR cannot be merged even with a positive review, so I don't think we should default to drafts. But people making a PR can (and perhaps should) change their PRs to draft if they think reviewer comments will take some time to address.

On 2025-09-01 9:51 a.m., Antonio Rojas wrote:

Which is why the bot should never change the status of PR's marked as "needs work". Going from "needs work" to "needs review" should always be a manual step IMO. I am also highly annoyed by this.

This would leave no way for a new contributor without permissions to change the GitHub labels to get attention on their PR after addressing the first reviewer's feedback (mostly an issue if the first reviewer is not available to review the changes).

I'm not sure if this is possible, but maybe a solution would be to have the GitHub Action responsible for changing "needs work" to "needs review" on PRs only do so when the author does not have permission to update the labels themselves. I think the current behaviour is mostly reasonable, but as people have mentioned in this thread it isn't always ideal. Someone with permissions on GitHub to change their PR from "needs work" to "needs review" can do so when they believe they have addressed the reviewer's feedback (which may take multiple commits), but contributors without the GitHub permissions (mostly new contributors, who we should try to make sure have a smooth experience so that they continue contributing) cannot do this. We would still have the same issues discussed here for PRs from new contributors, but I think these are a minority of PRs, so I'm not concerned that leaving the current behaviour only for these users would make it difficult to find PRs that actually need review.

Alternatively (or perhaps additionally), I'm pretty sure that merging develop always gives the same default commit message ("Merge branch 'develop' into [branch name]", not sure if this is different if done from the git command line instead of the GitHub web interface). Perhaps we just don't change the label from "needs work" to "needs review" if the commit message matches that? We should still change "positive review" to "needs review" though since a merge could break something (there is also nothing stopping someone from committing malicious code with the commit message "Merge branch 'develop' into [branch name]" after receiving "positive review").

[Martin R]

OK, github permissions seems to be a difficult topic.

What I thought is that one could have a special permission "is allowed to do reviews, i.e., approve a PR".  But maybe that's not how github works.

> how would one know that a draft PR needs review, without a "needs review" label?

By clicking on the "ready for review" button next to "This pull request is still a work in progress Draft pull requests cannot be merged."

Martin

[Vincent Macri]

On 2025-09-02 12:16 p.m., 'Martin R' via sage-devel wrote:
> OK, github permissions seems to be a difficult topic.
>
> What I thought is that one could have a special permission "is allowed
> to do reviews, i.e., approve a PR".  But maybe that's not how github
> works.

This prompted me to check, I was correct about the default behaviour but
there are settings to change it:
https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/managing-repository-settings/managing-pull-request-reviews-in-your-repository
and
https://docs.github.com/en/organizations/managing-organization-settings/managing-pull-request-reviews-in-your-organization.
I'm not sure exactly how this works or how much granularity it allows.
Only organization owners can change this setting. It's also not super
clear to me exactly what our policy is for allowing someone to approve a
PR. I was looking at the GitHub Action responsible for managing labels
and I think anyone who has committed before can approve a PR by
including the right phrase at the start of their review comment?

The easiest solution to the issue of the bot changing "needs work" to
"needs review" after merging develop can probably be solved by ignoring
commits with a message of "Merge 'develop' [...]" in the GitHub Action.
I've created https://github.com/sagemath/sage/issues/40758 if anyone
wants to try.

[Dima Pasechnik]

On Tue, Sep 2, 2025 at 1:16 PM 'Martin R' via sage-devel
<sage-...@googlegroups.com> wrote:
>
> OK, github permissions seems to be a difficult topic.
>
> What I thought is that one could have a special permission "is allowed to do reviews, i.e., approve a PR". But maybe that's not how github works.
>
> > how would one know that a draft PR needs review, without a "needs review" label?
>
> By clicking on the "ready for review" button next to "This pull request is still a work in progress Draft pull requests cannot be merged."

but this button removes the draft status.

> --
> You received this message because you are subscribed to the Google Groups "sage-devel" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+...@googlegroups.com.

> To view this discussion visit https://groups.google.com/d/msgid/sage-devel/86aad875-baf9-4db0-bbb3-ffa3f4f365b8n%40googlegroups.com.

[Martin R]

> but this button removes the draft status.

I guess that I severely miscommunicated.  I had the following process in mind:

1. PR is opened, and automatically set to "draft"

2. once it is ready for review, owner clicks "needs review", so the "draft" is removed

3. a developer with review privileges either selects "approve" or "request changes"

The labels "needs review", "needs work" and "positive review" are gone.

However, this would only work if there is such a thing as "review privilege".  Moreover, I can imagine that there are further problems.  In particular, I am not sure how filtering by review status works, currently "review:approved" gives no results.

Martin

[Tobia...@gmx.de]

I second that "needs review" and "needs work" are mostly obsolete and should be better handled by native github tools. Those labels were introduced when migrating to github to not change the workflow too much from the good old trac days. Besides the automatic transition "needs work" -> "needs review" after just merging develop, I also find it somewhat annoying to manually set the "needs work" label after just submitting a "request changes" review.

Perhaps as a transition period, those two labels could just reflect the github status. So:

- There is a review with "Request changes" -> "needs work"

- The PR is not a draft and not in "needs work" or "positive review" -> "needs review"

If someone gives a "request changes" review and the PR author addresses the changes, one can re-request a new review (last point in https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/requesting-a-pull-request-review#requesting-reviews-from-collaborators-and-organization-members), which then removes the "request changes" status and thereby would automatically transition the PR into "needs review". The button is not there for new contributors, but those can either ping the original reviewer for a new review (or in the rare case that nobody is reacting to such a call, ping the core team to have the review invalidated.)

The positive review label still needs to be there to signal Volker that the PR is ready to be merged. (The github way would be to replace the buildbots by the merge queue feature)

[Vincent Macri]

On 2025-09-03 6:01 a.m., 'Tobia...@gmx.de' via sage-devel wrote:
> I second that "needs review" and "needs work" are mostly obsolete and
> should be better handled by native github tools. Those labels were
> introduced when migrating to github to not change the workflow too
> much from the good old trac days. Besides the automatic transition
> "needs work" -> "needs review" after just merging develop, I also find
> it somewhat annoying to manually set the "needs work" label after just
> submitting a "request changes" review.
>
> Perhaps as a transition period, those two labels could just reflect
> the github status. So:
> - There is a review with "Request changes" -> "needs work"
> - The PR is not a draft and not in "needs work" or "positive review"
> -> "needs review"
>
> If someone gives a "request changes" review and the PR author
> addresses the changes, one can re-request a new review (last point
> in https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/requesting-a-pull-request-review#requesting-reviews-from-collaborators-and-organization-members),
> which then removes the "request changes" status and thereby would
> automatically transition the PR into "needs review". The button is not
> there for new contributors, but those can either ping the original
> reviewer for a new review (or in the rare case that nobody is reacting
> to such a call, ping the core team to have the review invalidated.)
>
> The positive review label still needs to be there to signal Volker
> that the PR is ready to be merged. (The github way would be to replace
> the buildbots by the merge queue feature)

In theory this behaviour is already implemented in
https://github.com/sagemath/sage/blob/develop/.github/sync_labels.py.
However it doesn't seem to work (I just tried on
https://github.com/sagemath/sage/pull/40634 and nothing happened, I'm
going to avoid setting the label manually in case it actually does work
just with a delay). So I guess that needs to be fixed. I'm not sure if
the sync_labels.py script is broken or if the GitHub Action that runs
the script just isn't triggering
(https://github.com/sagemath/sage/blob/develop/.github/workflows/sync_labels.yml).

Something to note from scanning through the code, in order for it to
determine if someone has sufficient permissions to set the label to
positive review, one must set their membership in the SageMath
organization to public (mine is set to public and it still didn't work).
So in order for this to work consistently we may want to encourage
people to set their membership in the SageMath GitHub organization to
public.

[Tobia...@gmx.de]

Right, good point, the script actually already has the logic to handle PR reviews. But the workflow run skips all steps when a PR review is submitted (see https://github.com/sagemath/sage/actions/runs/17460557035/job/49584072319), which suggests that the PR review event is in ' SYNC_LABELS_IGNORE_EVENTS'. Someone of the github admins needs to confirm/change that.

>  if: vars.SYNC_LABELS_ACTIVE == 'yes' && (! vars.SYNC_LABELS_IGNORE_EVENTS || ! contains(fromJSON(vars.SYNC_LABELS_IGNORE_EVENTS), github.event.action))