Stream: coqbot devs & users

Topic: opam archive CI not reporting status to GitHub


view this post on Zulip Karl Palmskog (Feb 28 2022 at 12:29):

looks like the GitLab CI for the opam archive is not getting reported back to GitHub: https://github.com/coq/opam-coq-archive/pull/2121

Compare jobs like this one on GitLab: https://gitlab.com/coq/opam-coq-archive/-/jobs/2143986516 ... which don't show up on GitHub, this is empty: https://github.com/coq/opam-coq-archive/pull/2121/checks

view this post on Zulip Guillaume Melquiond (Feb 28 2022 at 12:37):

I suppose it means that Coqbot died. @Théo Zimmermann

view this post on Zulip David Swasey (Feb 28 2022 at 13:37):

Perhaps related: opam update coq-released times out (so https://coq.inria.fr/opam/released seems to be down).

view this post on Zulip Karl Palmskog (Feb 28 2022 at 13:40):

opam update with coq-released defined as https://coq.inria.fr/opam/released works fine for me

view this post on Zulip Karl Palmskog (Feb 28 2022 at 13:41):

I also think this is Coqbot-related, and shouldn't affect anything else that Coqbot doesn't touch

view this post on Zulip David Swasey (Feb 28 2022 at 13:47):

Ack. traceroute suggests there are some problems between my location and coq.inria.fr. Sorry for the noise.

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 14:33):

It looks like the Coq repo is affected as well, confirming that this is coqbot-related.

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 14:36):

FTR, GitHub reports the following when coqbot attempts to create a new checkRun: {"errors":[{"path":["mutation newCheckRun","createCheckRun","input","headSha"],"extensions":{"code":"variableMismatch","variableName":"headSha","typeName":"String!","argumentName":"headSha","errorMessage":"Type mismatch"},"locations":[{"line":2,"column":77}],"message":"Type mismatch on variable $headSha and argument headSha (String! / GitObjectID!)"},{"path":["mutation newCheckRun","createCheckRun","input","detailsUrl"],"extensions":{"code":"variableMismatch","variableName":"url","typeName":"String!","argumentName":"detailsUrl","errorMessage":"Type mismatch"},"locations":[{"line":2,"column":121}],"message":"Type mismatch on variable $url and argument detailsUrl (String! / URI)"}]}

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 14:36):

Since nothing has changed in the last 15 days on the bot-side, this must be related to a change on the GitHub-side.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 14:38):

if it helps, the change likely happened about 6 days ago, just between the following PRs:

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 14:40):

What? GitHub statuses have not been reported for 6 days and I would hear about it only now? That doesn't sound credible, especially on the Coq repository.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 14:42):

well, I can only report what I saw, which is that PR 2120 in the archive didn't get job statuses. I thought it was some temporary fluke...

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 14:42):

OK, I will try to check if this is the same issue.

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 14:46):

I will track this here: https://github.com/coq/bot/issues/203

view this post on Zulip Pierre-Marie Pédrot (Feb 28 2022 at 14:49):

The same problem is currently happening with the Coq CI proper, but this is recent (today-ish?)

view this post on Zulip Pierre-Marie Pédrot (Feb 28 2022 at 14:51):

e.g. this one https://github.com/coq/coq/pull/15738 is fine but this one is not https://github.com/coq/coq/pull/15746 (note the absence of the gitlab-ci line)

view this post on Zulip Notification Bot (Feb 28 2022 at 14:55):

This topic was moved here from #Coq devs & plugin devs > opam archive CI not reporting status to GitHub by Théo Zimmermann.

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 15:15):

FTR, I couldn't find any trace of a similar error happening six days ago, so that must have been something else.

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 15:45):

FTR, I have pushed a hackish workaround which seems to have fixed the issue. Unfortunately, the long-term fix might be more difficult to design. See details at https://github.com/coq/bot/issues/203.


Last updated: Jan 31 2023 at 10:01 UTC