Installing why3 fails on docker image

Hello,

I have been trying to install Why3 within a docker image. The base system is Debian buster-slim. The error I get is the following:

[ERROR] The sources of the following couldn’t be obtained, aborting:
- dune.2.7.1: Could not extract archive
- stdlib-shims.0.1.0: Could not extract archive

Other packages required for Why3 seem to install successfully, but not these two. The same installation works on a standalone Debian of the same kind.

Any help is highly appreciated.

We are building and deploying an image of Why3 built on top of Debian buster-slim during our continuous integration. I don’t remember ever encountering your issue. Here is our Dockerfile, in case it helps:

1 Like

Hello,

Thank you for your message. I see that you use ocaml from Debian repository. I tried to install everything using opam.

I assume that with this “COPY --chown=guest:guest . /home/guest/why3” you copy and then compile the sources of why3.

I will probably need to follow your approach also.

I just tried it with opam in Docker and it worked for me. Here are the commands I used:

$ docker run --rm -it ocurrent/opam:debian-10-ocaml-4.11
opam@e6b8ea03ff81:~$ opam depext -i why3
[...]
-> installed why3.1.3.3
Done.
2 Likes

This works as well.

Here is my Docker script which fails with the above error.

FROM debian:buster-slim

ENV DEBIAN_FRONTEND noninteractive
RUN apt-get update
RUN apt-get install -yq apt-utils

RUN apt-get install -yq --no-install-recommends
ssl-cert
ca-certificates
gnupg
autoconf
make
m4
patch
gcc
unzip
bubblewrap
nano
sudo
libgmp-dev
zlib1g-dev
pslist
procps
wget
iptables
less
pkg-config

RUN adduser --disabled-password --gecos “” bob

RUN wget https://github.com/ocaml/opam/releases/download/2.0.7/opam-2.0.7-x86_64-linux
RUN cp opam-2.0.7-x86_64-linux /usr/local/bin/opam
RUN chmod ugo+rx /usr/local/bin/opam

RUN su - bob -c ‘opam init -y --disable-sandboxing’
RUN su - bob -c ‘echo “. /home/bob/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true” >> .bash_profile’
RUN su - bob -c ‘opam update -y’
RUN su - bob -c ‘opam install why3.1.3.3 alt-ergo.2.3.3 -y’

The two packages that fail have .tbz archives. I would suggest adding bzip2 to the packages you install, that should hopefully fix your problem.

This fixed my problem. Thank you.