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:
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 why188.8.131.52
This works as well.
Here is my Docker script which fails with the above error.
ENV DEBIAN_FRONTEND noninteractive
RUN apt-get update
RUN apt-get install -yq apt-utils
RUN apt-get install -yq --no-install-recommends
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 why184.108.40.206 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.