easy label

[felixpernegger]

FYI: Inspired by mathlib, I added an "easy" label.

We can use this for straightforward arguments (i.e. NOT having to read outside reference or introduction of new space /property).
This might help us review a bit faster.

[Moniker1998]

Oh I see. Well it would be nice to get everyone's agreement on this first before we start doing this as a practice.
I'm not opposed to this myself. Although do note that it's not immediately clear if a PR needs a reference or not.
We might add it later, generalize it which will mean it has to need one. Etc.

@prabau @yhx-12243

[prabau]

@felixpernegger Tell me again how that label would help in reviewing things?

We can try and see how it goes. Let's be careful to only use that label for things that are really easy. Sometimes things turn out more complicated than they seem.
But I agree for example that #1566 that you had labeled as easy was indeed easy.

[prabau]

@Moniker1998 Talking about labels, we are used to label issues with space/theorem/property, etc, which roughly matches the templates used to create the issue.
Lately you have been marking PRs also with such labels. I am not sure there is a benefit for PRs. What is that adding exactly?

[Moniker1998]

@prabau it makes it so that it's easier to see roughly what we're adding in PR's without reading the titles.
Maybe it doesn't help you, but it helps me. To me it also indicates which PR's should be prioritized, and how much time it will take to add it, roughly.
Theorems to me should be prioritized, traits after, then properties and then spaces.
(adding new spaces and properties is more important than adding traits, but it also comes with more energy that we need to spend on them and that is not very favourable)

Of course this is all roughly how it is, since as we've seen some PR's involving traits and even meta-properties require actual theorems, but not pi-base type theorems.

[felixpernegger]

@felixpernegger Tell me again how that label would help in reviewing things?

We can try and see how it goes. Let's be careful to only use that label for things that are really easy. Sometimes things turn out more complicated than they seem. But I agree for example that #1566 that you had labeled as easy was indeed easy.

As we only have 4 people who contribute and not many PR's admittedly, there isn't a big difference whether we have an easy label or not. However an easy label helps to quickly identify what PR's can be merged quickly, for example #1200 was open for over 10 months, which it likely would not have been without this label.

My motivation is, that when I made a PR on mathlib and added the easy label, it got reviewed in less than 2 days while another PR of similar size is still waiting in the review queue for over 2 weeks. So I think it is just a good practice in general to move quicker.

[felixpernegger]

@Moniker1998 Talking about labels, we are used to label issues with space/theorem/property, etc, which roughly matches the templates used to create the issue. Lately you have been marking PRs also with such labels. I am not sure there is a benefit for PRs. What is that adding exactly?

I agree with @Moniker1998 that this is a good thing to do. It is basically not additional work to quickly add a label but helps keep a better overview.

[Moniker1998]

@felixpernegger I can see how this might be useful, but at the same time I think it would confuse me

[felixpernegger]

@felixpernegger I can see how this might be useful, but at the same time I think it would confuse me

I just thought like: Add one simple simple theorem or (a few) simple traits, which dont require background knowledge and ideally can be written up in pi base itself, then this should deserve "easy" label, for example #1566, #1200 or even #1558 (at least how it was written in the end). One counterexample would be #1565, since it requires a proof of a paper which is over a page long or basically every time we introduce a new space.

We don't need some strict rules we this of course, just a vague guideline in the wiki maybe. In the mathlib contribution guide (which is of course much more detailed and so on than pi base) it is for example described as:
The easy label should be used to mark PRs that can be immediately approved. Maintainers and reviewers often look at easy PRs first to keep the queue flowing. Easy PRs typically add a single lemma, correct typos in documentation, or similar. If you have any doubt whether your PR is trivial, you should not add this label. In particular, a PR is generally not easy if the diff is more than 25 lines, it changes any existing definitions or theorem statements, it adds any definitions or new files, or it adds any simp lemmas or instances that are not immediately analogous to existing simp lemmas or instances. (If they are immediately analogous, you should put such context in the PR description anyway.) Note that a small diff does not automatically make a PR easy!

[Moniker1998]

Okay so I assume you know how that label should work. @prabau do you understand how that label should work?
Would you two assign it to yourself to put those tags on PR's? So that we are consistent?

[prabau]

I understand, and I am ok with using both the easy label and the theorem/space/etc labels.

[prabau]

And I would assume it's the author of the PR who would decide to put the easy label.
If another reviewer looks at the PR without the label and finds it "easy", they might as well review it directly.

[felixpernegger]

And I would assume it's the author of the PR who would decide to put the easy label. If another reviewer looks at the PR without the label and finds it "easy", they might as well review it directly.

I agree. Once again this should not be viewed as anything strict, I just think it is nice to have. @Moniker1998

[prabau]

We don't need some strict rules we this of course, just a vague guideline in the wiki maybe. In the mathlib contribution guide (which is of course much more detailed and so on than pi base) it is for example described as:
The easy label should be used to mark PRs that can be immediately approved. Maintainers and reviewers often look at easy PRs first to keep the queue flowing. Easy PRs typically add a single lemma, correct typos in documentation, or similar. If you have any doubt whether your PR is trivial, you should not add this label. In particular, a PR is generally not easy if the diff is more than 25 lines, it changes any existing definitions or theorem statements, it adds any definitions or new files, or it adds any simp lemmas or instances that are not immediately analogous to existing simp lemmas or instances. (If they are immediately analogous, you should put such context in the PR description anyway.) Note that a small diff does not automatically make a PR easy!

Yes, feel free to add something to the wiki. It's a little long maybe, but a good description.

For the first sentence, how about: The easy label can be used to mark PRs that would not require much discussion and could be easily approved. (I don't like "immediately approved", which makes it seems that the reviewer will be implicitly pressured to approve right away.)
Also, the cutoff of 25 lines seems a bit too much. How about keeping it vague, maybe something like: "... not easy if the change involves too many lines" ?

[felixpernegger]

Alright, I will write something in the wiki later.
The text I copied is just from mathlib, where there are of course different demands. I think we could have looser rules.