Label PRs and issues accordingly

[vmayoral]

@mlautman and @davetcoleman, can you consider labeling Pull Requests and issues accordingly?

I've been reviewing a few of the ongoing PRs and I'd love to tag them with a ToReview whereas I'd appreciate if you could tag those that you already reviewed and that need more work with such a label (e.g. NeedsWork).

To speed up the process, can you give @anasarrak and myself (@vmayoral) rights to label stuff?

[davetcoleman]

From our experience, labels like the ones you suggested quickly become out of date. For example, as soon as someone does a review, they must also remember to remove that label. Instead, we typically just use "WIP" in the title of the PR, which you can easily do through the Github web interface.

Overall, let's just focus on merging PRs quickly so that we don't need labels.

[vmayoral]

I can't say I agree with this. It certainly will help the reviewing process of the PRs and facilitate our work. Every time I open the PRs I need to manually navigate through them to get an intuition of what's requested and the status of it. Some simple labeling would help very much. I'm happy helping maintain this.

Overall, let's just focus on merging PRs quickly so that we don't need labels.

I understand this is the philosophy but it's not what's happening. We have PRs with 60+ comments, several of which pointed towards actions that weren't compiling or points discussed in other issues.

Please reconsider it.