Migration to Inria GitLab for CI (instead of GitLab.com) · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Migration to Inria GitLab for CI (instead of GitLab.com)

Théo Zimmermann (Sep 01 2023 at 11:03):

Hi all,
Since Wednesday, we (@Maxime Dénès and I) have switched the GitLab CI of the Coq repository to use Inria GitLab, which allows us to have better managed and more reliable custom runners. There may be some rough edges in the beginning, so please report them here if that's the case.

Théo Zimmermann (Sep 01 2023 at 11:06):

@Erik Martin-Dorel I guess we should duplicate the webhook for Docker-Coq that was present on the Coq GitLab.com repo, correct?

Guillaume Melquiond (Sep 01 2023 at 11:18):

What about the currently pending pull requests? Will they 1. fail, 2. use the old CI, or 3. use the new CI?

Guillaume Melquiond (Sep 01 2023 at 11:20):

Actually, one of those instantly restarted when I took a look at it. Not sure if it is a pure coincidence, of if just looking at them is enough.

Pierre-Marie Pédrot (Sep 01 2023 at 11:21):

It's not magic, I've just restarted two runs to double-check...

Théo Zimmermann (Sep 01 2023 at 11:25):

Guillaume Melquiond said:

What about the currently pending pull requests? Will they 1. fail, 2. use the old CI, or 3. use the new CI?

Any pipeline that was started before the switch will run on the old CI and results will still be reported. Any pipeline started after the switch (including using coqbot commands) should normally run on the new CI, including on old PRs.

Guillaume Melquiond (Sep 01 2023 at 11:26):

Actually, it seems to be running on the new CI, unless Pierre-Marie did something special when restarting it.

Théo Zimmermann (Sep 01 2023 at 11:26):

What did you do to restart the pipelines @Pierre-Marie Pédrot?

Guillaume Melquiond (Sep 01 2023 at 11:26):

(deleted)

Pierre-Marie Pédrot (Sep 01 2023 at 11:29):

I just clicked on "retry failed jobs" in the interface

Théo Zimmermann (Sep 01 2023 at 11:30):

Hum, OK. For this feature, I would have expected it to re-start the jobs on the old CI, but maybe I'm unclear on how this particular feature works...

Pierre-Marie Pédrot (Sep 01 2023 at 11:30):

these pipelines had already run on the new CI, they failed because of some weird transient error

Théo Zimmermann (Sep 01 2023 at 11:30):

Ah OK, that explains it.

Pierre Roux (Sep 01 2023 at 11:51):

BTW, who should we ask to get rights to manually restart jobs?

Maxime Dénès (Sep 01 2023 at 11:55):

What do you need for that? A gitlab account + some membership level in the Coq organization?

Théo Zimmermann (Sep 01 2023 at 12:05):

Yes, but note that you don't need that to restart failed jobs, as this is already doable from the GitHub interface.

Maxime Dénès (Sep 01 2023 at 12:06):

@Pierre Roux Do you have a specific need?

Pierre Roux (Sep 01 2023 at 12:08):

Indeed, that's probably enough for most cases. No specific need but sometimes you just want to restart a specific job (for instance after having updated an overlay).

Théo Zimmermann (Sep 01 2023 at 12:26):

Indeed. We should probably extend the coqbot command language to give every regular Coq contributor the opportunity to perform these operations without needing an Inria GitLab account.

Michael Soegtrop (Sep 01 2023 at 12:41):

@Théo Zimmermann : would it help Coq Platform CI to do a similar move?

Théo Zimmermann (Sep 01 2023 at 12:42):

For sure, we could use it for the Coq Platform CI as well, but this means rewriting the GitHub workflows into GitLab CI pipelines.

Théo Zimmermann (Sep 01 2023 at 12:42):

Note that we can also do a partial move (e.g., start by only moving Linux CI, especially as I don't know whether having Windows / Mac runners would be easy on Inria's GitLab).

Erik Martin-Dorel (Sep 01 2023 at 14:26):

Théo Zimmermann said:

Erik Martin-Dorel I guess we should duplicate the webhook for Docker-Coq that was present on the Coq GitLab.com repo, correct?

I don't think so, the webhook you may be speaking about was useful to trigger a manual CI pipeline in an external repo (i.e., so that each push in coq.master triggers a new pipeline in docker-coq, which is not a mirror of coq, but a sibling repo)

So, this is not needed.

Erik Martin-Dorel (Sep 01 2023 at 14:30):

Pierre-Marie Pédrot said:

these pipelines had already run on the new CI, they failed because of some weird transient error

@Théo Zimmermann This makes me think that after this migration, this feature wish may be important to be addressed:

https://github.com/coq/bot/issues/289

just to summarize the context: I noticed in gitlab.inria.fr/math-comp/docker-mathcomp that when there are pipeline with many jobs (here, 49) and each job requires a docker pull from Docker Hub, the probability of a spurious network failure is high, and having coqbot retry only 3 times automatically and that's all, can be a major usability issue.

Théo Zimmermann (Sep 01 2023 at 14:33):

Erik Martin-Dorel said:

Théo Zimmermann said:

Erik Martin-Dorel I guess we should duplicate the webhook for Docker-Coq that was present on the Coq GitLab.com repo, correct?

I don't think so, the webhook you may be speaking about was useful to trigger a manual CI pipeline in an external repo (i.e., so that each push in coq.master triggers a new pipeline in docker-coq, which is not a mirror of coq, but a sibling repo)

So, this is not needed.

Yes, but we have stopped the mirroring of Coq to GitLab.com, so the Docker-Coq repository will not receive any new webhooks when the Coq repo is updated.

Erik Martin-Dorel (Sep 01 2023 at 14:34):

Ah yes! You're right then, the migration of the webhook is needed as well.

Let me know if I have to check the pipelines logs tonight, after you setup this one.

Guillaume Melquiond (Sep 01 2023 at 15:10):

Erik Martin-Dorel said:

https://github.com/coq/bot/issues/289

just to summarize the context: I noticed in gitlab.inria.fr/math-comp/docker-mathcomp that when there are pipeline with many jobs (here, 49) and each job requires a docker pull from Docker Hub, the probability of a spurious network failure is high, and having coqbot retry only 3 times automatically and that's all, can be a major usability issue.

By curiosity, I went and looked at the issue. It is great that you have exponential backoff, but you are missing an important piece. You need to make the sleep length random. For example, if your current backoff is 25 seconds, you should not sleep for 25 seconds; you should sleep between 25 and 25*2=50 seconds. Otherwise, your 49 failing jobs will all wake up at the exact same time, and thus they will fail again.

Théo Zimmermann (Sep 01 2023 at 15:17):

Thanks for the comment. I think it deserves to be copied over there ;-)

Michael Soegtrop (Sep 01 2023 at 16:50):

@Théo Zimmermann : thanks - I will think about it, but I think I prefer a solution which supports all platforms.

Théo Zimmermann (Sep 01 2023 at 16:59):

Another solution is of course to plug in custom GitHub Actions runners to overcome the 6h limit.

Michael Soegtrop (Sep 01 2023 at 17:03):

Yes. I had a discussion with Romain Tetely (he works with Enrico) yesterday and he want to look into this (using INRA HW).

Emilio Jesús Gallego Arias (Sep 21 2023 at 12:41):

Hi folks, could you maybe update the rest of the CI team on the status and plan for this migration?

In particular I have a few comments:

in the previous attempt to migrate to inria.gitlab.fr we found problems with the limit in artifact size, was this solved?
should we take advantage of the extra tags availabe in Inria CI ? I was able to use those to great benefit actually on my previous attempt
what other steps you had to do to adapt our current setup?
is documentation updated? Does the new setup require extra documentation? I see that our CI docs still mention gitlab.com everywhere

Théo Zimmermann (Sep 21 2023 at 12:52):

in the previous attempt to migrate to inria.gitlab.fr we found problems with the limit in artifact size, was this solved?

I'm not sure what was the limit previously, but it doesn't seem to have hit us this time.

should we take advantage of the extra tags availabe in Inria CI ? I was able to use those to great benefit actually

That's irrelevant to us AFAICT because we are not using the shared runners but another infrastructure that allows us to get pre-configured custom runners. I hope that @Maxime Dénès will be able to do a write-up with links to relevant Inria doc, so that it is easy for others to know what's going on and how to maintain it. AFAIU, the shared runners were too few for the large usage we would have made of it.

what other steps you had to do to adapt our current setup?

Apart from the preliminary tests of Maxime and his interaction with the Inria SED team behind the custom runners infrastructure, not much, because coqbot had already been adapted previously (with Erik) to support pushing to alternative GitLab instances.

is documentation updated? Does the new setup require extra documentation? I see that we our CI docs still mention gitlab.com everywhere

It is not. It has been on my to-do to update it for a few weeks already.

Emilio Jesús Gallego Arias (Sep 21 2023 at 12:54):

I see, I was not aware of the custom runner setup, thanks for the update!

Let me know if you need help with the docs update, we could maybe take this chance to rework a bit the CI docs together like for an hour if you want, and do the rests of TODOs async

Emilio Jesús Gallego Arias (Sep 21 2023 at 12:56):

What are the specs of the custom runners? The large shared runners were pretty nice, so maybe we could selectively use those, but we need to document what Inria SED said about it I guess.

Théo Zimmermann (Sep 21 2023 at 12:58):

From what I've understood, Inria SED said to not use the shared runners for Coq, because the load would be too big. I don't know the spec of the custom runners. I hope they are documented somewhere or will be soon. Maybe we can tag @Thierry Martinez, who probably knows everything about this.

Thierry Martinez (Sep 21 2023 at 13:18):

The documentation for the custom runner is here: https://gitlab.inria.fr/inria-ci/custom-runner/ . It's still in beta: you are welcome to fill new issues (using the same link) if there are unexpected failures. The Coq CI already helped a lot to improve the implementation of the runners.

Emilio Jesús Gallego Arias (Sep 21 2023 at 13:20):

Thanks @Thierry Martinez , oh so the custom runners we are using now, are really managed too, right?

Emilio Jesús Gallego Arias (Sep 21 2023 at 13:21):

The setup looks pretty nice!

Théo Zimmermann (Sep 21 2023 at 13:24):

Thanks to this doc, I realize that there is macOS and Windows support too, so this means that we could migrate our GitHub workflows to use this if we want to. And it could help for the Coq Platform as well.

Emilio Jesús Gallego Arias (Sep 21 2023 at 13:24):

Yes and we get the large runners too, that can really reduce the critical path

Emilio Jesús Gallego Arias (Sep 21 2023 at 13:25):

for example if we implement https://github.com/coq/coq/issues/18050 , a large runner can make the compilation of all plugins pretty quick (one min or so I'd predict)

Michael Soegtrop (Sep 21 2023 at 14:00):

I wonder what I should do with Coq Platform CI. Should I migrate it to gitlab, split it into many small projects ...?

Théo Zimmermann (Sep 21 2023 at 14:04):

Unless you use some advanced GitHub Actions that would be difficult to replace in a GitLab workflow, migrating to GitLab (Inria) could indeed be a reasonable option. Something to discuss with Romain, I suppose!

Michael Soegtrop (Sep 21 2023 at 14:05):

I have a meeting with @Romain Tetley tomorrow and will address this. We need to come back to build full/extended installers in CI.

Gaëtan Gilbert (Sep 21 2023 at 14:33):

BTW looks like we're already using about as much artifact space on inria as on gitlab.com
https://gitlab.inria.fr/coq/coq/-/usage_quotas#storage-quota-tab
https://gitlab.com/groups/coq/-/usage_quotas#storage-quota-tab

Théo Zimmermann (Sep 21 2023 at 14:40):

That's huge and worrying!

Emilio Jesús Gallego Arias (Sep 21 2023 at 15:25):

I guess artifact expiry didn't quick in yet? I wonder what the "stable" size is. 1 TiB of data is indeed a lot, on the other hand seems about right for our load, if that's properly cleaned up.

If that's a problem we could optimize quite a few things I think.

Gaëtan Gilbert (Sep 21 2023 at 15:35):

we had https://docs.gitlab.com/ee/administration/settings/continuous_integration.html#keep-the-latest-artifacts-for-all-jobs-in-the-latest-successful-pipelines checked (I'm unchecking now, it was already unchecked on .com)

Emilio Jesús Gallego Arias (Sep 21 2023 at 15:41):

Nice @Gaëtan Gilbert , maybe we should start collecting these kind of tweaks in a document for the doc update?

Emilio Jesús Gallego Arias (Sep 21 2023 at 15:42):

I tend to forget all these details very quickly

Emilio Jesús Gallego Arias (Sep 21 2023 at 15:43):

Tho that setting should not have a large impact, right? The doc is a bit ambigous.

Gaëtan Gilbert (Sep 21 2023 at 15:51):

with it checked we keep artifacts for all the old open PRs
impact unclear tbh

Emilio Jesús Gallego Arias (Sep 21 2023 at 16:07):

Oh yes, that is because we push the branches to gitlab

Emilio Jesús Gallego Arias (Sep 21 2023 at 16:07):

I was thinking on the case of the main repos where we only have the official branches

Emilio Jesús Gallego Arias (Sep 21 2023 at 16:07):

that's for sure quite a bit of impact, yes

Emilio Jesús Gallego Arias (Sep 21 2023 at 16:12):

Added some notes to the wiki https://github.com/coq/coq/wiki/State-of-the-continuous-integration-infrastructure#migration-to-gitlab-ci

So we can get back to them when updating the docs

Hugo Herbelin (Sep 26 2023 at 18:55):

I don't know if it is already known, gitlab.inria.fr will be unavailable for maintenance from Monday 16 Oct 1pm to, at latest, Tuesday 17 oct 9am (Paris time).

Théo Zimmermann (Sep 27 2023 at 07:58):

Do we want to switch back temporarily to GitLab.com during these planned maintenance downtimes?

Pierre Roux (Sep 27 2023 at 08:52):

If it's only half a day we can probably live with it (I mean, with fiat-crypto, that's just one or two CI cycles).

Théo Zimmermann (Sep 27 2023 at 13:07):

Note that if GitLab Inria is down, any PR updated during the meantime won't have any GitLab CI running at all. It will not just be delayed like with email.

Emilio Jesús Gallego Arias (Sep 27 2023 at 13:13):

I guess the downtime is small enough so we can retrigger the workflows manually.

Théo Zimmermann (Sep 27 2023 at 14:00):

Yep. Using @coqbot run full / light ci is enough to retrigger missing pipelines

Matthieu Sozeau (Sep 28 2023 at 08:42):

IIUC, we have now moved away from GitLab.com's CI so I don't need to renew the OSS program application, right? @Théo Zimmermann, @Maxime Dénès ?

Guillaume Melquiond (Sep 28 2023 at 08:58):

We are still using it for the Opam archive.

Matthieu Sozeau (Sep 28 2023 at 09:07):

Ah, ok

Théo Zimmermann (Sep 28 2023 at 09:10):

And I think that since the migration is very recent, it's safer to keep the option to go back to GitLab.com, at least for the coming year.

Théo Zimmermann (Sep 28 2023 at 09:11):

In one year, we should have gained enough experience, and possibly we will have migrated the opam archive to GitLab Inria as well. We'll see.

Karl Palmskog (Sep 28 2023 at 10:10):

hmm, one drawback of Inria GitLab is that non-Inria people will all need to maintain sponsored accounts, right? adds overhead to co-maintainerships

Théo Zimmermann (Sep 28 2023 at 11:04):

Yes if they need to interact with GitLab directly, but I think we can minimize the number of interactions needed. Currently, it is already possible to restart failed jobs from the GitHub interface. We should add support to allow running other common operations from GitHub.

Thierry Martinez (Sep 30 2023 at 11:02):

I unregistered the runner by mistake from GitLab: I registered it again, but as far as I know, I can't preserve it enable on the projects it was previously enabled, sorry for this. Can anyone with admins right on gitlab.inria.fr/coq/coq enable inria-ci/custom-runner again in https://gitlab.inria.fr/coq/coq/-/settings/ci_cd? (If it is not already the case, I have to add the person to gitlab.inria.fr/inria-ci/custom-runner first.) Thanks, and sorry again. Hopefully, such inconveniences will not happen when the custom runner will be a shared runner in GitLab sense (which should happen soon now).