Erik Martin-Dorel (Jul 25 2020 at 21:47): 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:
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.
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
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.
Théo Zimmermann (Jul 26 2020 at 13:02):The /push event is not necessary on the other hand.
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.
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.
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.
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.
The webhooks should be sent to /github. Sorry for being confusing by using a slash to designate the events :confounded:
Théo Zimmermann (Jul 26 2020 at 14:08):But the two repositories are correctly configured AFAICS
Last updated: May 28 2023 at 18:29 UTC