On Tue, Sep 2, 2025 at 1:16 PM 'Martin R' via sage-devel <[email protected]> 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. > > Martin > > On Tuesday, 2 September 2025 at 18:53:02 UTC+2 Vincent Macri wrote: >> >> 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/86aad875-baf9-4db0-bbb3-ffa3f4f365b8n%40googlegroups.com. -- 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/CAAWYfq3QdvOCARimr_e83JfkTNpmZ-NJqpCZNUqCASRSyj_2Gw%40mail.gmail.com.
