remove "RM-Approved" and "reviewed" labels when a PR is synchronized

[ggouaillardet]

since it is possible to push new commits into a PR even after it has been reviewed and/or RM-Approved,
remove these labels each time a PR is synchronized (aka commits have changed)

assign: @jsquyres
label:enhancement

[jsquyres]

Nifty!

I'm going to ask the OMPI dev community if they want this. I think it sounds like a good idea, but let's make sure they want it.

We might actually want to modify the workflows a little:

• When receiving new commits on a PR, remove "rm-approved" and "reviewed", and add the "pushed-back" label. This means that there is a positive feedback loop (i.e., it's not just that "reviewed" disappeared -- you get a positive signal that something happened: "pushed-back").
• When adding "reviewed", remove the "pushed-back" label.

I'll ask the community.

[jsquyres]

Ok, per community discussion, let's have this PR do the following:

• When new commits are pushed to a PR:
  • Remove the reviewed label if it exists
  • ON THE v1.8 BRANCH: Remove the rm-approved label if it exists.
    • NOTE This should probably be some kind of top-level config variable (e.g., if the PR involves the "v1.8" branch, set some kind of global saying "yes, additional PR commits remove the rm-approved label"). This allows us to have a different policy on the v1.9/v2.0 branches, if we want it.
  • If either of those labels were removed, add the pushed-back label
• When someone adds the reviewed label
  • If the pushed-back label is set, remove it
• When someone adds the rm-approved label
  • If the pushed-back label is set, remove it

Cool?

[ggouaillardet]

@jsquyres is there an indentation issue ?

i read "When new commits are pushed to a PR, If either of those labels were removed, add the pushed-back label"

if a new commit is pushed to a PR, this means an other review is required, so why put the pushed-back label ?

also, when setting the pushed-back label, should the assignee be updated automatically ?
for example, i make a PR and assign to you.
you reject it by setting the pushed-back label, should the PR be assigned to me ?
if yes, when i fix my stuff, push new commits and assign it to you for a second review,
should the "pushed-back" label be removed automatically ?

[jsquyres]

The intent for the "pushed-back" label is just a visual indicator to the submitter / reviewer that the PR has been pushed back to them (i.e., away from the RM). So when they add a commit (for example), the PR gets pushed back to them for additional review. It's just a positive signal, vs. a negative signal of the "reviewed" label disappearing.

For assignee: mmm. Good point; I hadn't thought about automatically assigning the user assignment.

...I thought about this for a few minutes, and my conclusion is: I don't know. :-) I therefore think we probably shouldn't do it. Meaning: let's let this system loose on the community for a while and let's see how people use it. If there are common actions that people are doing (e.g., adding/removing pushed-back, assigning/unassigning owners), they we can slurp that into the bot.

Make sense?