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?
Example: https://github.com/coq-community/hydra-battles/actions/runs/3306206187/jobs/5456926736
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
@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
@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 ;-)
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?
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.
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
https://gitlab.com/math-comp/docker-mathcomp/-/pipelines/677525406 ; so we'll see the outcome soon :relieved:
It looks like the fix you deployed on mathcomp has worked.
Is this fix already there on the Coq side?
I was convinced it was the same problem because the log were showing the exact same errors.
Yes, it was already on the Coq side, unfortunately.
Last updated: Oct 13 2024 at 01:02 UTC