CI for modifies-synchronized-file label

Stream: general

[Alex J. Best]

Regarding 1, why don't we have CI add this automatically for new PRs? We already print a warning for such files, so surely adding the label wouldn't be much extra to implement and would save people forgetting or not seeing the above post.

[Eric Wieser]

Because making the CI to add the label requires a github token, and I didn't want to grant one from my personal account. If we could use github apps instead to authenticate (which is certainly possible) this problem would go away.

[Eric Wieser]

We already have a workflow that detects the modified files. It would be great if it added the label too!

[Alex J. Best]

I guess I'm a bit confused, we already have a lot of actions that do things with labels, why would this one require a personal token?

[Eric Wieser]

Every action that does stuff with labels requires a token I think; we just usually use a bot's "personal" token

[Notification Bot]

5 messages were moved here from #general > New policy regarding mathlib3 PRs that touch ported files by Eric Wieser.

[Alex J. Best]

What do you mean by "a bots" token? I would think using ${{ secrets.GITHUB_TOKEN }} like we do elsewhere would work with no additional setup

[Eric Wieser]

Oh, is that all we do? I thought it didn't have enough permissions to edit issues. I would be very happy for you to prove me wrong by making a PR that adds support for this!

[Alex J. Best]

#18782 seems to work now. Its pretty basic (e.g. if you stop modifying a ported file it won't remove the label

[Yaël Dillies]

It would also be nice to restore the merge-conflict label management.

[Eric Wieser]

I think that was much harder because it had to run on a Cron job and used up our API quota

[Eric Wieser]

Looks like we made a typo in the label name, #18788