I think coqbot should ignore draft PRs when closing PRs. Draft PRs are already marked as "unready", and I'm seeing a bunch of PRs with useful features be marked as stale, some of which are already marked as draft.
FWIW, I specifically insisted for the bot to also take draft PRs into account, with some argumentation.
The sad reality is that we have a lot of draft PRs that are not being worked on anymore.
Actually something seems borked, as the draft PRs weren't closed.
The fact that they propose useful feature is orthogonal to the fact that they're nowhere close to being merged since they're left in a derelict state.
@Emilio Jesús Gallego Arias yeah, the bot seems to have gone postal today
it marked more PRs than the allowed limit and did weird things
probably some bug in the code, sorry about that
anyways, about the closure of draft PRs: I believe PRs need attention to reach "escape velocity" to make it into the code
otherwise we just get a junkyard of slowly bitrotting code, as empirically observed
having a bunch of dead draft PRs is taking a heavy toll on the relative attention given to the whole set of PRs.
I am a vocal advocate for having a small set of PRs (that is, pull requests, I insist on both words) that we can concentrate on rather than just letting features die
I personally like the action of the bot. In a few cases I did remove the stale label and reopen the PR, since I believed it was important. But 9/10 times I just acknowledged the lack of time on my side. RIP.
I agree with @Enrico Tassi
Pierre-Marie Pédrot said:
it marked more PRs than the allowed limit and did weird things
Let's address this in a separate thread in the #coqbot devs & users stream.
Is it normal that I cannot reopen a PR closed by the bot after I rebased it? Should I reopen a new one?
GitHub does not let you do that. You need to first reopen it on the same commit, and then rebase. It's quite annoying but it seems to be on purpose.
Reverting to the same commit does not seem to work either. It says the branch was forced-pushed.
you can always open a new PR with the rebased branch
you can always open a new PR with the rebased branch
Ok, doing it.
Yeah, that's quite annoying. I considered modifying the closing message to alert about this. Do you think it would be useful?
Something like the following? "If you intend to resuscitate this pull request, reopen it BEFORE rebasing the branch. Otherwise it will become stuck."
Indeed we all have been bitten by this; it is annoying as you need to track the right hash to force-push :S
Last updated: Dec 07 2023 at 06:38 UTC