Synchronization of GitHub state and priority labels starts on Tuesday July 18th

[seb....@gmail.com]

Dear Sage developers,


Now, it's five months ago that the migration from Trac to GitHub happened. Many of us became familiar with the new workflows and probably found their own ways to use them. From this point of view it seems a little bit late to introduce a new feature to make the workflow more convenient. Convenience isn't the sole purpose of label sync, however. It will also keep our PR's and issues in an unambiguous state.

The bot will be activated in several steps. These are tracked in issue #35937. The first step activates the bot on the close event of a PR. This will happen next Tuesday. Please post any comments, suggestions and bug reports to this issue.


Sebastian

[Kwankyu Lee]

Look at the action of the synchronization workflow in the recently merged PR

https://github.com/sagemath/sage/pull/35997

(the last part). The workflow works well on the close event!

[Kwankyu Lee]

Personally, I want the feature to keep at most one status(state) label for a PR, so that if a person add a new status label (say "positive review"), then the old one ("needs review") is automatically removed. Currently it is annoying to do this manually.  

[seb....@gmail.com]

I've added a comment to issue #35927 to enable a next step accordingly. More information about what will change in this step can be found there.

[Kwankyu Lee]

How is this going?

[seb....@gmail.com]

Tobias activated the functionality today (see https://github.com/sagemath/sage/issues/35927#issuecomment-1703696369).

[Kwankyu Lee]

Thanks.

I noticed one defect (nothing serious). For "closed" event, the message is succinct. 

-------------------------------------------

-------------------------------------------

Now for adding status label ("s: needs work"), the message is 

-------------------------------------------

-------------------------------------------

I think this is too verbose. In particular, the message "kwankyu requested changes for this PR" is redundant. 

[Kwankyu Lee]

Note that "github-actions[bot]" in Reviewers. What does this mean? I don't understand how this happened...

 Could this be somehow related with the recent synchronization turn-on?

____________________________________________________________________________

[Dima Pasechnik]

well, obviously such a bot needs some sort of permissions. 

The present problem with this is also with permissions - reviews from non-admins are just comments, from GitHub's point of view, and in our development model this is not what's needed.

--
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 on the web visit https://groups.google.com/d/msgid/sage-devel/c63824aa-4430-45c3-9165-cbfc180ffd13n%40googlegroups.com.

[seb....@gmail.com]

> I think this is too verbose. In particular, the message "kwankyu requested changes for this PR" is redundant.

From the point of view of a developer familiar with Trac status labels, I agree. However, a key goal of the GitHub migration was to attract new developers who are familiar with the GitHub workflow but have no knowledge of Trac. The comment will show them that the label  s: needs work is used as a synonym for request changes. However, note that the comment is the body of the request changes review which cannot be omitted:


gh pr review 35172 -r
body cannot be blank for request-changes review

[seb....@gmail.com]

> Note that "github-actions[bot]" in Reviewers. What does this mean? I don't understand how this happened...
>
> Could this be somehow related with the recent synchronization turn-on?

Yes, since the GitHub state request-changes was not set before you add the s: needs work label the bot sets it for you. Of course it would be much nicer if the bot would set your name into the reviewer field (making the comment indeed redundant). But, this seems to be impossible (even via the REST API).

At the moment the labeled-trigger is disabled again by reasons indicated in Dima's post (for more information see this comment in #36177 and the following). I've opened PR #36213 to treat issues that have been observed in connection with the labeled event.

[Kwankyu Lee]

For a case where it's not done cleanly, see 

https://github.com/sagemath/sage/pull/36020#issuecomment-1722629380

[Kwankyu Lee]

On Friday, September 8, 2023 at 5:47:30 PM UTC+9 seb....@gmail.com wrote:

> I think this is too verbose. In particular, the message "kwankyu requested changes for this PR" is redundant.

From the point of view of a developer familiar with Trac status labels, I agree. However, a key goal of the GitHub migration was to attract new developers who are familiar with the GitHub workflow but have no knowledge of Trac. The comment will show them that the label  s: needs work is used as a synonym for request changes. However, note that the comment is the body of the request changes review which cannot be omitted:

OK. Shouldn't it be "@kwankyu"? 

[Kwankyu Lee]

In a message of https://github.com/sagemath/sage/pull/36020#issuecomment-1722629380, 

please change to "state label" (or "status label" which I prefer) from "state-label".

[seb....@gmail.com]

See the comment in #36213.

[seb....@gmail.com]

Yes. This will be done in PR #36292.

[seb....@gmail.com]

I don't understand what you mean here. Can you please explain this in the new PR.