Erik Martin-Dorel

Belated thanks for the suggestions! (and sorry that we didn't answer earlier) While I acknowledge the use case, I believe that the current features of learn-ocaml (version 1.0.0 then 1.1.0)...

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

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

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

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

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

Hi @hendriktews, Thanks for the ping, indeed I had refactored `C-_` feature a while ago (which was fairly broken before my patches) I'd like to let you know that I...

OK great! Thanks Hendrik and Stefan! BTW, if you think it's worth it (?), I could open another issue to track [the "limitation"](https://github.com/ProofGeneral/PG/issues/800#issuecomment-2492595759) I've just talked about… as I'll be...

FYI @CohenCyril @affeldt-aist, Cc @pPomCo this PR looks "ready" but has a merge conflict; I'm going to rebase it right now (and put the CHANGELOG in the new format)

Done. Feel free to take a look, and to *squash-merge* if this looks good to you (as I kept the 4 commits to ease the final review, but keeping them...