Labels for closed PRs #35116
Comments
|
Resolution is orthogonal to status. Also |
|
Yes. That is okay. My question (request) is about keeping "positive review" label after a PR is closed as the reason of closing. In this regard, "positive review" status label is kind of a resolution (decision) label. |
|
GitHub already has a distinction between merged PRs (purple) and those that were closed without merging (red). I'd think that the additional |
|
Okay. I am convinced. I removed all "positive review" labels from the merged PRs. Then "merged" event for a PR may trigger removing the status label by the script #187. |
|
You can filter merged PRs (closed PRs with positive review) with |
|
Related question: What about for issues? Those should have the status labels too, correct? At least that is how I am reading the workflow wiki. |
|
No for new issues. Currently only issues converted from trac have status labels (as they were "PRs") |
|
I made some filters in the wiki https://github.com/sagemath/sage/wiki |
We have no reasonable way to filter out the positively reviewed issues then. What do we do when there are multiple PRs to a single issue, including when the PRs only address one part of the issue? Not every trac ticket had a branch (and should be considered equivalent to a PR). Followup: Is Volker responsible for also closing the issues? Is there even a good way to tell when an issue is ready to be closed? |
|
Not related, but as we are here, I also propose to delete "r: worksforme" label, which is not used at all, and can be replaced with "r: invalid". |
We don't review issues as there is no code to be reviewed.
An issue is closed when all associated PRs are closed. An issue with no PR, like this one, perhaps should be closed by the creator or by anyone with the permission after the issue is resolved. |
That is not strictly true. We do have to look at them and decide which ones we will fix. However that is not quite my point. Now obviously someone has the manually check that the issue has been address and close it. Although it is not clear if that is Volker’s responsibility or the triage team. However, without looking at the corresponding PRs, without labels, there is no way to check that the issue has been fixed by positively reviewed PRs. While there would not be many, it would be very useful to not have to filter through them manually.
But who does that?
For this, I think it has been specified that it is the triage team’s duty. On the other hand, for those with a PR, Volker is the one that closes the PR when it is merged, right? So then does he have to do extra work to verify that indeed the corresponding issue is resolved and close that? Otherwise it becomes hard for someone else to keep track of when PRs are closed and a corresponding issue should be closed. |
Yes.
No.
The creator of the issue or a reviewer may close it after the linked PRs are merged. The status of the linked PRs are displayed in the issue. |
The creator of the issue generally would not have the power to close the issue as I understand it. Even if they did (and were paying enough attention to the PRs to say it was closed, which I would have no expectation that the person reporting the issue is the one is involved with fixing it), it is easy enough to forget to close an issue after a few weeks of getting that the PR has been closed and merged. I believe this will lead to a lot of orphaned issues that will be looking for closure. In fact, I am not even sure I have closed the issues that have had PRs. How would we even find out about such issues that have had at least one (or all) associated PRs that have been closed? |
|
If a PR references an issue using the format "Fixes ", then github automatically closes the issue when the PR is merged. |
|
While that is less likely to cause problems, it means that there is one and only one PR that can be associated to an issue. |
|
How robust is this as well? Does "Fixes" (with that capitalization) need to be in the PR title? At the start? We might need to change our recommended PR formatting. |
Yes. There should be one linked PR with "Fixes #12345" for the issue "#12345". If there are multiple such PRs, closing one of them closes the issue. In this sense, those PRs compete for the issue. If a PR partially solves an issue, perhaps it should be linked to the issue by "Fixes part of #12345" or "Fixes the item 1 of #12345". Closing this PR does not closes the issue. I think this is related with the workflow for meta issues. |
No. See the revised PR template in #35141. |
|
I am assuming by "closing a PR" you are meaning that it is merged-and-closed and not just closed (and not merged). So what happens if there is issue X, and you fix part A and I fix part B. We then have to share our code sometime and combine it into one PR? To me, this system strongly discourages us from having two independent (but possibly interlinked) PRs. How are we suppose to share code? For competing PRs A and B, let's say we adopt B (which means we are disregarding A), who is responsible for closing A? |
Yes. I meant that.
They can be reviewed and merged separately. You may put "Fixes part A[B] of X" to each of them. This is my idea. @tobiasdiez may know the established workflow, if there is one.
The release manager after a review with a resolution label (perhaps "r: duplicate"?) |
|
Closing as resolved. |
We keep labels added to a PR after it is closed, except the status (state) label, in particular, "positive review" label. This seems a trac tradition. Recently the "positive review" labels for closed PRs were mass removed.
But I think, as we keep labels explaining why it is closed, that is, the resolution labels "invalid", "wontfix", "duplicate" etc., in the same vein, we should keep the "positive review" label.
Is there a reason different from trac tradition to remove the "positive review" label?
The text was updated successfully, but these errors were encountered: