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.
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.
I just added the github app to docker-mathcomp, please tell me if that's enough
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
We should ask @Erik Martin-Dorel but I fear his availability is pretty low currently.
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?)
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]
@Karl Palmskog good news, the latest pipeline succeeded:
Hence these two images:
re-running a failed job to test
works great, thanks!
@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?
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).
@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.
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…
since MathComp itself is so stable, do we really want to completely remove the
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.
maybe have some timeout, like, if runner problem is not sorted in 1-2 weeks, remove MC
OK, thanks: that looks wise indeed.
Let's hope to have good news by 17 March then :fingers_crossed: :+1:
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.
Heads-up: see https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/On-going.20migration.20of.20Docker.20mathcomp.20images.20infrastructure/near/352944701
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
opam claims it's because menhir* dev have upstream changes
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.
the problem will likely be fixed (for now) by https://github.com/math-comp/math-comp/pull/1056
@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.
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.
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.
Hi! FYI, here are the latest pending pipelines:
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
My bad, mathcomp-2.1.0-coq-dev should rather be removed, since 2.1.0 no longer compiles on Coq master.
Last updated: Dec 01 2023 at 06:01 UTC