Zulip Chat Archive

Stream: general

Topic: mergify

Sebastien Gouezel (Jun 05 2019 at 07:47):

Is there a way to teach mergify that, if it merges a branch with master, then it should not dismiss approving reviews? #1085 is blocked because of this (and I can not approve it myself as I am the author :)

Bryan Gin-ge Chen (Mar 01 2020 at 20:15):

Does anyone know why mergify is stuck on this PR? https://github.com/leanprover-community/mathlib/pull/2056

Yury G. Kudryashov (Mar 01 2020 at 22:42):

I have no idea. What should I do: wait? merge manually?

Yury G. Kudryashov (Mar 02 2020 at 00:54):

Same for #2060

Yury G. Kudryashov (Mar 02 2020 at 00:55):

It seems that mergify doesn't like (some of) my PRs. Can we debug this problem?

Bryan Gin-ge Chen (Mar 02 2020 at 01:00):

The last PR that mergify worked on was #2062, so I suspect something in #2065 caused it to stop working.

Yury G. Kudryashov (Mar 02 2020 at 01:30):

Who has access to mergify logs? Note that #2065 was not merged automatically.

Yury G. Kudryashov (Mar 02 2020 at 01:43):

I don't understand what was the purpose of #2065, not speaking of possible unwanted side-effects.

Bryan Gin-ge Chen (Mar 02 2020 at 01:54):

I think #2065 was meant to address the comments here in #2048.

Yury G. Kudryashov (Mar 02 2020 at 02:10):

Let's call @Rob Lewis and @Gabriel Ebner

Yury G. Kudryashov (Mar 02 2020 at 06:50):

@Mario Carneiro Maybe you have access to some mergify logs?

Mario Carneiro (Mar 02 2020 at 06:52):

Nope, clicking around didn't lead me anywhere interesting

Mario Carneiro (Mar 02 2020 at 06:52):

there is a button labeled "view more details on mergify" but it leads to the same page

Mario Carneiro (Mar 02 2020 at 06:56):

Oh wait, I made it to the mergify dashboard. Here is the summary for #2056

#### Rule: automatic merge on CI success and review - pr (delete_head_branch, merge)
- [ ] `status-success=Build mathlib (leanprover-community/lean:3.5.1)`
- [X] `#changes-requested-reviews-by=0`
- [X] `base=master`
- [X] `label=ready-to-merge`
- [X] `approved-reviews-by=@leanprover-community/mathlib-maintainers`

#### Rule: automatic merge on CI success and review - push #1 (delete_head_branch, merge)
- [ ] `status-success=Build mathlib (leanprover-community/lean:3.5.1)`
- [X] `#changes-requested-reviews-by=0`
- [X] `base=master`
- [X] `label=ready-to-merge`
- [X] `approved-reviews-by=@leanprover-community/mathlib-maintainers`

Yury G. Kudryashov (Mar 02 2020 at 07:00):

Probably we should remove " (leanprover-community/lean:3.5.1)" from mergify.yml

Mario Carneiro (Mar 02 2020 at 07:03):

that certainly looks like the problem. Not clear what that string is supposed to bind to

Yury G. Kudryashov (Mar 02 2020 at 07:05):

#2077

Yury G. Kudryashov (Mar 02 2020 at 07:06):

See https://github.com/leanprover-community/mathlib/pull/2065/files#diff-898e737ee4e56ba042bda31764bed49eL9

Yury G. Kudryashov (Mar 02 2020 at 07:07):

Could you approve #2077 please?

Mario Carneiro (Mar 02 2020 at 07:08):

are you sure that's the right thing? It's still not clear how this config generates that string

Mario Carneiro (Mar 02 2020 at 07:09):

Oh I see, it is the build matrix thing at the top that got removed

Yury G. Kudryashov (Mar 02 2020 at 07:09):

I think that it added label from "matrix".

Mario Carneiro (Mar 02 2020 at 07:10):

I merged directly, maybe mergify has to be restarted for existing builds

Mario Carneiro (Mar 02 2020 at 07:12):

CI seems to be running so we'll see if things are fixed in an hour

Mario Carneiro (Mar 02 2020 at 07:17):

#2056 is merged so I think we're good

Yury G. Kudryashov (Mar 02 2020 at 07:19):

Is it?

Mario Carneiro (Mar 02 2020 at 07:20):

Oh I guess that was just the first stage; it put a merge commit on the branch

Yury G. Kudryashov (Mar 02 2020 at 07:22):

So, we'll know in about 1 hour as you said before.

Johan Commelin (Mar 02 2020 at 09:15):

Did mergify just merge something?

Yury G. Kudryashov (Mar 02 2020 at 09:16):

Yes.

Rob Lewis (Mar 04 2020 at 20:49):

Mergify is getting greedy, it's claiming commits as its own now. https://github.com/leanprover-community/mathlib/commit/9fc675c43151a53052b7f467c8182ea3bece7de6

Bryan Gin-ge Chen (Mar 04 2020 at 22:30):

It happened with the latest commit as well. Does anyone know what changed?

Floris van Doorn (Mar 05 2020 at 04:55):

so mergify will be an author of the mathlib 2.0 paper?

Marc Huisinga (Mar 05 2020 at 08:29):

the revolution is upon us

Gabriel Ebner (Mar 05 2020 at 10:29):

Apparently github changed something: https://github.com/Mergifyio/mergify-engine/issues/764

Gabriel Ebner (Mar 06 2020 at 13:52):

According to the reports on the mergify bug tracker, mergify is no longer greedy.

Kevin Buzzard (Mar 06 2020 at 18:36):

ha ha and I now see that the last commit was by leanprover-community-bot! They are taking over!

Chris Hughes (Mar 06 2020 at 18:37):

I think that one actually was a bot commit

Chris Hughes (Mar 06 2020 at 18:37):

Something about the prior commit meant it automatically made that commit I think.

Kevin Buzzard (Mar 06 2020 at 18:38):

When will leanprover-community-bot be able to bundle subgroups?

Rob Lewis (Mar 06 2020 at 20:32):

leanprover-community-bot is friendly and one of us. mergify[bot], though, that one has a bit of an attitude.

Last updated: Dec 20 2023 at 11:08 UTC