Going live of sync_labels #35927
Description
Problem Description
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 GitHub bot that will supervise our state and priority labels has been implemented in #35172, #36213 and #36292 and has already been merged into the develop branch. At the moment the bot is completely disabled in order not to confuse you with a sudden change in behavior when working on PRs and issues. Our plan is to activate it in several steps. Each step can be one or a couple of GitHub triggers the bot will start to listen to. The following events are possible:
Active triggers
- opening of a PR / issue, bot reaction
- reopening of a PR / issue, bot reaction
- closing of a PR / issue, bot reaction
- labelling a PR / issue, bot reaction
- unlabelling a PR / issue, bot reaction
- marking a draft PR as ready for review, bot reaction
- converting a PR to a draft, bot reaction
- submitting a review to a PR, bot reaction: request changes, approve PR
- synchronizing the branch of the PR (i.e. pushing a new commit or rebasing/merging with
developbranch), bot reaction
The idea is that the bot's current activity status is visible in the checkboxes above. Each change in the activity of the bot will be scheduled and announced a few days before here.
Proposed Solution
Schedule
| step | date | triggers | explanation |
|---|---|---|---|
| 1 | Tuesday July 18th (2023) | closed | #35927 (comment) |
| 2 | stalled | labeled | #35927 (comment) |
| 3 | Tuesday June 11th (2024) | opened, reopened, converted_to_draft | #35927 (comment) |
| 4 | Tuesday June 18 th (2024) | ready_for_review, synchronize | #35927 (comment) |
Currently progress is blocked because of a bug in the GitHub web-interface. For more information see this post on sage-devel or according remarks in the header of #36292. For the current status on this see #35927 (comment).
Alternatives Considered
If the bot causes you trouble, please report it here. If we can't find an acceptable workaround soon, the bot (or the particular event causing the problem) will be disabled.
If you want to make suggestions for the next steps to be activated, please post them here, too.
Additional Information
No response
Is there an existing issue for this?
- I have searched the existing issues for a bug report that matches the one I want to file, without success.