splice-bot

Stream: mathlib4

[Damiano Testa]

Recently, there is a new automation for splitting one file from a PR to a separate PR.

If you add a comment attached to a range of at least one line in a GitHub comment and the comment contains splice-bot as the start of one of the lines, then a bot will create a PR with just the selected file extracted and comment on the original PR, linking the newly opened PR.

The bot listens to all reviewers and maintainers, as well as the PR author.

This bot has not been tested very much, so please report any misbehaviour!

[Damiano Testa]

See https://github.com/leanprover-community/mathlib4/pull/34215#discussion_r2857794663 for the bot in action.

[Adam Topaz]

@Damiano Testa looking forward to using it! To confirm: I assume PR branches will have to merge upstream/master in order for reviewers to utilize this bot, is that right?

[Bryan Gin-ge Chen]

I think it should work without merging master, actually. It also tries to rebase the changes in the file onto the latest master automatically, but that might not always work if there are conflicts, etc.

[Eric Wieser]

There's no way for a contributor to modify the split PR, is there?

[Bryan Gin-ge Chen]

Only reviewers and maintainers have write access to the fork that the split PR is made from. However, other contributors can still make suggestions on the split PR.

[Bryan Gin-ge Chen]

I've been getting feedback that a command like splice-bot merge (available only to maintainers) which would have the bot create the PR and automatically put the auto-merge-after-CI label on the PR would be a welcome feature, so I'll be looking into adding that sometime next week.