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: Mar 02 2024 at 17:02 UTC