Stream: math-comp devs

Topic: extra-dev in mathcomp:1.15.0-coq-8.16


view this post on Zulip Karl Palmskog (Oct 23 2022 at 07:30):

Looks like mathcomp/mathcomp:1.15.0-coq-8.16 Docker image has extra-dev opam repo added by default, is this intended @Erik Martin-Dorel?

view this post on Zulip Karl Palmskog (Oct 23 2022 at 07:31):

Example: https://github.com/coq-community/hydra-battles/actions/runs/3306206187/jobs/5456926736

view this post on Zulip Erik Martin-Dorel (Oct 26 2022 at 09:45):

Hi @Karl Palmskog ! That's a good point, thanks for the ping.

It should not contain extra-dev indeed, the fact is that this stable image is still based on coq 8.16+rc1,
(cf. https://hub.docker.com/layers/mathcomp/mathcomp/latest-coq-8.16/images/sha256-767bb1167021acea88854221f061f1d8cfd5d451e66c4e8e457385159b6fc34e?context=explore )
I wasn't able to rebuild it because of the CI minutes expiration…

and after restarting the build of all math-comp images (to benefit from https://github.com/coq-community/docker-base/pull/21 )
I get a failing pipeline:
https://gitlab.com/math-comp/docker-mathcomp/-/pipelines/677011225

view this post on Zulip Erik Martin-Dorel (Oct 26 2022 at 09:46):

@Maxime Dénès could you have another look at the runner configuration?
because the following pipeline gitlab.com/math-comp/docker-mathcomp fails in an unexpected way:
https://gitlab.com/math-comp/docker-mathcomp/-/pipelines/677011225

see e.g. https://gitlab.com/math-comp/docker-mathcomp/-/jobs/3227412232

Running with gitlab-runner 15.4.0 (43b2dc3d)
on mathcomp-docker-machine-driver kgabKGp-
Preparing the "docker+machine" executor 00:47
ERROR: Preparation failed: exit status 1
Will be retried in 3s ...
ERROR: Preparation failed: exit status 1
Will be retried in 3s ...
ERROR: Preparation failed: exit status 1
Will be retried in 3s ...
ERROR: Job failed (system failure): exit status 1

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 10:03):

@Erik Martin-Dorel This is what I was reporting in #Coq devs & plugin devs > Runner failures on docker-machine runner FTR. Unfortunately, I haven't managed to get Maxime's attention on this point yet, probably because of the holidays ;-)

view this post on Zulip Maxime Dénès (Oct 26 2022 at 10:24):

I'm on holidays, yes. I'm not sure it is the same problem, though. @Erik Martin-Dorel I redeployed the mathcomp runners, can you try again now?

view this post on Zulip Maxime Dénès (Oct 26 2022 at 10:25):

The Coq runners had a fix which hadn't been deployed to the mathcomp ones yet, it should help. On the Coq side, it is not fully stable yet but we have other runners so I think it is safer to wait a bit before putting them back.

view this post on Zulip Erik Martin-Dorel (Oct 26 2022 at 10:39):

Maxime Dénès said:

I'm on holidays, yes. I'm not sure it is the same problem, though. Erik Martin-Dorel I redeployed the mathcomp runners, can you try again now?

OK thanks @Maxime Dénès :+1:

I just launched another pipeline, https://gitlab.com/math-comp/docker-mathcomp/-/pipelines/677419079 ; so we'll see the outcome soon :relieved:

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:35):

It looks like the fix you deployed on mathcomp has worked.

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:35):

Is this fix already there on the Coq side?

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:36):

I was convinced it was the same problem because the log were showing the exact same errors.

view this post on Zulip Maxime Dénès (Oct 28 2022 at 20:12):

Yes, it was already on the Coq side, unfortunately.


Last updated: Jan 29 2023 at 16:02 UTC