@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:
@Erik Martin-Dorel Can you check the history of webhook sent? Are some of them red? I've noticed some time outs recently.
@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
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.
/push event is not necessary on the other hand.
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.
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.
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.
However, I now have a doubt: are you sure the event should be
Because in the webhook events list, there is no singular form (issue), and if you look e.g. at
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:
But the two repositories are correctly configured AFAICS
Last updated: Jan 31 2023 at 10:01 UTC