search

math-comp / docker-mathcomp

Docker images of coq-mathcomp [maintainer=@erikmd]
https://hub.docker.com/r/mathcomp/mathcomp/#supported-tags
BSD 3-Clause "New" or "Revised" License
6 stars 2 forks source link

HB on mathcomp-dev/coq-dev docker image #17

Closed chdoc closed 2 years ago

chdoc commented 2 years ago

For a few days now, the coq-dev - elpi - HB chain fails to build on the mathcomp-dev:coq-dev docker image. From the looks of it, this is due to missing perl libraries:

https://github.com/coq-community/graph-theory/runs/5731921944?check_suite_focus=true

(I hope this is the right place to put this issue)

CC: @gares @erikmd

erikmd commented 2 years ago

Hi @chdoc, thanks for the report.

Apparently this comes from new dependencies of camlp5.

Fortunately, these dependencies have some depext:

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-string-shellquote/conf-perl-string-shellquote.3/opam

I'll have a look when coq-community/docker-base#17 will be propagated to mathcomp images.

Current workaround

In the meantime, you could try inserting (with proper indentation)

sudo apt-get update -y -q
sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends \
  libipc-system-simple-perl libstring-shellquote-perl

before this line.

chdoc commented 2 years ago

It appears that the changes you made yesterday resolved the issue for me: https://github.com/coq-community/graph-theory/actions