docker pull limit exceeded in CI

[hendriktews]

We now and then have CI tests where pulling the docker image fails with

Pull docker image
  COQ_IMAGE=proofgeneral/coq-emacs:coq-8.11.2-emacs-30.1
  
  Error response from daemon: No such image: proofgeneral/coq-emacs:coq-8.11.2-emacs-30.1
  Error response from daemon: toomanyrequests: You have reached your unauthenticated pull rate limit. https://www.docker.com/increase-rate-limit

If it is really the pull rate, I would expect that the last 20 or 50 tests from one run all fail with this message. However, I have seen only one or two tests failing like this in one run. Anyway, one can increase the limit by authenticating, see https://docs.docker.com/docker-hub/usage/ (note that other sources say that the limit is 10 per hour) and there is a login action (https://github.com/docker/login-action). What is not clear to me yet is where to store the docker access token in github and whether one could use an access token from the proofgeneral team on docker.

[erikmd]

Hi @hendriktews, Okay. This is not that surprising because Docker Hub limits the unauthenticated pulls to 100 pulls per hour for a given IP. See also this recent post of mine: https://bsky.app/profile/erikmartindorel.bsky.social/post/3llru2ma73s2y

So, either we apply to Docker Hub's OSS Sponsoring, which will fully lift this rate-limit. (This is what we did with https://hub.docker.com/u/coqorg and https://hub.docker.com/u/rocq .) Or we switch from Docker Hub to another container registry, like GitHub's or GitLab's (which TTBOMK, have no rate limit, albeit they are not regarded as "standard"… but this wouldn't matter much maybe, as the PG images are not intended to be useful for external users).

With the former solution, note that I couldn't apply to Docker Hub's OSS Sponsoring myself because one Docker user can only do one application for one Docker Hub organization. With the latter solution, it would be necessary to repush all images manually (unless we use an automated CI script (like docker-keeper or so) to populate the new container registry).

However, I'd be wary to switch to authenticated pulls (because in this case, the Docker Hub credentials would be used to test external PRs…), and moreover, this would only bump from 100 pulls per hour to 200 pulls per hour (so, without really addressing the issue).

[erikmd]

However, I'd be wary to switch to authenticated pulls (because our Docker Hub credentials should be used to test external PRs…), and moreover, this would only bump from 100 pulls per hour to 200 pulls per hour (so, without really addressing the issue).

[monnier]

Is it just me, or are those CI processes really wasteful? [ Not that PG is doing something worse than others: it just seems to be considered "par for the course". ]

[erikmd]

Is it just me, or are those CI processes really wasteful? [ Not that PG is doing something worse than others: it just seems to be considered "par for the course". ]

I don't know if your question was about the need to build Docker images of PG, or the use of CI/CD itself for PG:

• Regarding CI/CD, it's a necessary quality assurance infrastructure nowadays, and it is actually ways cheaper than the cost of current AI/LLM trends…
• Also, PG itself has to be kept compatible with many Emacs and Coq versions, so we must verify this in a systematic way, upstream. @hendriktews did a very meticulous job (with a dedicated tooling he develops) to select a "reasonable" subset of the whole matrix of {supported versions of Emacs} × {supported versions of Coq/Rocq versions}.
• Finally regarding the Docker images of PG: they are specifically devised to pre-build all dependencies for the various CI/CD jobs, so that none of them requires to re-build Coq or so at CI time. So this feature can be especially viewed as a "performance optimization".

Anyway, there is a hindrance with the current infrastructure currently (Docker Hub's rate-limit), so I guess we'll need to choose one solution to avoid it: suggested two of them in https://github.com/ProofGeneral/PG/issues/823#issuecomment-2775666101, which has diffrent pros/cons… @hendriktews, do you think we would arrange some video-meeting in a few days to decide this?

[monnier]

Is it just me, or are those CI processes really wasteful? [ Not that PG is doing something worse than others: it just seems to be considered "par for the course". ] I don't know if your question was about the need to build Docker images of PG, or the use of CI/CD itself for PG:

Neither, it was more a comment about the state of the world. AFAICT there's simply no way to use a CI system like Github's without such absurd waste. And AFAIK Github is no worse than others in this respect.

Of course, one can hope that MS is clever enough to implement a crapload of caching/memoizing to try and compensate, but the "pull limit exceeded" suggests that, if they do, it's not working well enough for the way we use it.

[erikmd]

Okay! But the "pull limit exceeded" is not triggered by GitHub (but by Docker Hub, which is the default Docker registry)

[monnier]

Okay! But the "pull limit exceeded" is not triggered by GitHub (but by Docker Hub, which is the default Docker registry)

Oh, I thought it was due to Github's CI pulling too many times from Docker Hub?

[erikmd]

I thought it was due to Github's CI pulling too many times from Docker Hub?

Yes, I guess GitHub CI runners form a pool of IPs, which are shared between many projects, so if we are unlucky, we can hit the 100 hits/hour limit of Docker Hub's free tier. Unless the Docker Hub repository at stake is an OSS sponsored project (which is the case of the rocq Docker images that I co-maintain with @himito). Or alternatively, we could use another Docker registry.