The following is a really bad sign (from here):
COQ_IMAGE=coqorg/coq:dev Error response from daemon: toomanyrequests: You have reached your pull rate limit. You may increase the limit by authenticating and upgrading: https://www.docker.com/increase-rate-limit
A Docker Pro subscription which makes the rate problems go away is apparently $60 USD/year, is this something Inria / Coq Consortium might pay for @Maxime Dénès? See https://www.docker.com/increase-rate-limits and https://www.docker.com/pricing
I think we are expected to run into this a lot in the future:
The rate limits of 100 container image requests per six hours for anonymous usage, and 200 container image requests per six hours for free Docker accounts are now in effect. Image requests exceeding these limits will be denied until the six hour window elapses.
And here is the increased limit, probably enough for a couple of years...
Upgrade to Pro or Team if necessary. One of the key benefits is an increased number of pulls to 5,000 in a 24 hour period from Docker Hub.
not sure I understand the anonymous/free distinction, maybe one can authenticate some pulls as mitigation...
My understanding is that the limits and the subscriptions are on the user-side, not on the Docker image publisher-side. Therefore, while we may pay a subscription to avoid this problem in Coq-community, this won't avoid the problem for other users. On the other hand, there are ways to lift the limits on the publisher-side, such as: https://www.docker.com/blog/expanded-support-for-open-source-software-projects/. We could submit an application to this program.
FTR when DockerHub announced these rate limits last year, we discussed this issue with @Erik Martin-Dorel and considered another option, which would be to cross-publish the Docker-Coq images on the GitHub Docker registry (which IIUC doesn't have such pull limits in place). This would leave the choice to users to use the DockerHub or the GitHub registry images.
Furthermore, the default images used in Docker-Coq-Action could very easily be replaced by the ones on the GitHub registry in a patch-level update of Docker-Coq-Action, as this would be fully transparent for the users.
We should probably discuss this in an upcoming Coq-Call if @Erik Martin-Dorel can attend.
if we can be part of the open source program thingy, that would be a nice centralized container service to provide to the community at large (even to commercial industrial users)
If this is for CI, isn't there a Docker image proxy? Gitlab has one.
I think that's the GitHub Docker registry Théo talked about? Not sure how I would use that in my CI configuration (needs input from Érik)
Ah yes, somehow I missed that part of Théo's message.
Théo Zimmermann said:
We should probably discuss this in an upcoming Coq-Call if Erik Martin-Dorel can attend.
Hi all; thanks @Théo Zimmermann for the ping!
Indeed, cross-deploying each image after each build to one more Docker registry is something we considered with Théo, which we can implement with a slight extension of the current build system (GitLab CI +docker-keeper).
When discussing the first time about this, we were not sure actually whether the new rate limits could be reached in practice with GHA and other CI providers thanks to their multiple-IPs available and so on (so we especially focused on other tasks), but this thread now shows it can occur.
Anyway, independently of this solution, we may also want to apply to the Open Source Project Qualification for the
What are the planned dates/slots for the upcoming Coq-calls? I'd be glad to join if I can.
@Erik Martin-Dorel We meet every Wednesday at 4pm (so right after our survey WG slot). Is this a time which you could make? If yes, we can add a point on the agenda (e.g., for next week). See https://github.com/coq/coq/wiki/Coq-Calls
@Théo Zimmermann Okay!
it happens I already have another constraint on next Wednesday 19 at 4pm-6pm; while Wednesday 26 January 4pm would be very fine!
so, do you believe we could add this point to the agenda of Wed. 2022-01-26?
if not (if you consider tackling this point is that urgent), I could try to postpone my constraint to be available on next slot, 2022-01-19…
Tell me what you think!
I'm not sure how urgent it is. @Karl Palmskog may have some hints. If it is very urgent, then we should act now, without even waiting for next week. If it's not so urgent (doesn't happen that often), then we can add this point on the agenda for the 26th.
I only saw it once this week in coq-community, so maybe not super urgent after all.
so we could go with Jan 26.
Doesn't prevent submitting an application to Docker open source in the meantime if it's easy though...
Sure, but I would usually defer this kind of (official) thing to Matthieu, so that's why I proposed raising the point in a Coq Call.
OK fine with me.
Hi @Karl Palmskog @Théo Zimmermann I know there will be some Coq call at 4:00 pm, but I'm afraid I won't be able to join serenely today because of teaching (several hard deadlines for submitting grades before the end of the week :-/)
OK, then I think we postpone this issue to the next Coq Call?
+1, Looks good to me... thanks.
Hi @Matthieu Sozeau @Karl Palmskog @Théo Zimmermann,
just FTR, I've written some notes in https://github.com/coq/coq/wiki/Coq-Call-2022-02-02 to recap the conclusions we reached at the Coq call.
Have a nice evening
thanks Erik, that looks great.
Last updated: Dec 05 2023 at 12:01 UTC