bikeshed: Labeling linter PRs with "feat"?

Stream: mathlib4

[Michael Rothgang]

In #13220, a question came up between @Yaël Dillies and me: how to label a PR adding a new linter? There are two reasonable positions here:

• "feat" is only for new mathematical content, so this should be labelled something like "chore"
• This is a new feature in the "linters" category. (We even have a "t-lint" label now.) So, this should be labelled "feat".

Any opinions on this bikeshed?

[Mario Carneiro]

This is obviously a "feat"

[Mario Carneiro]

there has never been a rule that "feat" is only for maths

[Yaël Dillies]

My reaction was mostly because I've seen clearly chore PRs being labelled as feat recently, so I was a bit worried people understood the convention to be "Start your PR title with feat:"

[Mario Carneiro]

not sure how to comment on that without knowing what the "clearly chore PRs" are. What is "clearly chore" to you?

[Yaël Dillies]

eg #13015, #13002, #12431, #12423, #12289, #12023, #11980, ...

[Yaël Dillies]

Not claiming all should be chore. Most of them should be refactor instead

[Michael Rothgang]

Arguably, generalising a proof could be a feature - but for mathematically trivial generalisations, using refactor seems better indeed.

[Eric Wieser]

I was under the impression that refactor was for non-trivial generalizations