lean4 repo triage

Stream: lean4

[Sebastian Ullrich]

At the Lean FRO, we want to improve our communication on external contributions, be they bug reports, PRs, or RFCs, and especially more clearly communicate the priority by which we plan to address such a contribution. Please see Reviews and Feedback in the contribution guidelines for details on this new triaging process that has now started.

[François G. Dorais]

I'm confused about the meaning of this part:

Accepted RFCs are marked with the label RFC accepted and afterwards assigned a new "implementation" priority as with bug reports.

Why is the word implementation in quotes here? It's also unclear exactly what "as with bug reports" is referring to: the interpretation of the new priority or the assignment process itself.

[Joachim Breitner]

Let me try to repharase: An accepted RFC becomes an open bug.
So while an RFC is not accepted the priority indicates how pressing we think it is to discuss the RFC and decide upon a design (or against the RFC). Once accepted, there is coding to do.
It’s feasible that some RFC looks important, but then the discussion shows that there is something to do (so we have an accepted design), but actually not that pressing (maybe good work-arounds have been demonstrated), so actually implementing the RFC is not of high priority.

[François G. Dorais]

That's much clearer but perhaps too detailed. Let me take a stab at something short and still clearer than the original:

Once a RFC is marked with the label RFC accepted, it will be assigned a new priority that reflects our commitment to implementing the proposal (similar to fixes for bug reports).

[François G. Dorais]

Another small issue. Since label changes don't ping anyone (including the OP), perhaps RFC accepted should be accompanied by a comment? (A message is not necessary for priority assignments since those are now expected.)

I recently had a RFC (lean4#4654) marked RFC accepted but I had no clue until I checked on the RFC to record the number. It's only by chance that I noticed the new label. I can easily imagine a RFC accepted label going unnoticed for a very long time.

[Joachim Breitner]

That's a good point. Maybe that can be integrated into our automation for this process that @Sebastian Ullrich is putting together