Stream: Hierarchy Builder devs & users

Topic: build failures on mathcomp/mathcomp-dev:coq-dev docker image


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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"?

view this post on Zulip Christian Doczkal (Mar 31 2022 at 08:43):

I haven't looked at Ubuntu in a while, but it used to be Debian-based. ^^

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Mar 31 2022 at 08:45):

Yep, the same should help here

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Mar 31 2022 at 09:34):

Absolutely, I thought we already did it

view this post on Zulip 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?]

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Mar 31 2022 at 09:38):

I'm opening a PR

view this post on Zulip Enrico Tassi (Mar 31 2022 at 09:41):

https://github.com/coq/opam-coq-archive/pull/2151

view this post on Zulip 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: Sep 28 2023 at 11:01 UTC