Stream: coq-community devs & users

Topic: handling unmerged important PRs


view this post on Zulip Karl Palmskog (Oct 12 2020 at 08:07):

@Théo Zimmermann so I think we have to own up to that these PRs might be stuck an undefined interval unless we intervene:

view this post on Zulip Karl Palmskog (Oct 12 2020 at 08:09):

what policy should we have for this in practice? Maybe there should be a timeout set by a bot somewhere?

view this post on Zulip Karl Palmskog (Oct 12 2020 at 08:12):

I would honestly feel better about mechanizing interventions, e.g., PRs marked "important" will go through some stages before being explicitly delegated to handling by others

view this post on Zulip Théo Zimmermann (Oct 12 2020 at 08:14):

The manifesto explicitly says that other coq-community members may step in when maintainers do not respond.

view this post on Zulip Théo Zimmermann (Oct 12 2020 at 08:15):

What I'm more worried about is whether this means that these projects should be considered unmaintained.

view this post on Zulip Karl Palmskog (Oct 12 2020 at 08:18):

right, there's no question interventions have been flagged up as possible, but I think we need more specific guidelines.

view this post on Zulip Paolo Giarrusso (Oct 12 2020 at 08:58):

Probably I miss sth, but maintainers might also have (mentally) classified those PRs as “unimportant”. They seem to mostly affect the coq-community infrastructure?

view this post on Zulip Paolo Giarrusso (Oct 12 2020 at 08:59):

doesn’t mean the projects are maintained, but those PRs don’t look important to me... (FWIW)

view this post on Zulip Karl Palmskog (Oct 12 2020 at 09:02):

@Paolo Giarrusso so what constitutes important updates in your book? Personally, I consider having non-stale links in a README important

view this post on Zulip Paolo Giarrusso (Oct 12 2020 at 09:07):

Webpages of most academics seem to disagree, but my book doesn’t matter.

view this post on Zulip Paolo Giarrusso (Oct 12 2020 at 09:07):

Ditto for mailboxes


Last updated: Mar 28 2024 at 17:01 UTC