Théo Zimmermann (Jul 28 2021 at 14:07): 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
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.
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.
Cyril Cohen (Jul 29 2021 at 09:05):I just added the github app to docker-mathcomp, please tell me if that's enough
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
Pierre Roux (Jan 20 2023 at 08:18):We should ask @Erik Martin-Dorel but I fear his availability is pretty low currently.
Erik Martin-Dorel (Jan 21 2023 at 00:20):Hi @Karl Palmskog @Pierre Roux, thanks for the ping. FYI:
there is indeed a systematic failure on the pipelines, because GitLab's montly CI minutes have expired and the runners need to be restarted or so
(I don't know the details as @Maxime Dénès handles that part, maybe he can take a look at this next Monday?)
regarding the mathcomp/mathcomp-dev:coq-8.17 image, it wasn't available up to now because of a detail to fix, so I opened this PR:
https://github.com/math-comp/math-comp/pull/960 [URL fixed]
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:
Karl Palmskog (Jan 21 2023 at 20:06):re-running a failed job to test
Karl Palmskog (Jan 21 2023 at 20:39):works great, thanks!
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?
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).
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.
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?
Karl Palmskog (Mar 02 2023 at 22:09):since MathComp itself is so stable, do we really want to completely remove the dev images?
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.
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.
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:
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.
Erik Martin-Dorel (Apr 26 2023 at 22:35):Last updated: Jun 01 2023 at 11:01 UTC