Zulip Chat Archive

Stream: PR reviews

Topic: mergify


view this post on Zulip Simon Hudon (Apr 01 2019 at 18:00):

Have you used it before? I'm writing a configuration file now. I can show it here for comments

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:09):

pull_request_rules:
  - name: automatic merge on CI success and review
    conditions:
      - status-success=continuous-integration/travis-ci/pr
      - "#approved-reviews-by>=1"
      - "#review-requested=0"
      - "#changes-requested-reviews-by=0"
      - base=master
      - label=['ready-to-merge']
    actions:
      - delete_head_branch
      - merge:
        method: squash
  - name: remove outdated reviews
    conditions:
      - status-success=continuous-integration/travis-ci/pr
      - "#approved-reviews-by>=2"
    actions:
      - dismiss_reviews:
        approved: True
      - remove: ['ready-to-merge']

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:13):

I'm testing it out on my fork. Can't seem to get it to work. My config file look like

pull_request_rules:
  - name: automatic merge with strict
    conditions:
      - status-success=continuous-integration/travis-ci/pr
      - status-success=continuous-integration/travis-ci/push
      - base=master
    actions:
      merge:
        method: squash
        strict: true

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:16):

What does strict mean?

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:19):

https://doc.mergify.io/strict-workflow.html

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:21):

That's probably best if we automate merges

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:22):

I set those rules, but it still just merged straight away before Travis passed.

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:25):

Both the PR build and the push build?

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:27):

Exactly those rules.

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:27):

I mean, did neither build terminate before the merge?

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:28):

Neither build terminated

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:29):

Screenshot-2019-04-01-at-19.28.42.png Only one box is ticked, but it says success.

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:30):

Is the list of condition a disjunction or a conjunction?

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:30):

Try removing the last condition

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:34):

Now it doesn't tell me anything.

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:36):

That's frustrating

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:36):

Can I let you look into it?

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:36):

But travis has also stopped.

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:37):

I'll have a go at sorting it out.

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:38):

Thanks! Let me know if you need something

view this post on Zulip Johan Commelin (Apr 01 2019 at 18:40):

If this works, it seems like a really good idea!

view this post on Zulip Simon Hudon (Apr 01 2019 at 18:44):

Yes! That could make things simpler. We could merge a branch by clicking "update branch" and adding the label "ready-to-merge". We have to remember to get back to them if they fail to merge though and we can't do more than one PR at a time with this approach

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:46):

What does status-success=continuous-integration/travis-ci/push mean if status-success is an array of strings? Will it fail if the array contains more than just that one string?

view this post on Zulip Chris Hughes (Apr 01 2019 at 18:56):

I know what's going on. "merge" means merge straight away with no further user input. We definitely don't want that. I never clicked "merge" on this PR https://github.com/ChrisHughes24/mathlib/pull/16

I don't think you can set it up to have a "merge when ready" button. You could do some hack, where you add a label to instigate a merge or something like that.

view this post on Zulip Simon Hudon (Apr 01 2019 at 19:00):

I would put that in condition

view this post on Zulip Chris Hughes (Apr 01 2019 at 19:00):

Maybe that was obvious to you, looking at your script.

view this post on Zulip Chris Hughes (Apr 01 2019 at 19:00):

So I think your script is about right, but just with strict added.

view this post on Zulip Chris Hughes (Apr 01 2019 at 19:28):

I setup some test PRs. I set up one of them to break after I changed mathlib. https://github.com/ChrisHughes24/mathlib/pulls Hopefully #20 will merge, but #21 and #22 won't

view this post on Zulip Johan Commelin (Apr 01 2019 at 19:30):

Cool! Let's see what happens.

view this post on Zulip Johan Commelin (Apr 01 2019 at 20:03):

Hmm... it seems that https://github.com/ChrisHughes24/mathlib/pull/20 is ready to merged. But the merge didn't automatically happen

view this post on Zulip Chris Hughes (Apr 01 2019 at 20:03):

It's because Travis failed because it's failing on master.

view this post on Zulip Johan Commelin (Apr 01 2019 at 20:04):

Hmm... ok. Bit weird that it says all the tests passed though. Too bad.

view this post on Zulip Johan Commelin (Apr 01 2019 at 20:06):

Can we see the Travis logs for the failing master builds? I can't find links from Githubs commit log

view this post on Zulip Chris Hughes (Apr 01 2019 at 20:06):

It's weird that the links aren't on the PRs any more.

view this post on Zulip Johan Commelin (Apr 01 2019 at 20:14):

This is the problematic test run: https://travis-ci.org/leanprover-community/mathlib/jobs/513991382

view this post on Zulip Johan Commelin (Apr 01 2019 at 20:14):

The first two stages went fine. Then the "Test" stage timed out because of no output in 10 minutes.

view this post on Zulip Rob Lewis (Apr 01 2019 at 20:15):

Travis is failing at the leanchecker stage since the pi PR. I noticed this earlier but haven't had time to investigate.

view this post on Zulip Simon Hudon (Apr 01 2019 at 20:16):

We have a trick to prevent this kind of issue. Let me take a look

view this post on Zulip Johan Commelin (Apr 01 2019 at 20:17):

If only there were some tool that could automatically and transparently handle these merge issues for us...

view this post on Zulip Rob Lewis (Apr 01 2019 at 20:18):

A tool that figures out what part of a PR is too hard for leanchecker, and fixes it?

view this post on Zulip Rob Lewis (Apr 01 2019 at 20:18):

I'd like that tool too.

view this post on Zulip Johan Commelin (Apr 01 2019 at 20:21):

Well that would be awesome. But I was thinking of a tool that merely checks whether 2 or 3 maintainers approve of a PR, and then waits till the build passes, and then merges.

view this post on Zulip Simon Hudon (Apr 01 2019 at 20:21):

That's what this thread (mergify) is about

view this post on Zulip Simon Hudon (Apr 01 2019 at 20:47):

I wonder if there's a way of automating the update of a PR when no branch is building and that it's marked as ready-to-merge

view this post on Zulip Kevin Buzzard (Apr 01 2019 at 21:30):

Do you want to test this on #854 by marking it ready-to-merge? ;-)

view this post on Zulip Scott Morrison (Apr 01 2019 at 22:05):

We have a trick to prevent this kind of issue. Let me take a look

@Simon Hudon what is this trick? I've several times had trouble with the test stage timing out after 10 minutes, and never known how to diagnose the problem.

view this post on Zulip Simon Hudon (Apr 01 2019 at 22:48):

here is the trick: https://github.com/leanprover-community/mathlib/compare/2f088fc1cb98...5995d460bc69

view this post on Zulip Johan Commelin (Apr 02 2019 at 08:14):

What is the status here? @Chris Hughes Did you rerun your experiment now that master is back on track?

view this post on Zulip Chris Hughes (Apr 02 2019 at 08:15):

Yes. It all seems to be working as expected.

view this post on Zulip Johan Commelin (Apr 02 2019 at 08:16):

That's great news.

view this post on Zulip Johan Commelin (Apr 02 2019 at 11:02):

Can maintainers override the mergify workflow? Or do they always have to abide, once we implement it?

view this post on Zulip Rob Lewis (Apr 02 2019 at 11:51):

I think Simon's setup is opt-in. Giving something the ready-to-merge tag is explicitly approving the mergify workflow.

view this post on Zulip Johan Commelin (Apr 02 2019 at 11:52):

Right. So then I don't really understand @Chris Hughes's concern over here: https://github.com/leanprover-community/mathlib/pull/871#discussion_r271218389

view this post on Zulip Rob Lewis (Apr 02 2019 at 11:54):

It's set up to only auto-merge if there's at least one approving review. For very easy PRs, Chris wants to be able to say "auto-merge this once Travis finishes successfully," without also having to post an empty approving review.

view this post on Zulip Johan Commelin (Apr 02 2019 at 11:55):

Aah, got it

view this post on Zulip Johan Commelin (Apr 02 2019 at 12:56):

@Simon Hudon @Chris Hughes I've fixed the errors with the mergify config. I don't think I diverted from your intentions.

view this post on Zulip Simon Hudon (Apr 02 2019 at 13:05):

nice! Thanks!

view this post on Zulip Simon Hudon (Apr 02 2019 at 13:06):

I'm happy with the current state of the PR. Any objections to me merging?

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:07):

How does the second condition work?

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:08):

Why do you need the review conditions. We want it to remove the label whenever there's a commit, regardless of the reviews.

view this post on Zulip Simon Hudon (Apr 02 2019 at 13:12):

You're right, I'll change it to:

      - base=master

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:12):

And it only triggers after a commit? This isn't what I would expect.

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:14):

I also don't understand the 2nd rule

view this post on Zulip Simon Hudon (Apr 02 2019 at 13:15):

Yeah, it's confusing to me too. Here is where I got it from: https://doc.mergify.io/examples.html#removing-stale-reviews

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:19):

Why is strict_method back to squash?

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:19):

That's not a valid value

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:21):

If it's set to merge, I think all the commits to the PR branch will be in the history of the branch.

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:21):

The question you need to answer is: If pr-branch is outdated, and I need to update it, I will use strict_methodto update pr-branch to current master.
Possible values are rebase and merge.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:21):

I didn't realise squash wasn't a valid value.

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:21):

No, it will still use squash, when it is performing the merge from pr-branch into master.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:21):

I see.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:21):

Then merge is correct.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:22):

I misunderstood.

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:23):

No worries. Btw, merge is the default value. So we can remove that line, if we want.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:24):

Okay, let's do that.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:24):

I just tested the second part on my fork. It does indeed do the right thing.

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:24):

Mergify is now happy: it says that there are no syntax errors in the config file

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:26):

Hmm... the README looks bad: https://github.com/leanprover-community/mathlib/tree/enable-mergify#mathlib

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:28):

There is a problem
https://github.com/ChrisHughes24/mathlib/pull/35
I can't add the ready-to-merge label to this, without mergify immediately removing it.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:29):

In fact I don't think it was behaving as expected at all.

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:30):

The badge in the README is now fixed

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:47):

To me the 2nd rule reads like
if (empty condition) then (remove reviews and remove label "ready-to-merge")

The condition isn't really empty. But it's only testing if we want to merge something into master

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:51):

@Chris Hughes Can you test whether it also dismisses reviews as soon as you make them?

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:53):

I can't make an approving review on my own PR.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:53):

Could you make a PR to my fork, and I'll make an approving review.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:53):

I think maybe it only cares about reviews by admin.

view this post on Zulip Johan Commelin (Apr 02 2019 at 13:56):

Done: https://github.com/ChrisHughes24/mathlib/pull/37

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:58):

It didn't remove it.

view this post on Zulip Chris Hughes (Apr 02 2019 at 13:58):

Now what happens if it's edited

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:07):

If what is edited?

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:08):

I added the tag ready-to-merge, so the event triggered, but it didn't remove the review. I can't edit the PR, because it's from Johan's fork.

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:08):

If there's a commit I meant.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:09):

Ok, I'll make another commit.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:10):

Done

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:11):

Ok, it removed your review

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:11):

So it's going to have to be slightly less nice.

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:12):

We need an approving review, and a tag?

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:12):

This means we can't use the "ready-to-merge" label.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:12):

So I suggest we ask for an approving review of a maintainer

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:12):

I suggest both.

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:13):

But the second condition has to only remove approving review and not labels.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:13):

And maybe there is a Github team of mathlib maintainers, and you can match on them in the mergify config with @something

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:14):

mergify only cares about reviews from people with write permission on the repository.

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:15):

Which I guess is a lot of people if it's talking about leanprover-community and not just leanprover-community/master

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:16):

Do you mean leanprover-community/mathlib or leanprover-community/mathlib/master?

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:20):

Yes.

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:20):

I don't know which of those two mergify means

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:21):

But it says repository, so I guess leanprover-community/mathlib

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:24):

You can do a regex match on the people who left a review

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:24):

It does mean that if the list of maintainers changes, you also need to update this config file.

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:26):

The attribute is approved-review-by and it takes an array of strings (the authors) as an argument. So we can use that.

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:31):

What is the suggested workflow to get mergify to merge once the build succeeds?

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:32):

@Simon Hudon I don't understand your question

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:33):

One maintainer gives an approving review, and someone gives a ready-to-merge label.

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:33):

But you were saying that the label ready-to-merge couldn't be used as intended

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:34):

Mergify won't remove it. (Or it will always remove it.)

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:34):

But @Chris Hughes thinks it is still a useful flag. And maybe I agree.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:35):

I think the maintainers need to agree on what they mean with an "Approving review"

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:35):

What does "always remove it" mean?

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:35):

We can't use the second condition to remove the label.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:35):

If you try to build a rule that removes the tag after new commits, the rule will remove the label as soon as it is added.

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:35):

Because it will be removed as soon as it's added, regardless of whether there are any commits.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:36):

Scenario: Maintainer gives approving review, thinking "looks good, but not exactly ready-to-merge". Doofus comes by and gives tag ready-to-merge. → Mergify goes ahead and merges.

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:38):

But only the maintainers can give a label so we should be ok as long as we don't choose doofuses as maintainers

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:38):

I don't think that scenario is any different from a doofus merging random PRs. Only click ready-to-merge, if it's ready to merge.

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:41):

I second that comment

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:47):

So we shouldn't remove the label automatically. Is this right?

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:47):

Yes.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:48):

Hmmm, I thought I saw people assigning WIP to their PRs.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:48):

Maybe that's a special label?

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:49):

Can you assign a label?

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:51):

#854

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:53):

Didn't realise that. I remember not being able to do it when we were at leanprover, but I guess you have write access to community.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:53):

@Simon Hudon @Chris Hughes So how about "Only click Approved review if it's ready to merge"?

view this post on Zulip Simon Hudon (Apr 02 2019 at 14:56):

If we have the label mechanism, do we also need the approved review mechanism. Maybe they should be two separate options: either you tag it as ready to merge or you approve a review

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:56):

The label mechanism is fragile

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:57):

Because an "old" label is not dismissed when someone pushes new commits

view this post on Zulip Chris Hughes (Apr 02 2019 at 14:57):

You don't need to be a maintainer to give a label.

view this post on Zulip Johan Commelin (Apr 02 2019 at 14:57):

Also :point_up:

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:04):

Are you sure? Johan, have you tried adding a label?

view this post on Zulip Chris Hughes (Apr 02 2019 at 15:07):

#854

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:11):

blast

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:11):

Ok a review too then

view this post on Zulip Chris Hughes (Apr 02 2019 at 15:12):

But the new rule has to be "Only give an approving review if it's ready to merge"

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:12):

Hmm... how about we make the rule "If it is approved by the person that got assigned, then merge"

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:13):

It might mean making 8 duplicate rules in the config file

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:13):

One for each maintainer

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:13):

But that is not very hard to maintain. And it is closer to current mathlib policy.

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:18):

I just assigned @Kevin Buzzard to #854

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:18):

I don't think that affects the issue at hand. But apparently this is possible

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:19):

blast! We have much less security than I thought on repo

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:20):

/me is a doofus :warning:

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:20):

I think you have a good idea. Let's go with that

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:20):

Haha! No duh! :P

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:20):

Also, it means that we shouldn't try to hack a has_review_by = assigned because that is unsecure.

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:21):

Explicitly test against a list of maintainers.

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:21):

I'm on a flaky connection, so I can't currently edit the file.

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:24):

Is the second rule of any use?

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:24):

It would be nice if the presence of a mergify.yml created a "Pass this to mergify" button next to the regular merge button...

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:24):

But I'm not going to PR to mergify (-;

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:24):

The current second rule doesn't have too much use anymore.

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:25):

I don't know what happens if someone pushes new commits in the 60 minutes between Mario's approval and Mergifies merging.

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:25):

maybe it's good to keep the rule in place

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:26):

It's going to reject the merge and we're going to need to update it again

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:26):

independent of the 2nd rule?

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:27):

With 50 open PRs at the same time, a few people might end up upgrading at the same time which will create a race condition and require one of them to start over. It might be better if we don't require a strict workflow

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:27):

Yes

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:28):

I think mergify maintains a queue

view this post on Zulip Chris Hughes (Apr 02 2019 at 15:28):

We still need the second rule.

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:29):

@Johan Commelin I don't think mergify can resolve that race condition with strict merge

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:29):

@Chris Hughes why?

view this post on Zulip Johan Commelin (Apr 02 2019 at 15:29):

I'm hopping on a bike. See you :bicycle:

view this post on Zulip Chris Hughes (Apr 02 2019 at 15:29):

In case there's a commit after an approving review.

view this post on Zulip Chris Hughes (Apr 02 2019 at 15:30):

The strict:smart means that there won't be a race, there'll just be a queue instead.

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:30):

How does that work?

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:31):

I just looked it up

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:31):

That sounds good. Let's do that

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:37):

@Chris Hughes Can you try this rule and see if it takes 7 reviews?

  - name: automatic merge on CI success and review
    conditions:
      - status-success=continuous-integration/travis-ci/pr
      - "#changes-requested-reviews-by=0"
      - base=master
      - label=ready-to-merge
      - approved-reviews-by=['avigad','rwbarton','digama0','cipher1024','ChrisHughes24','robertylewis','patrickmassot']
    actions:
      delete_head_branch: {}
      merge:
        method: squash
        strict: smart
        strict_method: merge

view this post on Zulip Simon Hudon (Apr 02 2019 at 15:38):

Also, you're saying that we need the second rule to remove stale reviews but why does it not work to remove ready-to-merge?

view this post on Zulip Chris Hughes (Apr 02 2019 at 15:52):

That's an invalid configuration. Not sure why

view this post on Zulip Simon Hudon (Apr 02 2019 at 16:20):

what if you only write - approved-reviews-by='avigad'? or `- approved-reviews-by=avigad?

view this post on Zulip Johan Commelin (Apr 02 2019 at 16:24):

@Simon Hudon For some (buggy) reason Mergify will dismiss-old-reviews only when there is an actual new commit, but it will label: remove [foobar] whenever something happens (for example, when "adding foobar" happens).

view this post on Zulip Simon Hudon (Apr 02 2019 at 16:33):

Ok, I filed an issue: https://github.com/Mergifyio/mergify-engine/issues/360

view this post on Zulip Simon Hudon (Apr 02 2019 at 16:34):

maybe we should add - label!=ready-to-merge in the conditions

view this post on Zulip Simon Hudon (Apr 02 2019 at 16:34):

no, that's dumb

view this post on Zulip Johan Commelin (Apr 02 2019 at 16:36):

I upvoted your issue

view this post on Zulip Simon Hudon (Apr 02 2019 at 18:08):

In the mean time, are we ready to merge the mergify setup?

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:08):

Is Mergify ready to merge the setup?

view this post on Zulip Simon Hudon (Apr 02 2019 at 18:09):

Huh?

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:09):

/joke

view this post on Zulip Chris Hughes (Apr 02 2019 at 18:09):

Not as is. It's not doofus proof currently.

view this post on Zulip Simon Hudon (Apr 02 2019 at 18:09):

You got me

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:09):

/me is a doofus :warning:

view this post on Zulip Chris Hughes (Apr 02 2019 at 18:10):

And the configuration Simon posted is invalid.

view this post on Zulip Simon Hudon (Apr 02 2019 at 18:10):

What is missing to make it doofus proof?

view this post on Zulip Simon Hudon (Apr 02 2019 at 18:10):

Oh, that

view this post on Zulip Simon Hudon (Apr 02 2019 at 18:10):

ok

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:10):

I'll happily break mathlib if you give me the chance

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:10):

I think we want 1 rule for every maintainer

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:11):

We don't want the maintainer of foobarology to approve of a PR in xyzzygies and suddenly the PR is merged by Mergify.

view this post on Zulip Chris Hughes (Apr 02 2019 at 18:14):

This is invalid for some reason

pull_request_rules:
- name: automatic merge on CI success and review
    conditions:
      - status-success=continuous-integration/travis-ci/pr
      - "#changes-requested-reviews-by=0"
      - base=master
      - label=ready-to-merge
      #- approved-reviews-by=avigad
    actions:
      delete_head_branch: {}
      merge:
        method: squash
        strict: smart
        strict_method: merge

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:15):

What is the error message?

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:15):

The current version in the PR is approved of by Mergify

view this post on Zulip Chris Hughes (Apr 02 2019 at 18:17):

Mergify configuration is invalid: position (3:15)

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:53):

I have no clue what is wrong. But the syntax highligher also isn't highlighting the 3rd line

view this post on Zulip Reid Barton (Apr 02 2019 at 18:54):

maybe an indentation issue? is this yaml syntax?

view this post on Zulip Chris Hughes (Apr 02 2019 at 18:56):

This works and its indistinguishable

pull_request_rules:
  - name: automatic merge when CI passes
    conditions:
      - status-success=continuous-integration/travis-ci/pr
      - "#changes-requested-reviews-by=0"
      - base=master
      - label=ready-to-merge
      - approved-reviews-by=['avigad','rwbarton','digama0','cipher1024','ChrisHughes24','robertylewis','patrickmassot']
    actions:
      merge:
        method: squash
        strict: smart
        strict_method: merge

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:58):

The difference is on the 2nd line

view this post on Zulip Johan Commelin (Apr 02 2019 at 18:58):

You indented the - name

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:02):

Good!

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:03):

Now, do we need 7 identical rules or is it ok to enumerate the maintainers?

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:03):

I think we need 7 rules

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:04):

But that's really up to the maintainers...

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:04):

Do you regard the maintainer of foobargles a doofus when it comes to xyzzygies?

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:05):

@Simon Hudon Approve of this to test.

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:05):

https://github.com/ChrisHughes24/mathlib/pull/47

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:08):

Do I make a review and approve?

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:08):

I think you need to invite me to review

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:08):

Are foobargles and xyzzygies two of your projects Johan?

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:08):

I think you can just click the "Changed files" tab

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:08):

And then "Review changes" -> "Approve"

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:10):

Foobargles and xyzzygies are both fundamental objects in scitamehtam

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:11):

https://github.com/Mergifyio/mergify-engine/issues/360#issuecomment-479148498

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:11):

obviously!

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:11):

I just wanted to know if you knew it

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:12):

obviously :grinning_face_with_smiling_eyes:

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:13):

Looks like your review didn't trigger it @Simon Hudon

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:14):

Would <= instead of = work?

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:14):

I don't think so...

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:14):

You could write a regex though

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:15):

Something like ~= nameA|nameB|nameC

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:15):

Modulo quotes etc

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:16):

In fact, I think you don't need any quotes

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:17):

uh!

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:17):

Nice

view this post on Zulip Reid Barton (Apr 02 2019 at 19:18):

I haven't really been following what's going on here, but I think there's no need (at least currently) to formally enforce a policy of which maintainers can approve what kind of PRs

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:19):

I agree @Reid Barton and I think the idea hasn't been considered seriously

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:19):

There is no such policy.

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:20):

I am thinking that Mergify PRs that have been approved by the maintainer assigned to the PR.

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:20):

Everyone can assign everyone to every PR

view this post on Zulip Reid Barton (Apr 02 2019 at 19:20):

We don't want the maintainer of foobarology to approve of a PR in xyzzygies and suddenly the PR is merged by Mergify.

Then I don't understand what this is about...?

view this post on Zulip Reid Barton (Apr 02 2019 at 19:21):

Using regexes to match usernames sounds like a bad idea to me

view this post on Zulip Reid Barton (Apr 02 2019 at 19:21):

you don't want to accidentally allow notrwbarton to merge PRs for example, it just seems like there is too much scope for error

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:23):

What I mean is that we can choose how careful maintainers should be with giving "approving" reviews.

view this post on Zulip Reid Barton (Apr 02 2019 at 19:23):

Oh, I see

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:24):

If we want to allow them to use it as a signal to another maintainer that they think a PR is fine, even if they don't want to trigger a merge, then we could follow my proposal

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:25):

Otoh, if the approve of a PR that was assigned to them, then I guess they also think that it is ready for merging. So Mergify can go ahead.

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:25):

And of course we can decorate the regex with ^(theregex)$

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:29):

This is showing up as Simon not having reviewed https://github.com/ChrisHughes24/mathlib/pull/47/checks?check_run_id=91331543

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:29):

With approved-reviews-by=cipher1024

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:33):

Weird...

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:35):

No, I did approve that PR

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:35):

Exactly... I can see that on the "Conversation" tab. But Mergify isn't picking this up.

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:36):

Maybe because it's a stale review

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:37):

But you don't have "Rule 2"

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:37):

@Simon Hudon Could you approve again?

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:47):

I just did

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:47):

Still doesn't fly

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:47):

And it didn't change the status

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:48):

This will match only reviewers with admin or write permission on the repository.

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:48):

I think that explains the issue

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:49):

Ah!

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:49):

Give me permission then

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:49):

Sorry, I can't do that (-;

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:49):

I'm not enough of a doofus

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:49):

Sent an invite

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:52):

It would be nice if it said "write permission on the base branch".

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:52):

Would save us a bunch of headaches

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:53):

Tada! :tada:

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:53):

It got merged! Well done @Simon Hudon @Chris Hughes

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:53):

:tada: :tada:

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:54):

Yay!

view this post on Zulip Simon Hudon (Apr 02 2019 at 19:54):

I think this addresses the doofus objection

view this post on Zulip Patrick Massot (Apr 02 2019 at 19:55):

I did follow closely. Did you find a website that will review all of Kenny's algebra PR and merge them?

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:55):

Only the extra-maintainer doofus objection

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:56):

But the intra-maintainer doofus objection still stands... You'll have to figure that out amongst yourselves though

view this post on Zulip Chris Hughes (Apr 02 2019 at 19:56):

Can you approve this one @Simon Hudon
https://github.com/ChrisHughes24/mathlib/pull/48
Just to see if the list of maintainers works

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:58):

Do we still want the label?

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:59):

By the way, there is a strict upper bound on the number of tests that @Chris Hughes can perform: at some point the README file in his fork will be empty.

view this post on Zulip Chris Hughes (Apr 02 2019 at 20:01):

Probably we don't want the label. But we'll have to be careful merging mergify, because there are a bunch of open PRs with approving reviews.

view this post on Zulip Simon Hudon (Apr 02 2019 at 20:02):

I think we can keep the label for two reasons: communicate with each other and avoid mistreating existing PRs

view this post on Zulip Johan Commelin (Apr 02 2019 at 20:09):

So the list version isn't working, it seems

view this post on Zulip Johan Commelin (Apr 02 2019 at 20:09):

I guess it means that you require all those people to approve

view this post on Zulip Chris Hughes (Apr 02 2019 at 20:10):

Maybe 7 conditions then.

view this post on Zulip Johan Commelin (Apr 03 2019 at 11:00):

I went ahead and edited the config into the 7 + 1 rules

view this post on Zulip Simon Hudon (Apr 03 2019 at 11:59):

I'm happy with that. What about you guys?

view this post on Zulip Simon Hudon (Apr 03 2019 at 12:08):

I think I can just merge this. We don't need to wait for the build

view this post on Zulip Johan Commelin (Apr 03 2019 at 12:21):

Let's go for it!

view this post on Zulip Johan Commelin (Apr 03 2019 at 12:22):

(Sorry I was distracted: trying to prove a theorem)

view this post on Zulip Simon Hudon (Apr 03 2019 at 12:38):

silly theorem getting in the way of real work

view this post on Zulip Simon Hudon (Apr 03 2019 at 12:38):

done

view this post on Zulip Simon Hudon (Apr 03 2019 at 12:38):

Let's try it for a couple of rounds and then advertise it. How about that?

view this post on Zulip Johan Commelin (Apr 03 2019 at 12:39):

Cool!

view this post on Zulip Simon Hudon (Apr 03 2019 at 13:50):

Does mergify only use the .mergify.yml file on master or does it use the one in the current branch?

view this post on Zulip Chris Hughes (Apr 03 2019 at 13:52):

Current branch

view this post on Zulip Simon Hudon (Apr 03 2019 at 13:52):

That might be a security issue ...

view this post on Zulip Chris Hughes (Apr 03 2019 at 13:54):

Yes, just realised.

view this post on Zulip Chris Hughes (Apr 03 2019 at 13:57):

How about exploiting it to commit a fix to the mergify repository?

view this post on Zulip Simon Hudon (Apr 03 2019 at 13:59):

Hahaha! To they use their own tool?

view this post on Zulip Chris Hughes (Apr 03 2019 at 14:00):

Yes.

view this post on Zulip Chris Hughes (Apr 03 2019 at 14:01):

Although mergify is disabled for PRs that change the configuration

view this post on Zulip Chris Hughes (Apr 03 2019 at 14:01):

So there is no problem

view this post on Zulip Simon Hudon (Apr 03 2019 at 14:02):

How do you do that?

view this post on Zulip Chris Hughes (Apr 03 2019 at 14:04):

It's disabled by default

view this post on Zulip Chris Hughes (Apr 03 2019 at 14:04):

We're fine

view this post on Zulip Simon Hudon (Apr 03 2019 at 14:05):

ooof :)

view this post on Zulip Simon Hudon (Apr 03 2019 at 14:05):

I almost wrote a panicked issue to them :P

view this post on Zulip Simon Hudon (Apr 03 2019 at 14:07):

Now I'm trying to change how travis deals with PRs. Right now, every time you push to a PR, you get two builds. I'd like them to cancel the push build. We'd get way more builds in.

view this post on Zulip Chris Hughes (Apr 03 2019 at 14:33):

Travis does seem to be less generous with allocating build time lately. A lot more queued builds.

view this post on Zulip Simon Hudon (Apr 03 2019 at 14:40):

I think it's because of duplicated work

view this post on Zulip Simon Hudon (Apr 03 2019 at 14:53):

I feel like disabling PR builds and only keeping push builds

view this post on Zulip Simon Hudon (Apr 03 2019 at 14:53):

But then, people creating PRs from other repos wouldn't get a build automatically

view this post on Zulip Rob Lewis (Apr 03 2019 at 15:14):

Regarding Travis slowdowns, I guess it's probably possible to pay for more time/power, right? Does anyone know how much this costs? I can't find it immediately on their website.

view this post on Zulip Johan Commelin (Apr 03 2019 at 15:15):

Or maybe one of the full profs can ask/instruct/request a local sysadmin to setup and maintain a CI server?

view this post on Zulip Simon Hudon (Apr 03 2019 at 15:17):

Those are possibilities. But right now, we're misusing the resources that we do have so first, let's see if we can use them better

view this post on Zulip Simon Hudon (Apr 03 2019 at 15:17):

And Robb: https://travis-ci.com/plans

view this post on Zulip Rob Lewis (Apr 03 2019 at 15:18):

Huh. travis-ci.com is different from travis-ci.org.

view this post on Zulip Rob Lewis (Apr 03 2019 at 15:25):

Should it become necessary, we could probably put a bit of Jasmin's Lean Forward money to an upgraded account. I don't know what the limitations are on the free account, so it's not clear which upgrade would be appropriate, or how much Jasmin would be willing to spend.

view this post on Zulip Simon Hudon (Apr 03 2019 at 15:27):

I think premium might be better than what we currently get

view this post on Zulip Simon Hudon (Apr 03 2019 at 15:27):

Open source projects get a pretty sweet deal

view this post on Zulip Rob Lewis (Apr 03 2019 at 15:28):

Okay, yeah, I doubt that would happen.

view this post on Zulip Chris Hughes (Apr 03 2019 at 19:21):

@Simon Hudon Your change fixed the old error on minchaowu's PR, but there's a new one, which is the same as the error on all the other PRs.

view this post on Zulip Scott Morrison (Apr 03 2019 at 22:01):

mergify doesn't seem to be working:

view this post on Zulip Scott Morrison (Apr 03 2019 at 22:01):

https://github.com/leanprover-community/mathlib/pull/865/checks?check_run_id=92382766

view this post on Zulip Simon Hudon (Apr 04 2019 at 13:10):

I'm going try and remove the protection on master for a moment. Let's see if that makes a difference

view this post on Zulip Simon Hudon (Apr 04 2019 at 15:26):

One thing we could do is go back to a way of working with two repo. That would fix the permission situation and that would lighten the load on mathlib Travis build budget

view this post on Zulip Rob Lewis (Apr 04 2019 at 15:41):

@Simon Hudon what happened when you removed the branch protection? If you do that, you could try a fresh start of mergify, by approving and tagging e.g. https://github.com/leanprover-community/mathlib/pull/831

view this post on Zulip Simon Hudon (Apr 04 2019 at 17:17):

We just got one successful build. It corresponds to me disabling the protection

view this post on Zulip Chris Hughes (Apr 04 2019 at 19:12):

Should we reenable the protection by enabling "Require review from Code Owners", and making administrators code owners for every file?

view this post on Zulip Simon Hudon (Apr 04 2019 at 19:14):

How do we set the code owners?

view this post on Zulip Chris Hughes (Apr 04 2019 at 19:15):

https://help.github.com/en/articles/about-code-owners

view this post on Zulip Simon Hudon (Apr 04 2019 at 19:19):

That sounds like a great solution!

view this post on Zulip Simon Hudon (Apr 04 2019 at 19:19):

Let's do it!

view this post on Zulip Simon Hudon (Apr 04 2019 at 19:20):

We can set @mathlib-maintainers as the owner

view this post on Zulip Chris Hughes (Apr 04 2019 at 21:23):

Do you know where the update branch button has gone by the way?

view this post on Zulip Simon Hudon (Apr 04 2019 at 21:24):

I do not

view this post on Zulip Simon Hudon (Apr 05 2019 at 00:03):

@Scott Morrison I'm not sure your interruption control code works. Can you look at it?

view this post on Zulip Simon Hudon (Apr 05 2019 at 00:04):

https://github.com/leanprover-community/mathlib/blob/e791b57f819a1ec6948f186b8148c895a805cbf5/scripts/update-mathlib.py#L91-L93

I'm told signal is not in scope.

view this post on Zulip Chris Hughes (Apr 06 2019 at 20:05):

Why is #862 failing? Is it because the pr build finished before the push build perhaps? It says push build has failed when it has passed.

view this post on Zulip Simon Hudon (Apr 06 2019 at 20:15):

I'll look into it. It might be because of a new rule I'm trying out

view this post on Zulip Chris Hughes (Apr 07 2019 at 00:25):

I think the best thing would be to make sure that the branch protections <= mergify conditions

view this post on Zulip Chris Hughes (Apr 07 2019 at 00:26):

It didn't say it had failed actually, it says pending.

view this post on Zulip Simon Hudon (Apr 07 2019 at 01:56):

the next two PRs should merge automatically now


Last updated: May 06 2021 at 11:23 UTC