Stream: Coq devs & plugin devs

Topic: Coq Docker rate limit


view this post on Zulip Karl Palmskog (Jan 12 2022 at 06:23):

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

view this post on Zulip Karl Palmskog (Jan 12 2022 at 06:26):

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

view this post on Zulip Karl Palmskog (Jan 12 2022 at 06:31):

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.

view this post on Zulip Karl Palmskog (Jan 12 2022 at 06:33):

not sure I understand the anonymous/free distinction, maybe one can authenticate some pulls as mitigation...

view this post on Zulip Théo Zimmermann (Jan 12 2022 at 10:42):

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.

view this post on Zulip Théo Zimmermann (Jan 12 2022 at 10:43):

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.

view this post on Zulip Théo Zimmermann (Jan 12 2022 at 10:44):

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.

view this post on Zulip Théo Zimmermann (Jan 12 2022 at 10:45):

We should probably discuss this in an upcoming Coq-Call if @Erik Martin-Dorel can attend.

view this post on Zulip Karl Palmskog (Jan 12 2022 at 11:07):

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)

view this post on Zulip Maxime Dénès (Jan 12 2022 at 12:56):

If this is for CI, isn't there a Docker image proxy? Gitlab has one.

view this post on Zulip Karl Palmskog (Jan 12 2022 at 13:12):

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)

view this post on Zulip Maxime Dénès (Jan 12 2022 at 13:16):

Ah yes, somehow I missed that part of Théo's message.

view this post on Zulip Erik Martin-Dorel (Jan 12 2022 at 22:54):

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 coqorg namespace…

What are the planned dates/slots for the upcoming Coq-calls? I'd be glad to join if I can.

view this post on Zulip Théo Zimmermann (Jan 13 2022 at 11:10):

@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

view this post on Zulip Erik Martin-Dorel (Jan 13 2022 at 13:15):

@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!

view this post on Zulip Théo Zimmermann (Jan 13 2022 at 15:00):

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.

view this post on Zulip Karl Palmskog (Jan 13 2022 at 15:04):

I only saw it once this week in coq-community, so maybe not super urgent after all.

view this post on Zulip Karl Palmskog (Jan 13 2022 at 15:05):

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...

view this post on Zulip Théo Zimmermann (Jan 13 2022 at 15:20):

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.

view this post on Zulip Karl Palmskog (Jan 13 2022 at 15:22):

OK fine with me.

view this post on Zulip Erik Martin-Dorel (Jan 26 2022 at 11:59):

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 :-/)

view this post on Zulip Karl Palmskog (Jan 26 2022 at 12:01):

OK, then I think we postpone this issue to the next Coq Call?

view this post on Zulip Erik Martin-Dorel (Jan 26 2022 at 12:02):

+1, Looks good to me... thanks.

view this post on Zulip Erik Martin-Dorel (Feb 02 2022 at 18:07):

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

view this post on Zulip Karl Palmskog (Feb 02 2022 at 18:11):

thanks Erik, that looks great.


Last updated: Feb 06 2023 at 01:02 UTC