Stream: coqbot devs & users

Topic: coqbot failed to trigger some pipelines?


view this post on Zulip Erik Martin-Dorel (Jul 25 2020 at 21:47):

@Théo Zimmermann I believe some PRs were missed by Coqbot to trigger pipelines on GitLab CI;
Do you believe this is a known bug of coqbot's current deployment, or is it due to GitHub / GitLab ?

cf. e.g. this PR:

view this post on Zulip Théo Zimmermann (Jul 26 2020 at 12:50):

@Erik Martin-Dorel Can you check the history of webhook sent? Are some of them red? I've noticed some time outs recently.

view this post on Zulip Erik Martin-Dorel (Jul 26 2020 at 13:00):

@Théo Zimmermann , no, no item is in red… but it seems for all these requests X-GitHub-Event: push, the response says:

No action taken: Unhandled GitHub event.

Maybe I've overlooked, but see https://github.com/coq-community/docker-base/settings/hooks/231342757 for details

view this post on Zulip Théo Zimmermann (Jul 26 2020 at 13:02):

Did it ever work correctly for PRs from forks for this repo? It seems that pull requests events are not being sent, so this is why nothing is happening.

view this post on Zulip Théo Zimmermann (Jul 26 2020 at 13:02):

The /push event is not necessary on the other hand.

view this post on Zulip Erik Martin-Dorel (Jul 26 2020 at 13:14):

OK I understand, thanks @Théo Zimmermann! I guess it had worked at the time of the Coq workshop because the other event /issue had been enough to trigger the pr pipeline… and I had believed everything was fine. But not fully indeed, so, my bad, I should have read the coqbot documentation more closely :)
Sorry for the noise.

view this post on Zulip Théo Zimmermann (Jul 26 2020 at 13:16):

No worries, but the /issue event shouldn't have been enough to trigger the pipeline, so I'm still surprised. However, if these were PRs from branches in the repository, then GitLab's mirroring feature would have replaced it, and the webhooks from GitLab would have been sufficient to get the results back.

view this post on Zulip Erik Martin-Dorel (Jul 26 2020 at 13:22):

I confirm you're right: the builds I was thinking about were actually in docker-mathcomp (whose webhook was well-configured).
So no surprise expected: the /issue event didn't trigger something weird.

view this post on Zulip Erik Martin-Dorel (Jul 26 2020 at 13:28):

However, I now have a doubt: are you sure the event should be /issue, not /issues?
Because in the webhook events list, there is no singular form (issue), and if you look e.g. at

https://github.com/coq-community/docker-coq/settings/hooks/231342784

the event 2020-07-08 11:22:24 yields:

Request URL: https://coqbot.herokuapp.com:
Request method: POST
Accept: */*
content-type: application/json
[…]
X-GitHub-Event: issues

and the response:

No action taken: Unhandled GitHub action.

view this post on Zulip Théo Zimmermann (Jul 26 2020 at 14:08):

The webhooks should be sent to /github. Sorry for being confusing by using a slash to designate the events :confounded:

view this post on Zulip Théo Zimmermann (Jul 26 2020 at 14:08):

But the two repositories are correctly configured AFAICS


Last updated: Jan 31 2023 at 10:01 UTC