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)?
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.
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.
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.
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?)
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.
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?"?
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.
In the end, it is the job of the RM to decide whether it's worth backporting or not.
So, the PR author or assignee can just use the milestone to signal an intent.
Last updated: Oct 15 2021 at 21:02 UTC