Erik Martin-Dorel

FTR, today (2024-07-02) in a 1-job pipeline, gitlab.inria.fr failed with: https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/4509247 ``` (...) $ pwd /builds/2mk6rsew/0/math-comp/docker-mathcomp $ /usr/bin/env bash -e -c ' # collapsed multi-line command bash Error response from...

FYI @Zimmi48 : @palmskog and I we got new 502 errors at `docker pull` time with this message ↑ I believe this form of the error message is not covered...

@Zimmi48 > What about entirely disabling the mirroring for projects which choose to use coqbot for this task? Yes of course, if coqbot could perform the "fast-forward push mirroring of...

OK @Zimmi48, looks great !

Hi @Zimmi48 , I've just tested the coqbot-app in docker-coq and the Checks tab (listing all GitLab CI jobs) is very nice! → https://github.com/coq-community/docker-coq/pull/14/checks Some small suggestions BTW, regarding the...

> Perhaps it should be configurable? I guess it would be a nice feature indeed! > Maybe something like coqbot minimize optional-coq-version? yes… in this case, I guess one could...

> Current workflow: I should go to Docker Hub and find what OCaml versions are available for 8.14. OK, looks fine. > Is there a way to get notified of...

Anyway, beyond what I said in my previous comment, I could think of automating things further in the short run, namely: the Coq/OCaml correspondence that appears in https://github.com/coq-community/docker-coq/wiki#ocaml-versions-policy: ```yaml *...

Hi @JasonGross ! thanks, yes, that looks both sensible and feasible. Regarding the feasibility, this would just amount to implementing in docker-coq the same feature as [this one discussed on...

Hi @brandenburg, thanks for opening this issue! 🙂 Actually, this is precisely on the roadmap: we already had a meeting this week with @MSoegtropIMC and @Zimmi48 to discuss this objective,...