Stream: math-comp devs

Topic: docker-mathcomp CI


view this post on Zulip Théo Zimmermann (Jul 28 2021 at 14:07):

I've seen some coqbot logs that make me think that something is off in the coqbot installation for the docker-mathcomp repository:

Error while creating check run: Server responded to GraphQL request with errors: Resource not accessible by integration

view this post on Zulip Théo Zimmermann (Jul 28 2021 at 14:09):

My interpretation of this is that coqbot is setup on the GitLab side (webhooks) but the GitHub App is not installed on the GitHub repo.

view this post on Zulip Théo Zimmermann (Jul 28 2021 at 14:10):

If that's correct, then this should be fixed by either removing the GitLab webhooks, or extending the repositories where the GitHub App is installed to include this one.

view this post on Zulip Cyril Cohen (Jul 29 2021 at 09:05):

I just added the github app to docker-mathcomp, please tell me if that's enough

view this post on Zulip Karl Palmskog (Jan 20 2023 at 07:56):

is the MathComp dev Docker image getting updated properly? I keep getting coq-elpi issues in CI, even though they have disappeared locally with coq.dev (coq-elpi overlay was merged 2-3 days ago): https://github.com/coq-community/graph-theory/actions/runs/3965033951/jobs/6794395645

view this post on Zulip Pierre Roux (Jan 20 2023 at 08:18):

We should ask @Erik Martin-Dorel but I fear his availability is pretty low currently.

view this post on Zulip Erik Martin-Dorel (Jan 21 2023 at 00:20):

Hi @Karl Palmskog @Pierre Roux, thanks for the ping. FYI:

view this post on Zulip Erik Martin-Dorel (Jan 21 2023 at 19:56):

@Karl Palmskog good news, the latest pipeline succeeded:

https://gitlab.com/math-comp/math-comp/-/pipelines/753938267

Hence these two images:

view this post on Zulip Karl Palmskog (Jan 21 2023 at 20:06):

re-running a failed job to test

view this post on Zulip Karl Palmskog (Jan 21 2023 at 20:39):

works great, thanks!

view this post on Zulip Karl Palmskog (Feb 02 2023 at 10:04):

@Erik Martin-Dorel it's now possible to do mathcomp/mathcomp:1.16.0-coq-8.17. Maybe a good exercise for our new co-maintainer?

view this post on Zulip Reynald Affeldt (Feb 02 2023 at 10:17):

If you are talking about the preparation of docker packages for MathComp 1.16.0, there is actually a PR in progress. It looks like it needs to be mirrored on gitlab and this synchronization is taking time (or needs to be triggered manually).

view this post on Zulip Karl Palmskog (Feb 26 2023 at 09:40):

@Erik Martin-Dorel the mathcomp-dev images seem to be stalled (not getting rebuilt) since a while. Just double-checking if you are aware of this. We noticed since coq-equations.dev no longer builds with the coq-dev MathComp docker image.

view this post on Zulip Erik Martin-Dorel (Mar 02 2023 at 22:08):

Thanks @Karl Palmskog. I was aware of the unresolved unstability of runners. But it seems the issue is even stronger now. Sorry for that.
I plan to video-meet with Maxime next week to look for solutions.
In the meantime, I believe we should remove all stalled images (mathcomp-dev:coq-*), but that would not be a very pleasant move, as we don't have an ETA about the date where we'll be able to rebuild all of them…
WDYT?

view this post on Zulip Karl Palmskog (Mar 02 2023 at 22:09):

since MathComp itself is so stable, do we really want to completely remove the dev images?

view this post on Zulip Karl Palmskog (Mar 02 2023 at 22:09):

I switched to the regular Coq dev images in projects where I needed Hierarchy Builder, etc., but I don't think it hurts keeping the stalled MC ones.

view this post on Zulip Karl Palmskog (Mar 02 2023 at 22:10):

maybe have some timeout, like, if runner problem is not sorted in 1-2 weeks, remove MC dev.

view this post on Zulip Erik Martin-Dorel (Mar 02 2023 at 22:15):

OK, thanks: that looks wise indeed.
Let's hope to have good news by 17 March then :fingers_crossed: :+1:

view this post on Zulip Erik Martin-Dorel (Mar 08 2023 at 10:31):

Just FYI: we video-met with Maxime just now, and we have a 3-step plan to fix/improve math-comp's gitlab ci.
Regarding the first step, the custom runner involved in gitlab.com/math-comp is working again now:
https://gitlab.com/math-comp/math-comp/-/pipelines so the immediate situation is improved a bit.
The other steps need some additional developments; I'll give more details by March 17, as soon as the plan is implemented and whether it is conclusive or not.

view this post on Zulip Erik Martin-Dorel (Apr 26 2023 at 22:35):

Heads-up: see https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/On-going.20migration.20of.20Docker.20mathcomp.20images.20infrastructure/near/352944701

view this post on Zulip Karl Palmskog (Aug 01 2023 at 19:48):

it seems like all mathcomp-dev Docker images are currently rebuilding everything each CI run. Maybe some package issue. mathcomp-dev runs taking 3-4 times the regular runs here: https://github.com/coq-community/gaia/pull/15

view this post on Zulip Paolo Giarrusso (Aug 01 2023 at 22:43):

opam claims it's because menhir* dev have upstream changes

view this post on Zulip Pierre Roux (Aug 02 2023 at 07:22):

It's likely not a package issue. It's a known issue with Docker images, each time the ocaml repo modifies an already released OPAM file that is used in the image (and they do it a lot), the images have to be recompiled by hand (and only Erik can do it). It's very annoying but AFAIK there is currently no known fix.

view this post on Zulip Karl Palmskog (Aug 10 2023 at 12:14):

the problem will likely be fixed (for now) by https://github.com/math-comp/math-comp/pull/1056

view this post on Zulip Karl Palmskog (Nov 22 2023 at 09:10):

@Erik Martin-Dorel it looks like the MathComp 2.0 Docker images for 8.1X are rebuilding all MathComp packages every time, here is an example where deps take 12 min to build: https://github.com/coq-community/reglang/actions/runs/6954961345/job/18922795709?pr=66

Probably an image refresh is needed due to upstream opam changes.

view this post on Zulip Erik Martin-Dorel (Nov 28 2023 at 11:31):

Hi @Karl Palmskog ! thanks a lot, and sorry for not replying earlier this time.
(BTW this would be worth it to automate, maybe… at least dedicated jobs to "detect" this situation; so I'll think more about it soonish in my next docker-keeper sprint)
Meanwhile, I just started a full rebuild of coqorg/base, coqorg/coq, mathcomp/mathcomp, I'll comment here when this is done.

view this post on Zulip Pierre Roux (Nov 28 2023 at 12:50):

I also just updated HB dev https://github.com/coq/opam/pull/2849 so the mathcomp 2/master coq-dev images probably also need rebuilding.

view this post on Zulip Erik Martin-Dorel (Nov 29 2023 at 07:53):

Hi! FYI, here are the latest pending pipelines:

view this post on Zulip Pierre Roux (Nov 29 2023 at 12:39):

Thanks, mathcomp:2.1.0-coq-dev seems to need a rebuild too: https://github.com/math-comp/odd-order/actions/runs/7032594930/job/19136654716?pr=53

view this post on Zulip Pierre Roux (Nov 29 2023 at 13:29):

My bad, mathcomp-2.1.0-coq-dev should rather be removed, since 2.1.0 no longer compiles on Coq master.

view this post on Zulip Erik Martin-Dorel (Dec 01 2023 at 10:39):

Thanks @Pierre Roux, already done:
https://gitlab.inria.fr/math-comp/docker-mathcomp/-/commit/b85d41a42285c29b9bb17715e0ad4fe6f08bf506

view this post on Zulip Karl Palmskog (Jul 12 2024 at 18:56):

@Erik Martin-Dorel I'm seeing package reinstalls in all the stable MathComp Docker images. I don't think I have rights to trigger rebuilds for these images, right? Example: https://github.com/coq-community/autosubst/actions/runs/9912722034/job/27388158931?pr=35

view this post on Zulip Erik Martin-Dorel (Jul 12 2024 at 19:06):

Indeed, I can see - recompile coq-mathcomp-ssreflect 2.2.0* [upstream or system changes]
and you only have commit rights in coq-community.

→ do you have an active gitlab.inria.fr account? I've seen there's x-KPalms but trying to invite you as Developer in docker-mathcomp, I get No matches found

view this post on Zulip Karl Palmskog (Jul 12 2024 at 19:06):

hmm, the account may have expired

view this post on Zulip Karl Palmskog (Jul 12 2024 at 19:07):

let me see if I can reactivate

view this post on Zulip Erik Martin-Dorel (Jul 12 2024 at 19:07):

Yes: maybe you should ask for your Inria sponsor to reactivate it; meanwhile I will push a rebuild commit

view this post on Zulip Karl Palmskog (Jul 12 2024 at 19:09):

Welcome back! Your account had been deactivated due to inactivity but is now reactivated.

view this post on Zulip Erik Martin-Dorel (Jul 12 2024 at 19:09):

OK great :)

view this post on Zulip Erik Martin-Dorel (Jul 12 2024 at 19:11):

I think I can add you as Developer soonish, so that you can push a commit in github (and monitor the docker-mathcomp rebuild in gitlab).

I'll let you know and send you some guidelines by DM

view this post on Zulip Karl Palmskog (Jul 12 2024 at 19:12):

sounds good, I heavily lean on the Docker images for nearly all maintenance work in coq-community / Platform


Last updated: Jul 24 2024 at 11:01 UTC