Jason Gross (Mar 23 2021 at 20:17): Jason Gross (Mar 23 2021 at 20:17):Is it possible to set up GitHub to assign milestones to PRs by default? If so, would it make sense to set up Coq to do this (and people who want the PRs backported can manually change the milestone)?
Théo Zimmermann (Mar 24 2021 at 07:51):No, as of today you can use issue templates to auto-set labels and assignees but not milestones. And this only applies to issues, not pull requests, whose templates are limited to a default body.
Théo Zimmermann (Mar 24 2021 at 07:52):We could use the bot to do this though, but I'm not convinced this is useful given that if the milestone is not set it is the job of the assignee to set it before merging.
Théo Zimmermann (Mar 24 2021 at 07:53):What we could do to help the assignee would be to suggest a milestone in the coqbot reply when the milestone was forgotten and the assignee tried to merge.
Jason Gross (Mar 24 2021 at 12:32):Yes, I think suggesting a milestone would be helpful. (Ideally, in cases where there's an option to mark the PR for backporting, coqbot could also let me know whether or not there would be any merge conflicts in backporting the PR?)
Théo Zimmermann (Mar 24 2021 at 14:41):Sure, it could do that. But it's not really a reason for deciding to not backport, is it? Or at least, it should be left to the RM to decide eventually.
Jason Gross (Mar 24 2021 at 22:08):I think that for minor changes (fixing spelling errors, minor doc tweaks, etc), whether or not there are conflicts might be the dominating factor in whether or not to backport them? Is there a guide somewhere for "which milestone should I assign?"?
Théo Zimmermann (Mar 25 2021 at 10:20):PR authors and assignee can signal a desire to have a PR backported by selecting an appropriate milestone. Most of the time, the choice of milestone is between two options: the next major version that has yet to branch from master, or the next version (beta, final, or patch-level release) of the active release branch. In the end, it is the RM who decides whether to follow or not the recommendation of the PR assignee, and who backports PRs to the release branch.
(from https://github.com/coq/coq/blob/master/CONTRIBUTING.md#release-management)
Théo Zimmermann (Mar 25 2021 at 10:20):In the end, it is the job of the RM to decide whether it's worth backporting or not.
Théo Zimmermann (Mar 25 2021 at 10:21):So, the PR author or assignee can just use the milestone to signal an intent.
Last updated: Nov 29 2023 at 19:01 UTC