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).


Last updated: Feb 09 2023 at 02:02 UTC