Groups keyboard shortcuts have been updated
Dismiss
See shortcuts

Synchronization of GitHub state and priority labels continues on Tuesday July 11th

303 views
Skip to first unread message

seb....@gmail.com

unread,
Jun 7, 2024, 5:49:54 PM6/7/24
to sage-devel
Dear Sage developers,

We will now continue with a process that started last July. Unfortunately, this was blocked for many months while we waited for GitHub to fix a bug in their web-interface. Although this bug is still not fixed (see this comment on #35927), parts of label sync that are less critical to this bug should continue.

As before, the bot will be enabled in several steps. These are tracked in issue #35927. We are moving on to step 3 and 4, the first of which will be enabled next Tuesday. These steps will allow developers who are not members of the Triage team to have the s: needs review label on their PRs.

Please post comments, suggestions and bug reports on #35927.

Sebastian

seb....@gmail.com

unread,
Jun 7, 2024, 5:54:07 PM6/7/24
to sage-devel
Sorry, typo in the headline: July -> June!

seb....@gmail.com

unread,
Jun 10, 2024, 6:08:51 AM6/10/24
to sage-devel
Currently ther are about 90 open PR's that are not drafts but don't have any state label set (see this list). Obviously not all of them are authored by developers who cannot set these labels because they are not members of Triage. If you are a member of Triage and one of your PRs is among them, you should pay attention to what will change tomorrow:

1. If you simply forgot to set the s: needs review label, then the bot will do it for you in the future.
2. If you intentionally didn't set s: needs review for your PR (for example, because you want to check CI results first), then you should open your PR as a draft in the future (see item 6 here) and change its status to ready for review later on (see this page). Otherwise, the PR will have the s: needs review label from the start.

seb....@gmail.com

unread,
Jun 14, 2024, 3:10:26 AM6/14/24
to sage-devel
We will continue with this next Tuesday (June 18th) with step four. After that the s: needs review label will be set automatically if you mark a draft as ready for review or push a new commit to a non draft PR.

Kwankyu Lee

unread,
Aug 4, 2024, 7:10:07 AM8/4/24
to sage-devel
Hi

It seems that synchronization script adds "needs review" label whenever a new commit is uploaded to (non-draft) PR.

If a merge (with develop branch) commit is uploaded to a PR that has already got "positive review" label, then the "positive review" label is replaced with "needs review" label. This is annoying.

How about adding "needs review" label only when draft PR is converted to a non-draft PR?

seb....@gmail.com

unread,
Aug 4, 2024, 8:48:55 AM8/4/24
to sage-devel
We've already discussed this here: https://github.com/sagemath/sage/pull/36213#issuecomment-1711595430 and Tobias made a good argument for leaving it as is in https://github.com/sagemath/sage/pull/36213#issuecomment-1711640422.

What was the reason for rebasing a positively reviewed PR?

Kwankyu Lee

unread,
Aug 4, 2024, 9:49:22 PM8/4/24
to sage-devel
On Sunday, August 4, 2024 at 9:48:55 PM UTC+9 seb....@gmail.com wrote:
We've already discussed this here: https://github.com/sagemath/sage/pull/36213#issuecomment-1711595430 and Tobias made a good argument for leaving it as is in https://github.com/sagemath/sage/pull/36213#issuecomment-1711640422.

Once positively reviewed, we usually leave it to the author to keep the PR branch in good state to be merged with the develop branch. This is like "checking galley proof" stage of publishing a research paper.
 
What was the reason for rebasing a positively reviewed PR?

To see if the PR branch still work with the new develop branch (by running checks all again).
 

seb....@gmail.com

unread,
Aug 5, 2024, 2:05:00 AM8/5/24
to sage-devel
I see! On the other hand, you do benefit from this bot action after pushing changes to a non-draft PR (which probably happens much more often). But more importantly, if we disable this action, it would be a regression for developers who cannot set labels themselves.

Kwankyu Lee

unread,
Aug 5, 2024, 6:50:53 AM8/5/24
to sage-devel
 But more importantly, if we disable this action, it would be a regression for developers who cannot set labels themselves.

Isn't it enough to add "needs review" label only when draft PR is converted to a non-draft PR? Those developers may control the draft status. 

seb....@gmail.com

unread,
Aug 6, 2024, 2:30:29 AM8/6/24
to sage-devel
This would replace something annoying for senior developers by something annoying for new contributors. I'm not sure if this is a good idea.

Did you have to manually resolve merge conflicts in your example? If not, just don't push it back to the repository in such a situation in the future. If so, I agree with Tobias that *needs review* is a correct status.

Kwankyu Lee

unread,
Aug 6, 2024, 9:42:26 AM8/6/24
to sage-devel
On Tuesday, August 6, 2024 at 3:30:29 PM UTC+9 seb....@gmail.com wrote:
This would replace something annoying for senior developers by something annoying for new contributors. I'm not sure if this is a good idea.

Naturally, the volume of annoyance is much larger for senior developers. 

Did you have to manually resolve merge conflicts in your example? If not, just don't push it back to the repository in such a situation in the future. If so, I agree with Tobias that *needs review* is a correct status.

Not for my example, but I observed in others that trivial merge conflicts resolution put the PR back to "needs review" status.

If others do not share my opinion, I won't insist anymore. Let others speak.



 

Bagas Sanjaya

unread,
Aug 6, 2024, 9:17:52 PM8/6/24
to sage-...@googlegroups.com
On 8/6/24 20:42, Kwankyu Lee wrote:
> On Tuesday, August 6, 2024 at 3:30:29 PM UTC+9 seb....@gmail.com wrote:
>
> This would replace something annoying for senior developers by
> something annoying for new contributors. I'm not sure if this is a
> good idea.
>
>
> Naturally, the volume of annoyance is much larger for senior developers.
>
> Did you have to manually resolve merge conflicts in your example? If
> not, just don't push it back to the repository in such a situation
> in the future. If so, I agree with Tobias that *needs review* is a
> correct status.
>
>
> Not for my example, but I observed in others that trivial merge
> conflicts resolution put the PR back to "needs review" status.
>

Force-pushing will too.

Kwankyu Lee

unread,
Aug 29, 2024, 2:58:37 AM8/29/24
to sage-devel
Another instance of annoyance: https://github.com/sagemath/sage/pull/38564

I am fighting with the dumb synchronizer.

Matthias Koeppe

unread,
Aug 29, 2024, 2:18:56 PM8/29/24
to sage-devel
In this example, the synchronizer has been removing the "needs info" label from the PR on pushes.

Perhaps we should just phase out the use of the "needs info" label for PRs.

Personally, I do not recall much success in soliciting info from others using the "needs info" label. It may just be too ambiguous: Who's requesting info from whom?

Perhaps we should be defining this label it more narrowly: For flagging bug reports that do not have enough information for repro. In this case, there is a clear action that can be taken when no info comes in after a while: Closing the bug report as not actionable.

Kwankyu Lee

unread,
Aug 29, 2024, 8:07:20 PM8/29/24
to sage-devel
OK, I can live without the "needs info" label.

On the other hand, the PR is not yet for review because it intends to fix things in deprecation period. How can I stop the synchronizer from adding "needs review" whenever I push a commit?

Matthias Koeppe

unread,
Aug 29, 2024, 8:48:39 PM8/29/24
to sage-devel
Make it a draft PR, then the synchronizer is not active.

If it's waiting for something external, I also add the "pending" label.

Kwankyu Lee

unread,
Aug 29, 2024, 10:16:32 PM8/29/24
to sage-devel
On Friday, August 30, 2024 at 9:48:39 AM UTC+9 Matthias Koeppe wrote:
Make it a draft PR, then the synchronizer is not active.

Confirmed. Thanks.
Reply all
Reply to author
Forward
0 new messages