Stream: math-comp devs

Topic: Docker images and num

view this post on Zulip Karl Palmskog (Dec 31 2022 at 17:12):

Just a note that the MathComp Docker images that rely on num currently have heavy rebuild times as the regular Coq images did before the recent rebuild. Example job that takes 6x longer on a Coq version that requires num: https://github.com/coq-community/coqeal/actions/runs/3806595409/jobs/6475530660

@Erik Martin-Dorel any chance for a MathComp Docker rebuild?

view this post on Zulip Erik Martin-Dorel (Dec 31 2022 at 17:43):

Hi @Karl Palmskog, yes I was aware of this issue at the time I rebuilt the coqorg/coq images, but the fact is that the mathcomp CI/CD runners were broken, so on December 21 I sent a private Zulip message to @Maxime Dénès (sorry for not posting a public message instead) so that he can take a look as he maintains the inria runners.
But good news: the problem is fixed since Wednesday evening. So now a rebuild is possible.
So I'll rebuild everything tonight (just after bumping dune to 3.6.1)

view this post on Zulip Erik Martin-Dorel (Jan 01 2023 at 21:07):

Hi @Karl Palmskog, FYI coqorg/base and coqorg/coq have been rebuilt with dune 3.6.1;
while mathcomp/mathcomp is on-going, cf. https://gitlab.com/math-comp/docker-mathcomp/-/pipelines/735793000

view this post on Zulip Erik Martin-Dorel (Jan 01 2023 at 21:15):

And I'm thinking more and more about improving docker-keeper further… so that I can just push in coqorg/base, and that's it :)

Last but not least, happy new year! :sparkles:

view this post on Zulip Karl Palmskog (Jan 01 2023 at 21:21):

literal translation of a Swedish saying used after a new year: "good continuation".

view this post on Zulip Karl Palmskog (Jan 01 2023 at 21:23):

if just a push is required, then maybe we can have some redundancy with the push privilege (not necessarily me, but someone in the Coq Team)

Last updated: Oct 12 2024 at 13:01 UTC