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").
--
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 [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/sage-devel/542b30fc-91c7-431a-b18e-cd9cbe7170a4%40ucalgary.ca.
