Rejected PRs

Stream: mathlib4

[Winston Yin (尹維晨)]

Given the observation that the #queue is getting longer, and after reading through a few old PRs myself, I wonder if there should be a new github tag for PRs like #7449, which are written nicely with the best intentions but are not accepted by reviewers. Perhaps the feature already exists, or the kind of contribution is inconsistent with mathlib's project philosophy (e.g. not general enough / unjustified new definitions). I've written quite a few of PRs like that as I'm learning, but I usually close them myself sometime after the review.

A new github tag has the following benefits:

• "awaiting review" can be removed, so the queue won't be cluttered with PRs in limbo, wasting reviewers' time.
• It clearly indicates that the review has been done sufficiently without stringing the author along. "awaiting author", if applied for such PRs, could mislead the author to do unnecessary work on something that won't be merged.
• After a set amount of time (e.g. 3 months), such PRs can be closed automatically (but keeping the branch for longer).

However, it has the following risks:

• It may come off as very harsh, potentially discouraging new contributors.
• A different reviewer might disagree with the rejection, thus tossing away hard work that can be useful.

I believe the risks can be reduced / avoided if each application of this tag comes with a delicate and polite message, stating why it is rejected and what could be written in its place, if any. For example, the review on PR #7449 could have been more polite.

Now that I made the suggestion, what could this tag be called? Words I would not want to see on the receiving end are "rejected" and "unfit for mathlib". Perhaps "shelved"?

[Kim Morrison]

A "functional" label like closing soon seems much better than any descriptive label, which someone will inevitably choose to interpret the wrong way.

[Alex J. Best]

I think we already have #wontfix right? But I think Scott's suggestion is reasonable also.

[Yaël Dillies]

For #7449 in particular, the author had been ignoring my more polite comments across several PRs already. Also note that I do not intend that PR to be closed. What I want to do is go through the other PRs and sort out what needs to be done to avoid defining Function.toval. I just haven't had time yet.