Stream: Coq devs & plugin devs

Topic: Docker ToS change


view this post on Zulip Andres Erbsen (Mar 17 2023 at 00:44):

https://blog.alexellis.io/docker-is-deleting-open-source-images/ sounds like it might affect Coq. Do we think it does, specifically did anyone receive an email to this effect? This post's example, https://hub.docker.com/r/curlimages/curl, looks pretty similar to https://hub.docker.com/r/coqorg/coq/ from an outsider's perspective. (There's also an apologies&clarification post by Docker Inc, but after reading it I do not feel comfortable linking to it).

view this post on Zulip Guillaume Melquiond (Mar 17 2023 at 04:54):

You write that Curl is that blog post's example, but there is only one single mention of it in the blog post, and it does not say anything about their images being deleted. Am I misunderstanding something? Also the blog post says that "Docker's Open Source program is hostile and out of touch", but both Coq and Curl are part of this program, so not so "out of touch" (and also not impacted by Docker's change, as far a I can tell).

view this post on Zulip Karl Palmskog (Mar 17 2023 at 08:14):

however, the MathComp images may be affected, if I remember correctly due to Docker not allowing software under CECILL-B/C licenses in their open source program

view this post on Zulip Paolo Giarrusso (Mar 17 2023 at 08:17):

Thanks for the link Andres, but I'm going to link to the blog post (even without endorsing it) https://www.docker.com/blog/we-apologize-we-did-a-terrible-job-announcing-the-end-of-docker-free-teams/ — it specifically claims images are not going to be deleted by Docker, which might make a significant difference...

And indeed https://hub.docker.com/u/mathcomp isn't "Sponsored Open Source" — what's a "community organization"? If they are a "Docker Free Team" (they can check in their account), they're affected and somebody should have gotten an email...

view this post on Zulip Paolo Giarrusso (Mar 17 2023 at 08:19):

Regardless, Docker has been evolving to extract more profit from users (which is legitimate); "Docker sunsets its open source program" (à la Travis) seems now slightly more probable. Does that warrant some effort for risk management?

view this post on Zulip Karl Palmskog (Mar 17 2023 at 08:20):

well, we just got into the open source program with Coq, would be surprising if they sunset it right away

view this post on Zulip Karl Palmskog (Mar 17 2023 at 08:23):

I guess one can do risk management in the sense of, we as a community might prepare to pay some amount to have Docker images around (since right now they are important to testing projects with new Coq versions). Probably there are ways to apply for money for this. The fallback/backup right now is essentially Nix.

view this post on Zulip Paolo Giarrusso (Mar 17 2023 at 08:23):

there are other Docker repositories. And other clients lets you change the default repo from docker hub apparently :-)

view this post on Zulip Karl Palmskog (Mar 17 2023 at 08:25):

sure, but other repos are probably also paid somewhere by someone, then there are possible frictions in changing repos

view this post on Zulip Karl Palmskog (Mar 17 2023 at 08:32):

in any case, the MathComp Docker discussion is best handled elsewhere

view this post on Zulip Andres Erbsen (Mar 17 2023 at 12:44):

If Coq is not affected, that's great. All I'm asking is that we figure out who would have received an email if we were sent one and check that we did not receive one. The curl maintainer did get one https://mastodon.social/@bagder/110032947631819780


Last updated: Jun 23 2024 at 01:02 UTC