Short version is I am strongly opposed to such a policy, automated or not. It's good to see what code has been contributed but not merged for different issues. We also should not assume unresponsive authors means they have abandoned their PR too since I would say most of us have more limited time than we wish to contribute.
IMO, GH is quite cluttered and generally horrible for organization of things like this (in particular, their PR/issue search is severely lacking), but we can't do too much about that I'm afraid. On Thursday, January 23, 2025 at 2:20:43 PM UTC+9 Nils Bruin wrote: On Wednesday, 22 January 2025 at 20:30:46 UTC-8 jackson...@gmail.com wrote: I had a similar thought but didn’t know if it was possible. I don’t really understand the idea of being religious about not touching someone’s PR if they were the one that opened it. Surely just getting the code finished and merged is more important, and being able to rebase rather than abandoning seems like a good idea. The conversation on the PR is part of the sagemath repo, so team members can for the most part comment there. The code, however, resides in a fork that is owned by the person who made the PR. You can't really expect to be able to push updates to that branch. "Taking over" a PR on trac meant one would connect a different branch to the ticket. I'm not sure github allows that. Unfortunately that is the case. PRs are directly linked to branches. However, as Nils said, you can at least pull a PR's branch into your own fork and then create a new PR based on that. So the new PR then "replaces" the old one. It looks like "allow edits by maintainers" goes some way to alleviating these problems (see https://github.blog/news-insights/product-news/improving-collaboration-with-forks/), but I expect we don't have enough "maintainers" to really make this useful (only people with push privilege on the sagemath repo would qualify). Elevating people to maintainers gives some very special privileges beyond that IIRC. It likely If you'd know beforehand that there are several people who'll be working on a PR it should be possible to just make a fork where all these people are given push privilege. But that requires some advance planning which wouldn't help these after-the-fact resuscitation endeavours. There's always the option of forking the PR branch and make a new pull request from that. The git metadata would still accurately reflect authorship of the earlier commits. It would lead to a discontinuity in the discussion history, though, and it could give people the feeling their "PR" was stolen if they're more concentrated on PR authorship than commit authorship. For posterity, the git commit data is much more important but in github the PR discussions are much more visible, so it's not unlikely people would feel strongly about PR authorship. Even on trac, where tickets were owned by the organization, people would often feel attached to "their" tickets. Indeed, but I think that is a fairly unlikely to happen. GH's model makes it even more difficult in some ways to have such things happen. I probably wouldn't spend much effort thinking about such situations. Best, Travis -- 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+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/sage-devel/7973dd29-4c56-42ab-a886-735e9aac5d96n%40googlegroups.com.
