Stream: coqbot devs & users

Topic: opam archive CI seems dead

Karl Palmskog (Aug 26 2020 at 14:27):

Since 1-2 days ago, we don't get any CI jobs from pull requests to the opam archive. @Enrico Tassi do you know what's going on?

Enrico Tassi (Aug 26 2020 at 14:46):

Hum no. @Théo Zimmermann any clue? Is it related to the recent coqbot changes?

Théo Zimmermann (Aug 26 2020 at 15:01):

There were several problems that were reported and that were fixed already so let me know if this is still the case with new of updated PRs.

Karl Palmskog (Aug 26 2020 at 15:45):

@Théo Zimmermann I just opened a new opam archive PR, still no CI: https://github.com/coq/opam-coq-archive/pull/1403

Karl Palmskog (Aug 26 2020 at 15:50):

on the other hand, it looks like this commit got a CI run on merge: https://github.com/coq/opam-coq-archive/commit/b206d27e4c03596ab3bb07c3967c0783bb96526e

Karl Palmskog (Aug 26 2020 at 17:00):

ah, now my force-pushed PR started its CI, let me see if it persists

Karl Palmskog (Aug 26 2020 at 18:08):

hmm, maybe this is related to GitLab pipeline/job limitations?

Karl Palmskog (Aug 26 2020 at 18:25):

it looks like the jobs are being run, but nothing is reported back on GitHub: https://gitlab.com/coq/opam-coq-archive/-/pipelines

Théo Zimmermann (Aug 26 2020 at 18:37):

OK I know what the issue is.

Théo Zimmermann (Aug 26 2020 at 18:46):

FTR here it is: coqbot used to push status checks as a normal user. Now it supports posting them as a GitHub App (but also the old method for backward compatibility). The GitHub App was installed on the Coq repository but only given access to the Coq repository and not the opam-coq-archive repository. Thus, attempts to push status checks (as an App) for the latter were rejected. I fixed this by extending the installation of the App and I've resent a few webhooks to make sure that was it.

Notification Bot (Aug 26 2020 at 18:46):

This topic was moved here from #Coq devs & plugin devs > opam archive CI seems dead by Théo Zimmermann

Karl Palmskog (Aug 26 2020 at 18:51):

that makes sense, thanks for the fix, I thought I was going to spend the week cross-referencing between GitHub and GitLab

Théo Zimmermann (Aug 26 2020 at 18:58):

When you see such issues, feel free to ping me immediately.

Karl Palmskog (Aug 26 2020 at 18:59):

sure, now that I know how it works at a high level. I just review the PRs and merge over here...

Last updated: Sep 28 2023 at 10:01 UTC