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).
I think we can conclude based on other issues that Erik is very busy at the moment.
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
The build runs on Ubuntu, so is it missing opam-depext, or is Ubuntu outside the Debian "os-family"?
I haven't looked at Ubuntu in a while, but it used to be Debian-based. ^^
In analysis, this helped https://github.com/math-comp/analysis/pull/609/commits/62787b3e7d2aa5e58f440cd89afaeb0a1ede994f
(though the coq-dev images are still outdated)
Aah, with opam 2.0.9 it's literally just https://github.com/math-comp/analysis/pull/609#issuecomment-1080435393
Yep, the same should help here
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
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.
@Enrico Tassi I think this is also a good reason to move the opam archive CI to opam 2.1?
Absolutely, I thought we already did it
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?]
looks like we are on 2.0.6 currently: https://github.com/coq/opam-coq-archive/blob/master/.gitlab-ci.yml#L16
I'm opening a PR
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