HB on mathcomp-dev/coq-dev docker image

[chdoc]

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]

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]

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