Stream: Coq devs & plugin devs

Topic: CI infrastructure


view this post on Zulip Maxime Dénès (Jun 06 2023 at 06:59):

Hi there,

Since gitlab.com's change of policy for free CI minutes, we are still running on a somewhat degraded (manually maintained) infrastructure. I initiated some discussion with the Inria teams in charge of CI, and will present them in two weeks our use case and what we tried.

Meanwhile, it could be worth trying to transition our CI backend to the Inria gitlab as was mentioned some time ago.

@Théo Zimmermann is coqbot now ready for that, since it was done for mathcomp?

view this post on Zulip Théo Zimmermann (Jun 06 2023 at 07:00):

It is. But AFAIAA, only math-comp/docker-mathcomp has migrated yet, and this remains to be done for math-comp/math-comp.

view this post on Zulip Théo Zimmermann (Jun 06 2023 at 07:01):

So I would be curious for math-comp/math-comp experience after migrating before Coq does the same.

view this post on Zulip Gaëtan Gilbert (Jun 06 2023 at 07:02):

Meanwhile, it could be worth trying to transition our CI backend to the Inria gitlab as was mentioned some time ago.

What would this gain us?
Does inria gitlab have the docker registry on?
What quotas do they set (our artifacts storage use is pretty large especially)?

view this post on Zulip Maxime Dénès (Jun 06 2023 at 07:02):

Théo Zimmermann said:

So I would be curious for math-comp/math-comp experience after migrating before Coq does the same.

Oh yes, I thought this was done already.

view this post on Zulip Maxime Dénès (Jun 06 2023 at 07:04):

Gaëtan Gilbert said:

Meanwhile, it could be worth trying to transition our CI backend to the Inria gitlab as was mentioned some time ago.

What would this gain us?
Does inria gitlab have the docker registry on?
What quotas do they set (our artifacts storage use is pretty large especially)?

The point is to target an infrastructure that is managed for us and provides us enough resources. If they set something that is not suitable / not enough for us, we should list it and talk to them.

view this post on Zulip Maxime Dénès (Jun 06 2023 at 07:05):

The compute resources will definitely not be enough for now, but if we managed to add the CloudStack-based orchestration on top of it, there's a chance they will generalize it to other projects and maintain it.

view this post on Zulip Maxime Dénès (Jun 06 2023 at 07:05):

The docker registry is available, yes.

view this post on Zulip Maxime Dénès (Jun 06 2023 at 07:06):

Do you have numbers on our artifacts storage use?

view this post on Zulip Maxime Dénès (Jun 06 2023 at 07:11):

Théo Zimmermann said:

It is. But AFAIAA, only math-comp/docker-mathcomp has migrated yet, and this remains to be done for math-comp/math-comp.

@Erik Martin-Dorel is it going to happen?

view this post on Zulip Gaëtan Gilbert (Jun 06 2023 at 07:21):

https://gitlab.com/groups/coq/-/usage_quotas#storage-quota-tab

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2023 at 10:58):

Last time I tried the main problem was the artifact size limit, our _build directory is too big for Inria limits.

If that restriction is lifted, we could have Inria devs use their fork with Inria CI

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2023 at 11:00):

In terms of total storage not so much space is needed, if we want to preserve logs they can be moved to cold storage

view this post on Zulip Maxime Dénès (Jun 06 2023 at 11:58):

Btw, do we have no runners left for building the docker image? https://gitlab.com/coq/coq/-/jobs/4420805963

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2023 at 12:08):

@Maxime Dénès I'm unsure of the status, so far what I've been doing is enabling shared runners for a minute (so the job with the docker tag is picked up by the public runner) then I disable the public runners again.

view this post on Zulip Gaëtan Gilbert (Jun 06 2023 at 12:08):

we never had any
In the past we just turned shared runners on until they picked up the job they turned them back off
I made https://github.com/coq/coq/pull/17246 so we could run just the docker job on shared runners but we never set the env variables to use this system

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2023 at 12:09):

Emilio Jesús Gallego Arias said:

Last time I tried the main problem was the artifact size limit, our _build directory is too big for Inria limits.

If that restriction is lifted, we could have Inria devs use their fork with Inria CI

That could be a nice thing to ask even now, as it will allow us to run some experiments with the branches we have for Inria CI, which could provide some useful info for the presentation to CI folks in the upcoming weeks

view this post on Zulip Maxime Dénès (Jun 06 2023 at 12:16):

Ok, I will do the same then (temporarily activate shared runners).

view this post on Zulip Maxime Dénès (Jun 06 2023 at 14:15):

I put back the CloudStack-based orchestrator, which happens to also provide runners capable of building docker images. FYI, the runner is named "test-docker-machine-driver".

view this post on Zulip Erik Martin-Dorel (Jun 06 2023 at 20:55):

Maxime Dénès said:

Théo Zimmermann said:

It is. But AFAIAA, only math-comp/docker-mathcomp has migrated yet, and this remains to be done for math-comp/math-comp.

Erik Martin-Dorel is it going to happen?

Sure. Thanks for the ping. Recent weeks upto this one were still full of teaching duties…
And I cannot do the migration alone, I'll need to coordinate several actions with @Théo Zimmermann and @Pierre Roux.

@ Théo and Pierre: would you have possible slots to talk about this synchronously on next Monday afternoon, 12 June 2023?

view this post on Zulip Pierre Roux (Jun 07 2023 at 06:44):

I'm not sure how I can help but I'll be available on June 12th before 2pm or after 4pm.

view this post on Zulip Maxime Dénès (Jun 07 2023 at 12:12):

FYI, I'm migrating coq-*.ci runners to ephemeral ones, which should improve the situation on runners having their disk full

view this post on Zulip Théo Zimmermann (Jun 07 2023 at 12:35):

I'm available too.

view this post on Zulip Erik Martin-Dorel (Jun 07 2023 at 20:10):

Great! Thanks @Théo Zimmermann and @Pierre Roux, I propose that we video-meet from 16:00 to 16:30 on June 12 ; I'll send you a zoom link...

view this post on Zulip Gaëtan Gilbert (Jun 09 2023 at 07:12):

the "docker-machine-driver" runners keep dying so I turned them off
eg https://gitlab.com/coq/coq/-/jobs/4444140531 and lots more in that pipeline

view this post on Zulip Maxime Dénès (Jun 09 2023 at 07:40):

I'll have a look

view this post on Zulip Maxime Dénès (Jun 09 2023 at 07:40):

is the test-docker-machine-driver still ok?

view this post on Zulip Gaëtan Gilbert (Jun 09 2023 at 07:46):

both test- and coq- had failures

view this post on Zulip Maxime Dénès (Jun 09 2023 at 07:47):

probably a CloudStack issue, then, I'll try to get some logs before restarting

view this post on Zulip Maxime Dénès (Jun 09 2023 at 07:55):

hard to tell, I'll clean up and restart


Last updated: May 24 2024 at 22:02 UTC