Stream: Coq devs & plugin devs

Topic: coqbot closing PRs


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2021 at 15:33):

Actually something seems borked, as the draft PRs weren't closed.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Aug 25 2021 at 15:34):

@Emilio Jesús Gallego Arias yeah, the bot seems to have gone postal today

view this post on Zulip Pierre-Marie Pédrot (Aug 25 2021 at 15:34):

it marked more PRs than the allowed limit and did weird things

view this post on Zulip Pierre-Marie Pédrot (Aug 25 2021 at 15:34):

probably some bug in the code, sorry about that

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Aug 25 2021 at 15:38):

otherwise we just get a junkyard of slowly bitrotting code, as empirically observed

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2021 at 17:22):

I agree with @Enrico Tassi

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Sep 24 2021 at 08:34):

you can always open a new PR with the rebased branch

view this post on Zulip Hugo Herbelin (Sep 24 2021 at 08:37):

you can always open a new PR with the rebased branch

Ok, doing it.

view this post on Zulip 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?

view this post on Zulip 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."

view this post on Zulip 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: Oct 15 2021 at 20:02 UTC