Zulip Chat Archive

Stream: PR reviews

Topic: mergify

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

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']

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

Simon Hudon (Apr 01 2019 at 18:16):

What does strict mean?

Chris Hughes (Apr 01 2019 at 18:19):

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

Simon Hudon (Apr 01 2019 at 18:21):

That's probably best if we automate merges

Chris Hughes (Apr 01 2019 at 18:22):

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

Simon Hudon (Apr 01 2019 at 18:25):

Both the PR build and the push build?

Chris Hughes (Apr 01 2019 at 18:27):

Exactly those rules.

Simon Hudon (Apr 01 2019 at 18:27):

I mean, did neither build terminate before the merge?

Chris Hughes (Apr 01 2019 at 18:28):

Neither build terminated

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.

Simon Hudon (Apr 01 2019 at 18:30):

Is the list of condition a disjunction or a conjunction?

Simon Hudon (Apr 01 2019 at 18:30):

Try removing the last condition

Chris Hughes (Apr 01 2019 at 18:34):

Now it doesn't tell me anything.

Simon Hudon (Apr 01 2019 at 18:36):

That's frustrating

Simon Hudon (Apr 01 2019 at 18:36):

Can I let you look into it?

Chris Hughes (Apr 01 2019 at 18:36):

But travis has also stopped.

Chris Hughes (Apr 01 2019 at 18:37):

I'll have a go at sorting it out.

Simon Hudon (Apr 01 2019 at 18:38):

Thanks! Let me know if you need something

Johan Commelin (Apr 01 2019 at 18:40):

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

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

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?

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.

Simon Hudon (Apr 01 2019 at 19:00):

I would put that in condition

Chris Hughes (Apr 01 2019 at 19:00):

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

Chris Hughes (Apr 01 2019 at 19:00):

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

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

Johan Commelin (Apr 01 2019 at 19:30):

Cool! Let's see what happens.

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

Chris Hughes (Apr 01 2019 at 20:03):

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

Johan Commelin (Apr 01 2019 at 20:04):

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

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

Chris Hughes (Apr 01 2019 at 20:06):

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

Johan Commelin (Apr 01 2019 at 20:14):

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

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.

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.

Simon Hudon (Apr 01 2019 at 20:16):

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

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...

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?

Rob Lewis (Apr 01 2019 at 20:18):

I'd like that tool too.

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.

Simon Hudon (Apr 01 2019 at 20:21):

That's what this thread (mergify) is about

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

Kevin Buzzard (Apr 01 2019 at 21:30):

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

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.

Simon Hudon (Apr 01 2019 at 22:48):

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

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?

Chris Hughes (Apr 02 2019 at 08:15):

Yes. It all seems to be working as expected.

Johan Commelin (Apr 02 2019 at 08:16):

That's great news.

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?

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.

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

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.

Johan Commelin (Apr 02 2019 at 11:55):

Aah, got it

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.

Simon Hudon (Apr 02 2019 at 13:05):

nice! Thanks!

Simon Hudon (Apr 02 2019 at 13:06):

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

Chris Hughes (Apr 02 2019 at 13:07):

How does the second condition work?

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.

Simon Hudon (Apr 02 2019 at 13:12):

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

      - base=master

Chris Hughes (Apr 02 2019 at 13:12):

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

Johan Commelin (Apr 02 2019 at 13:14):

I also don't understand the 2nd rule

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

Johan Commelin (Apr 02 2019 at 13:19):

Why is strict_method back to squash?

Johan Commelin (Apr 02 2019 at 13:19):

That's not a valid value

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.

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.

Chris Hughes (Apr 02 2019 at 13:21):

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

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.

Chris Hughes (Apr 02 2019 at 13:21):

I see.

Chris Hughes (Apr 02 2019 at 13:21):

Then merge is correct.

Chris Hughes (Apr 02 2019 at 13:22):

I misunderstood.

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.

Chris Hughes (Apr 02 2019 at 13:24):

Okay, let's do that.

Chris Hughes (Apr 02 2019 at 13:24):

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

Johan Commelin (Apr 02 2019 at 13:24):

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

Johan Commelin (Apr 02 2019 at 13:26):

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

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.

Chris Hughes (Apr 02 2019 at 13:29):

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

Johan Commelin (Apr 02 2019 at 13:30):

The badge in the README is now fixed

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

Johan Commelin (Apr 02 2019 at 13:51):

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

Chris Hughes (Apr 02 2019 at 13:53):

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

Chris Hughes (Apr 02 2019 at 13:53):

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

Chris Hughes (Apr 02 2019 at 13:53):

I think maybe it only cares about reviews by admin.

Johan Commelin (Apr 02 2019 at 13:56):

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

Chris Hughes (Apr 02 2019 at 13:58):

It didn't remove it.

Chris Hughes (Apr 02 2019 at 13:58):

Now what happens if it's edited

Simon Hudon (Apr 02 2019 at 14:07):

If what is edited?

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.

Chris Hughes (Apr 02 2019 at 14:08):

If there's a commit I meant.

Johan Commelin (Apr 02 2019 at 14:09):

Ok, I'll make another commit.

Johan Commelin (Apr 02 2019 at 14:10):

Done

Johan Commelin (Apr 02 2019 at 14:11):

Ok, it removed your review

Chris Hughes (Apr 02 2019 at 14:11):

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

Chris Hughes (Apr 02 2019 at 14:12):

We need an approving review, and a tag?

Johan Commelin (Apr 02 2019 at 14:12):

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

Johan Commelin (Apr 02 2019 at 14:12):

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

Chris Hughes (Apr 02 2019 at 14:12):

I suggest both.

Chris Hughes (Apr 02 2019 at 14:13):

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

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

Chris Hughes (Apr 02 2019 at 14:14):

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

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

Simon Hudon (Apr 02 2019 at 14:16):

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

Chris Hughes (Apr 02 2019 at 14:20):

Yes.

Chris Hughes (Apr 02 2019 at 14:20):

I don't know which of those two mergify means

Chris Hughes (Apr 02 2019 at 14:21):

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

Johan Commelin (Apr 02 2019 at 14:24):

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

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.

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.

Simon Hudon (Apr 02 2019 at 14:31):

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

Johan Commelin (Apr 02 2019 at 14:32):

@Simon Hudon I don't understand your question

Chris Hughes (Apr 02 2019 at 14:33):

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

Simon Hudon (Apr 02 2019 at 14:33):

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

Johan Commelin (Apr 02 2019 at 14:34):

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

Johan Commelin (Apr 02 2019 at 14:34):

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

Johan Commelin (Apr 02 2019 at 14:35):

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

Simon Hudon (Apr 02 2019 at 14:35):

What does "always remove it" mean?

Chris Hughes (Apr 02 2019 at 14:35):

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

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.

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.

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.

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

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.

Simon Hudon (Apr 02 2019 at 14:41):

I second that comment

Simon Hudon (Apr 02 2019 at 14:47):

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

Chris Hughes (Apr 02 2019 at 14:47):

Yes.

Johan Commelin (Apr 02 2019 at 14:48):

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

Johan Commelin (Apr 02 2019 at 14:48):

Maybe that's a special label?

Chris Hughes (Apr 02 2019 at 14:49):

Can you assign a label?

Johan Commelin (Apr 02 2019 at 14:51):

#854

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.

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"?

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

Johan Commelin (Apr 02 2019 at 14:56):

The label mechanism is fragile

Johan Commelin (Apr 02 2019 at 14:57):

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

Chris Hughes (Apr 02 2019 at 14:57):

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

Johan Commelin (Apr 02 2019 at 14:57):

Also :point_up:

Simon Hudon (Apr 02 2019 at 15:04):

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

Chris Hughes (Apr 02 2019 at 15:07):

#854

Simon Hudon (Apr 02 2019 at 15:11):

blast

Simon Hudon (Apr 02 2019 at 15:11):

Ok a review too then

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"

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"

Johan Commelin (Apr 02 2019 at 15:13):

It might mean making 8 duplicate rules in the config file

Johan Commelin (Apr 02 2019 at 15:13):

One for each maintainer

Johan Commelin (Apr 02 2019 at 15:13):

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

Johan Commelin (Apr 02 2019 at 15:18):

I just assigned @Kevin Buzzard to #854

Johan Commelin (Apr 02 2019 at 15:18):

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

Simon Hudon (Apr 02 2019 at 15:19):

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

Johan Commelin (Apr 02 2019 at 15:20):

/me is a doofus :warning:

Simon Hudon (Apr 02 2019 at 15:20):

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

Simon Hudon (Apr 02 2019 at 15:20):

Haha! No duh! :P

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.

Johan Commelin (Apr 02 2019 at 15:21):

Explicitly test against a list of maintainers.

Johan Commelin (Apr 02 2019 at 15:21):

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

Simon Hudon (Apr 02 2019 at 15:24):

Is the second rule of any use?

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...

Johan Commelin (Apr 02 2019 at 15:24):

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

Johan Commelin (Apr 02 2019 at 15:24):

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

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.

Johan Commelin (Apr 02 2019 at 15:25):

maybe it's good to keep the rule in place

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

Johan Commelin (Apr 02 2019 at 15:26):

independent of the 2nd rule?

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

Simon Hudon (Apr 02 2019 at 15:27):

Yes

Johan Commelin (Apr 02 2019 at 15:28):

I think mergify maintains a queue

Chris Hughes (Apr 02 2019 at 15:28):

We still need the second rule.

Simon Hudon (Apr 02 2019 at 15:29):

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

Simon Hudon (Apr 02 2019 at 15:29):

@Chris Hughes why?

Johan Commelin (Apr 02 2019 at 15:29):

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

Chris Hughes (Apr 02 2019 at 15:29):

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

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.

Simon Hudon (Apr 02 2019 at 15:30):

How does that work?

Simon Hudon (Apr 02 2019 at 15:31):

I just looked it up

Simon Hudon (Apr 02 2019 at 15:31):

That sounds good. Let's do that

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

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?

Chris Hughes (Apr 02 2019 at 15:52):

That's an invalid configuration. Not sure why

Simon Hudon (Apr 02 2019 at 16:20):

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

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).

Simon Hudon (Apr 02 2019 at 16:33):

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

Simon Hudon (Apr 02 2019 at 16:34):

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

Simon Hudon (Apr 02 2019 at 16:34):

no, that's dumb

Johan Commelin (Apr 02 2019 at 16:36):

I upvoted your issue

Simon Hudon (Apr 02 2019 at 18:08):

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

Johan Commelin (Apr 02 2019 at 18:08):

Is Mergify ready to merge the setup?

Simon Hudon (Apr 02 2019 at 18:09):

Huh?

Johan Commelin (Apr 02 2019 at 18:09):

/joke

Chris Hughes (Apr 02 2019 at 18:09):

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

Simon Hudon (Apr 02 2019 at 18:09):

You got me

Johan Commelin (Apr 02 2019 at 18:09):

/me is a doofus :warning:

Chris Hughes (Apr 02 2019 at 18:10):

And the configuration Simon posted is invalid.

Simon Hudon (Apr 02 2019 at 18:10):

What is missing to make it doofus proof?

Simon Hudon (Apr 02 2019 at 18:10):

Oh, that

Simon Hudon (Apr 02 2019 at 18:10):

Johan Commelin (Apr 02 2019 at 18:10):

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

Johan Commelin (Apr 02 2019 at 18:10):

I think we want 1 rule for every maintainer

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.

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

Johan Commelin (Apr 02 2019 at 18:15):

What is the error message?

Johan Commelin (Apr 02 2019 at 18:15):

The current version in the PR is approved of by Mergify

Chris Hughes (Apr 02 2019 at 18:17):

Mergify configuration is invalid: position (3:15)

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

Reid Barton (Apr 02 2019 at 18:54):

maybe an indentation issue? is this yaml syntax?

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

Johan Commelin (Apr 02 2019 at 18:58):

The difference is on the 2nd line

Johan Commelin (Apr 02 2019 at 18:58):

You indented the - name

Simon Hudon (Apr 02 2019 at 19:02):

Good!

Simon Hudon (Apr 02 2019 at 19:03):

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

Johan Commelin (Apr 02 2019 at 19:03):

I think we need 7 rules

Johan Commelin (Apr 02 2019 at 19:04):

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

Johan Commelin (Apr 02 2019 at 19:04):

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

Chris Hughes (Apr 02 2019 at 19:05):

@Simon Hudon Approve of this to test.

Chris Hughes (Apr 02 2019 at 19:05):

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

Simon Hudon (Apr 02 2019 at 19:08):

Do I make a review and approve?

Simon Hudon (Apr 02 2019 at 19:08):

I think you need to invite me to review

Simon Hudon (Apr 02 2019 at 19:08):

Are foobargles and xyzzygies two of your projects Johan?

Johan Commelin (Apr 02 2019 at 19:08):

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

Johan Commelin (Apr 02 2019 at 19:08):

And then "Review changes" -> "Approve"

Johan Commelin (Apr 02 2019 at 19:10):

Foobargles and xyzzygies are both fundamental objects in scitamehtam

Simon Hudon (Apr 02 2019 at 19:11):

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

Simon Hudon (Apr 02 2019 at 19:11):

obviously!

Simon Hudon (Apr 02 2019 at 19:11):

I just wanted to know if you knew it

Johan Commelin (Apr 02 2019 at 19:12):

obviously :grinning_face_with_smiling_eyes:

Chris Hughes (Apr 02 2019 at 19:13):

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

Chris Hughes (Apr 02 2019 at 19:14):

Would <= instead of = work?

Johan Commelin (Apr 02 2019 at 19:14):

I don't think so...

Johan Commelin (Apr 02 2019 at 19:14):

You could write a regex though

Johan Commelin (Apr 02 2019 at 19:15):

Something like ~= nameA|nameB|nameC

Johan Commelin (Apr 02 2019 at 19:15):

Modulo quotes etc

Johan Commelin (Apr 02 2019 at 19:16):

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

Simon Hudon (Apr 02 2019 at 19:17):

uh!

Simon Hudon (Apr 02 2019 at 19:17):

Nice

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

Simon Hudon (Apr 02 2019 at 19:19):

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

Johan Commelin (Apr 02 2019 at 19:19):

There is no such policy.

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.

Johan Commelin (Apr 02 2019 at 19:20):

Everyone can assign everyone to every PR

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...?

Reid Barton (Apr 02 2019 at 19:21):

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

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

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.

Reid Barton (Apr 02 2019 at 19:23):

Oh, I see

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

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.

Johan Commelin (Apr 02 2019 at 19:25):

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

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

Chris Hughes (Apr 02 2019 at 19:29):

With approved-reviews-by=cipher1024

Johan Commelin (Apr 02 2019 at 19:33):

Weird...

Simon Hudon (Apr 02 2019 at 19:35):

No, I did approve that PR

Johan Commelin (Apr 02 2019 at 19:35):

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

Chris Hughes (Apr 02 2019 at 19:36):

Maybe because it's a stale review

Johan Commelin (Apr 02 2019 at 19:37):

But you don't have "Rule 2"

Johan Commelin (Apr 02 2019 at 19:37):

@Simon Hudon Could you approve again?

Simon Hudon (Apr 02 2019 at 19:47):

I just did

Johan Commelin (Apr 02 2019 at 19:47):

Still doesn't fly

Chris Hughes (Apr 02 2019 at 19:47):

And it didn't change the status

Johan Commelin (Apr 02 2019 at 19:48):

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

Johan Commelin (Apr 02 2019 at 19:48):

I think that explains the issue

Simon Hudon (Apr 02 2019 at 19:49):

Ah!

Simon Hudon (Apr 02 2019 at 19:49):

Give me permission then

Johan Commelin (Apr 02 2019 at 19:49):

Sorry, I can't do that (-;

Johan Commelin (Apr 02 2019 at 19:49):

I'm not enough of a doofus

Chris Hughes (Apr 02 2019 at 19:49):

Sent an invite

Johan Commelin (Apr 02 2019 at 19:52):

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

Johan Commelin (Apr 02 2019 at 19:52):

Would save us a bunch of headaches

Johan Commelin (Apr 02 2019 at 19:53):

Tada! :tada:

Johan Commelin (Apr 02 2019 at 19:53):

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

Simon Hudon (Apr 02 2019 at 19:53):

:tada: :tada:

Simon Hudon (Apr 02 2019 at 19:54):

Yay!

Simon Hudon (Apr 02 2019 at 19:54):

I think this addresses the doofus objection

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?

Johan Commelin (Apr 02 2019 at 19:55):

Only the extra-maintainer doofus objection

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

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

Johan Commelin (Apr 02 2019 at 19:58):

Do we still want the label?

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.

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.

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

Johan Commelin (Apr 02 2019 at 20:09):

So the list version isn't working, it seems

Johan Commelin (Apr 02 2019 at 20:09):

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

Chris Hughes (Apr 02 2019 at 20:10):

Maybe 7 conditions then.

Johan Commelin (Apr 03 2019 at 11:00):

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

Simon Hudon (Apr 03 2019 at 11:59):

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

Simon Hudon (Apr 03 2019 at 12:08):

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

Johan Commelin (Apr 03 2019 at 12:21):

Let's go for it!

Johan Commelin (Apr 03 2019 at 12:22):

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

Simon Hudon (Apr 03 2019 at 12:38):

silly theorem getting in the way of real work

Simon Hudon (Apr 03 2019 at 12:38):

done

Simon Hudon (Apr 03 2019 at 12:38):

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

Johan Commelin (Apr 03 2019 at 12:39):

Cool!

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?

Chris Hughes (Apr 03 2019 at 13:52):

Current branch

Simon Hudon (Apr 03 2019 at 13:52):

That might be a security issue ...

Chris Hughes (Apr 03 2019 at 13:54):

Yes, just realised.

Chris Hughes (Apr 03 2019 at 13:57):

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

Simon Hudon (Apr 03 2019 at 13:59):

Hahaha! To they use their own tool?

Chris Hughes (Apr 03 2019 at 14:00):

Yes.

Chris Hughes (Apr 03 2019 at 14:01):

Although mergify is disabled for PRs that change the configuration

Chris Hughes (Apr 03 2019 at 14:01):

So there is no problem

Simon Hudon (Apr 03 2019 at 14:02):

How do you do that?

Chris Hughes (Apr 03 2019 at 14:04):

It's disabled by default

Chris Hughes (Apr 03 2019 at 14:04):

We're fine

Simon Hudon (Apr 03 2019 at 14:05):

ooof :)

Simon Hudon (Apr 03 2019 at 14:05):

I almost wrote a panicked issue to them :P

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.

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.

Simon Hudon (Apr 03 2019 at 14:40):

I think it's because of duplicated work

Simon Hudon (Apr 03 2019 at 14:53):

I feel like disabling PR builds and only keeping push builds

Simon Hudon (Apr 03 2019 at 14:53):

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

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.

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?

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

Simon Hudon (Apr 03 2019 at 15:17):

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

Rob Lewis (Apr 03 2019 at 15:18):

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

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.

Simon Hudon (Apr 03 2019 at 15:27):

I think premium might be better than what we currently get

Simon Hudon (Apr 03 2019 at 15:27):

Open source projects get a pretty sweet deal

Rob Lewis (Apr 03 2019 at 15:28):

Okay, yeah, I doubt that would happen.

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.

Scott Morrison (Apr 03 2019 at 22:01):

mergify doesn't seem to be working:

Scott Morrison (Apr 03 2019 at 22:01):

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

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

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

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