Hi folks, what do you think about changing the kind: infrastructure
tag to part: infra
?
Actually that'd work better in terms of part: infrastructure
being almost covered by part: CI
, part: build
, etc...
What is the reason?
"kind: " today has a special status for coq/bot for instance.
kind:
is a mandatory label category to merge a PR. If we remove it (e.g., in favor of part: CI
, part: build
, etc.), this means that we have to always add another kind:
label, such as kind: feature
, kind: enhancement
, kind: fix
. And it's often the case that we don't want to qualify infrastructure work as such IINM...
Good point @Théo Zimmermann , what would be an example of such a change?
For me part: X
vs kind: A
is about "action A on object X"
we have kind: internal
and kind: cleanup
tho
Indeed. I agree in principle with your interpretation and that we are not always consistent.
I wouldn't object to revisiting the labels, even if it requires adapting coqbot BTW.
Does coqbot care about kind: infra
? As far as I know is the only label that seems wrong
At least that's the one I feel most out of sync, the rest of kind seem logical to me
Yes, kind: infrastructure
specifically is also special as it deactivates minimization.
Last updated: Oct 13 2024 at 01:02 UTC