Maxime Dénès (Jun 06 2023 at 06:59): 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?
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.
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.
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)?
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.
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.
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.
Maxime Dénès (Jun 06 2023 at 07:05):The docker registry is available, yes.
Maxime Dénès (Jun 06 2023 at 07:06):Do you have numbers on our artifacts storage use?
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?
Gaëtan Gilbert (Jun 06 2023 at 07:21):https://gitlab.com/groups/coq/-/usage_quotas#storage-quota-tab
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
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
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
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.
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
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
Maxime Dénès (Jun 06 2023 at 12:16):Ok, I will do the same then (temporarily activate shared runners).
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".
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?
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.
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
Théo Zimmermann (Jun 07 2023 at 12:35):I'm available too.
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...
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
Maxime Dénès (Jun 09 2023 at 07:40):I'll have a look
Maxime Dénès (Jun 09 2023 at 07:40):is the test-docker-machine-driver still ok?
Gaëtan Gilbert (Jun 09 2023 at 07:46):both test- and coq- had failures
Maxime Dénès (Jun 09 2023 at 07:47):probably a CloudStack issue, then, I'll try to get some logs before restarting
Maxime Dénès (Jun 09 2023 at 07:55):hard to tell, I'll clean up and restart
Last updated: Nov 29 2023 at 21:01 UTC