Stream: Coq devs & plugin devs

Topic: `merge-pr.sh`?


view this post on Zulip Michael Soegtrop (Jun 07 2021 at 10:17):

How about the documentation? Is there something I haven't seen yet? The Contributing.md file just says that it exists. Not that merge-pr.sh would have documentation, but I know what it does.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 07 2021 at 11:33):

Merge PR is still useful for backports and other stuff that the bot doesn't handle I think ; also, I don't like to depend on the bot without a fallback

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 11:46):

@Michael Soegtrop coqbot does not have warnings: it refuses to merge in some cases (no assignee, no kind label, left-over needs label, no milestone, author merge their own PR) but it doesn't check the status of CI (it assumes that the merger did it since it's right in front of their nose).

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 11:47):

However, @Gaëtan Gilbert we shouldn't remove the merge script because it's still needed to merge in release branches (coqbot doesn't do that yet).

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 11:47):

We could add a warning to the merge script saying: you are merging in master, why don't you use the bot.

view this post on Zulip Michael Soegtrop (Jun 07 2021 at 12:37):

@Théo Zimmermann : thanks! I think this information should go here:(https://github.com/coq/coq/blob/master/CONTRIBUTING.md#additional-notes-for-pull-request-reviewers-and-assignees). I will give coqbot a try next time.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 12:38):

@Michael Soegtrop Can you open a PR with the additional info you'd like to see, or open an issue and assign me to it?

view this post on Zulip Michael Soegtrop (Jun 07 2021 at 12:55):

@Théo Zimmermann : I will draft something and you correct it in case.

view this post on Zulip Théo Zimmermann (Jun 07 2021 at 12:56):

Great, thanks!

view this post on Zulip Michael Soegtrop (Jun 08 2021 at 12:50):

@Théo Zimmermann : i am just doing the PR. One question: reviewers are allowed to do minor changes to a PR and still merge themselves according to the rules (afaik). Can you elaborate on what coqbot actually checks? Say just the main author? Are minor corrections by reviewers still possible?

view this post on Zulip Théo Zimmermann (Jun 08 2021 at 12:57):

Yes, coqbot does a very dumb check: it looks at the author of the PR according to GitHub, not according to the commit it contains.


Last updated: Oct 21 2021 at 21:03 UTC