Gaëtan Gilbert (Jun 07 2021 at 09:36): Gaëtan Gilbert (Jun 07 2021 at 09:36):Is it time to remove this script? We have @coqbot: merge now to replace it, and having 2 ways to merge is kinda strange
Pierre-Marie Pédrot (Jun 07 2021 at 09:37):AFAIK the author of the merge is still not taken into account by coqbot
Pierre-Marie Pédrot (Jun 07 2021 at 09:38):this should be fixed before removing the script
Michael Soegtrop (Jun 07 2021 at 09:38):I would appreciate some documentation on what coqbot does in case of warnings or errors - e.g. what it enforces. For merge-pr.sh this is more obvious and one always can decide against the final push.
Gaëtan Gilbert (Jun 07 2021 at 09:39):Pierre-Marie Pédrot said:
AFAIK the author of the merge is still not taken into account by coqbot
it is
see our latest merge commit https://github.com/coq/coq/commit/19b489a7f87928dcfe0687c7dd9bef4ed7aaebed
Pierre-Marie Pédrot (Jun 07 2021 at 09:40):where is the relevant data?
Pierre-Marie Pédrot (Jun 07 2021 at 09:41):I don't see anything with git log
Gaëtan Gilbert (Jun 07 2021 at 09:41):the Co-authored-by in the commit message
Pierre-Marie Pédrot (Jun 07 2021 at 09:41):ah, ok
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.
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
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).
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).
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.
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.
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?
Michael Soegtrop (Jun 07 2021 at 12:55):@Théo Zimmermann : I will draft something and you correct it in case.
Théo Zimmermann (Jun 07 2021 at 12:56):Great, thanks!
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?
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: Sep 15 2024 at 13:02 UTC