Christian Doczkal (Mar 31 2022 at 08:33): Christian Doczkal (Mar 31 2022 at 08:33):I'm not sure this is the right place to ask, but the elpi - coq-elpi - HB stack no longer builds on the current mathcomp/mathcomp-dev:coq-dev docker images. I filed an issue on the docker GitHub, but I've received no reaction. Does someone know what's going on? (Feel free to move this thread to the appropriate place).
Karl Palmskog (Mar 31 2022 at 08:35):I think we can conclude based on other issues that Erik is very busy at the moment.
Paolo Giarrusso (Mar 31 2022 at 08:41):I've seen those perl packages, but they seem to have the correct depexts for Debian https://github.com/ocaml/opam-repository/blob/master/packages/conf-perl-ipc-system-simple/conf-perl-ipc-system-simple.3/opam https://github.com/ocaml/opam-repository/blob/master/packages/conf-perl-ipc-system-simple/conf-perl-ipc-system-simple.3/opam
Paolo Giarrusso (Mar 31 2022 at 08:42):The build runs on Ubuntu, so is it missing opam-depext, or is Ubuntu outside the Debian "os-family"?
Christian Doczkal (Mar 31 2022 at 08:43):I haven't looked at Ubuntu in a while, but it used to be Debian-based. ^^
Pierre Roux (Mar 31 2022 at 08:44):In analysis, this helped https://github.com/math-comp/analysis/pull/609/commits/62787b3e7d2aa5e58f440cd89afaeb0a1ede994f
(though the coq-dev images are still outdated)
Paolo Giarrusso (Mar 31 2022 at 08:44):Aah, with opam 2.0.9 it's literally just https://github.com/math-comp/analysis/pull/609#issuecomment-1080435393
Paolo Giarrusso (Mar 31 2022 at 08:45):Yep, the same should help here
Paolo Giarrusso (Mar 31 2022 at 08:48):But shouldn't one call depext on the package you pinned? Elpi’s going to drop the dependency on camlp5 — Enrico already merged the change
Enrico Tassi (Mar 31 2022 at 09:32):I'd love to release a version of Elpi wich optionally depends on camlp5 today, or on Monday at the latest.
In the meanwhile you can either pin elpi to 1.14.1 (if you use an "old" ocaml) or run depext.
In any case the docker images should move to opam 2.1, which would have hidden the depext issue: https://github.com/coq-community/docker-coq/issues/38
I'm sorry Elpi (well, camlp5) is causing such troubles... the next time one has the bright idea to make an ocaml package depend on non standard perl modules "because they are the good libs for the task", well, send him to me first.
Karl Palmskog (Mar 31 2022 at 09:33):@Enrico Tassi I think this is also a good reason to move the opam archive CI to opam 2.1?
Enrico Tassi (Mar 31 2022 at 09:34):Absolutely, I thought we already did it
Enrico Tassi (Mar 31 2022 at 09:34):The two points I raise in that issue have nothing to do with docker actually [sorry, I pointed to another similar issue, where did I open mine?]
Karl Palmskog (Mar 31 2022 at 09:34):looks like we are on 2.0.6 currently: https://github.com/coq/opam-coq-archive/blob/master/.gitlab-ci.yml#L16
Enrico Tassi (Mar 31 2022 at 09:38):I'm opening a PR
Enrico Tassi (Mar 31 2022 at 09:41):https://github.com/coq/opam-coq-archive/pull/2151
Enrico Tassi (Mar 31 2022 at 09:43):Oh, that's my issue, it is actually a PR: https://github.com/coq-community/docker-base/pull/17
Last updated: May 28 2023 at 18:29 UTC