Jason Gross (Aug 25 2021 at 15:30): Jason Gross (Aug 25 2021 at 15:30):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.
Pierre-Marie Pédrot (Aug 25 2021 at 15:32):FWIW, I specifically insisted for the bot to also take draft PRs into account, with some argumentation.
Pierre-Marie Pédrot (Aug 25 2021 at 15:33):The sad reality is that we have a lot of draft PRs that are not being worked on anymore.
Emilio Jesús Gallego Arias (Aug 25 2021 at 15:33):Actually something seems borked, as the draft PRs weren't closed.
Pierre-Marie Pédrot (Aug 25 2021 at 15:34):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.
Pierre-Marie Pédrot (Aug 25 2021 at 15:34):@Emilio Jesús Gallego Arias yeah, the bot seems to have gone postal today
Pierre-Marie Pédrot (Aug 25 2021 at 15:34):it marked more PRs than the allowed limit and did weird things
Pierre-Marie Pédrot (Aug 25 2021 at 15:34):probably some bug in the code, sorry about that
Pierre-Marie Pédrot (Aug 25 2021 at 15:37):anyways, about the closure of draft PRs: I believe PRs need attention to reach "escape velocity" to make it into the code
Pierre-Marie Pédrot (Aug 25 2021 at 15:38):otherwise we just get a junkyard of slowly bitrotting code, as empirically observed
Pierre-Marie Pédrot (Aug 25 2021 at 15:38):having a bunch of dead draft PRs is taking a heavy toll on the relative attention given to the whole set of PRs.
Pierre-Marie Pédrot (Aug 25 2021 at 15:39):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
Enrico Tassi (Aug 25 2021 at 17:20):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.
Emilio Jesús Gallego Arias (Aug 25 2021 at 17:22):I agree with @Enrico Tassi
Théo Zimmermann (Aug 25 2021 at 17:34):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.
Hugo Herbelin (Sep 24 2021 at 08:06):Is it normal that I cannot reopen a PR closed by the bot after I rebased it? Should I reopen a new one?
Pierre-Marie Pédrot (Sep 24 2021 at 08:07):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.
Hugo Herbelin (Sep 24 2021 at 08:16):Reverting to the same commit does not seem to work either. It says the branch was forced-pushed.
Enrico Tassi (Sep 24 2021 at 08:34):you can always open a new PR with the rebased branch
Hugo Herbelin (Sep 24 2021 at 08:37):you can always open a new PR with the rebased branch
Ok, doing it.
Théo Zimmermann (Sep 24 2021 at 09:14):Yeah, that's quite annoying. I considered modifying the closing message to alert about this. Do you think it would be useful?
Guillaume Melquiond (Sep 24 2021 at 09:20):Something like the following? "If you intend to resuscitate this pull request, reopen it BEFORE rebasing the branch. Otherwise it will become stuck."
Emilio Jesús Gallego Arias (Sep 24 2021 at 15:58):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: Jun 08 2023 at 04:01 UTC