Stream: coq-community devs & users

Topic: GitLab pipeline on coq-community/docker-base does not start?


view this post on Zulip Erik Martin-Dorel (Jun 29 2020 at 17:02):

Hi @Théo Zimmermann @Anton Trunov, just FYI the migration I had outlined in https://github.com/coq-community/docker-coq/issues/4 (from multi-branches Docker Hub builds to single-branch GitLab CI) is now complete − I just need to deploy the configuration I devised.

So after doing some successful tests in a private gitlab.com repo, I've just pushed a new master here:
https://gitlab.com/coq-community/docker-base/-/tree/master

However I don't understand why no pipeline starts… given there is now some .gitlab-ci.yml committed in the master branch!

Any idea/advice? (normally you are both Owners of this coq-community/docker-base repo).

view this post on Zulip Erik Martin-Dorel (Jun 29 2020 at 17:37):

actually it seems there is an on-going issue with the infrastructure of GitLab CI, according to the e-mail below I received (FYI I had subscribed to both GitLab status and GitHub status notifications).

Status update from GitLab System Status

Current Status: Degraded Performance
Started: June 29, 2020 15:18 UTC
Resolved:

Affected Infrastructure:
Components: API, Background Processing, CI/CD, Canary, Git (ssh and https), Windows Runners
(beta),Website
Locations: Google Compute Engine

Update: We have no material update to provide at this time but are still closely monitoring our
infrastructure and are strategizing on how to scale up our fleet to compensate.

Status Page: https://status.gitlab.com

view this post on Zulip Erik Martin-Dorel (Jun 29 2020 at 17:59):

unfortunately it does not seem to work yet:
I started manually a pipeline on branch stage and it was OK:
https://gitlab.com/coq-community/docker-base/-/pipelines
but no pipeline seems to be started automatically on a push to (GitHub) branch…

view this post on Zulip Paolo Giarrusso (Jun 29 2020 at 18:16):

Fwiw Travis seems also in trouble because of Google Cloud https://www.traviscistatus.com/, sounds like an “Internet is down” day?

view this post on Zulip Erik Martin-Dorel (Jun 29 2020 at 18:16):

@Théo Zimmermann in the meantime, I have configured coq bot for both repos (to be able to handle further PRs for docker-base / docker-coq); normally you'll receive an invitation for that.

view this post on Zulip Paolo Giarrusso (Jun 29 2020 at 18:24):

Fwiw https://status.cloud.google.com/incident/compute/20004 and https://status.cloud.google.com/incident/cloud-networking/20005 have details on the underlying issues

view this post on Zulip Erik Martin-Dorel (Jun 29 2020 at 22:09):

I've just been able to "workaround" the issue I mentioned by starting pipelines manually…

Actually I dived in the GitLab CI documentation, and I found this:

However the documented "Trigger pipelines for mirror updates" option was not mentioned at all in the settings:

@Théo Zimmermann do you think there was a recent (not yet documented) change that prevents configuring pipelines to be automatically run from mirror updates? or is this feature normally provided by coqbot?

view this post on Zulip Théo Zimmermann (Jun 30 2020 at 07:37):

IIRC this option is available when creating the repository as a mirror (the "mirror for CI/CD only" being the best creation method). I don't recall where to find it otherwise.

view this post on Zulip Théo Zimmermann (Jun 30 2020 at 07:37):

We could delete and recreate these repositories if needed.

view this post on Zulip Erik Martin-Dorel (Jun 30 2020 at 10:27):

We could delete and recreate these repositories if needed.

OK @Théo Zimmermann, hopefully this will address the issue; so could you do it for both projects?

(I can't do it myself as I'm not an owner of the projects)

view this post on Zulip Théo Zimmermann (Jun 30 2020 at 17:38):

Doing this right now.

view this post on Zulip Théo Zimmermann (Jun 30 2020 at 17:43):

Done but I'm not sure it changed anything. No pipeline was triggered upon creation. This might be different when you push though.

view this post on Zulip Erik Martin-Dorel (Jun 30 2020 at 18:22):

Hi @Théo Zimmermann, thanks; can you re-add me with the Maintainer role in both projects?

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

Done

view this post on Zulip Erik Martin-Dorel (Jul 01 2020 at 10:04):

Hi, good news: a git push now triggers a branch pipeline for both repos :) thanks a lot @Théo Zimmermann!


Last updated: Feb 04 2023 at 03:30 UTC