Autolabel PRs

[felixpernegger]

I think it would be nice if we could set up https://github.com/actions/labeler to make a github action to autolabel PRs (this is very doable).
For example the following way:

• If theorem file is touched (or created), add theorem tag
• If README.md file of space is touched add space tag
• If trait is touched, add trait tag

I often find myself adding tags to PRs opened by others.
Having this action would make the contribution process a tiny bit smoother I think :)

[prabau]

Possibly. But consider this sample scenario. A PR is adding some traits to a space and at the same time something was not well expressed and a minor clarification is made to the README for the space. The PR should have the trait tag, obviously, but the autolabel would also tag this as space, which is kind of misleading. One could think of other cases where the PR contains a minor tweak belonging to a different type than the main focus of the PR.

One could manually undo the autolabel of course.

But when changes are added to a PR, will the autolabel kick in for every additional change as well? If so, one may need to manually undo it again?

[felixpernegger]

Possibly. But consider this sample scenario. A PR is adding some traits to a space and at the same time something was not well expressed and a minor clarification is made to the README for the space. The PR should have the trait tag, obviously, but the autolabel would also tag this as space, which is kind of misleading. One could think of other cases where the PR contains a minor tweak belonging to a different type than the main focus of the PR.

I thought about this, (one could also only add the space tag automatically if a new file gets added for example). In any case, I think the tradeoff is worth it.

One could manually undo the autolabel of course.

Yes

But when changes are added to a PR, will the autolabel kick in for every additional change as well? If so, one may need to manually undo it again?

Im very sure there is a setting for this

[StevenClontz]

I think this is worth trying. If someone else wants to make a PR adding the action and tag me as a reviewer, that might be quicker than waiting on me to figure it out.

[felixpernegger]

I think this is worth trying. If someone else wants to make a PR adding the action and tag me as a reviewer, that might be quicker than waiting on me to figure it out.

Yes I can make it maybe tomorrow

[felixpernegger]

Sorry for assigning, I think that may have come over a bit rude.

[StevenClontz]

I didn't take offense, no worries!