Coq Platform scripts on Alpine 3.16 · Coq Platform devs & users

Stream: Coq Platform devs & users

Topic: Coq Platform scripts on Alpine 3.16

Donald Sebastian Leung (Jul 18 2022 at 14:12):

I'm trying to build a container image with Alpine 3.16 as base containing the full Coq Platform 2022.04.1 package set using the platform scripts. Here is my Dockerfile:

FROM docker.io/library/alpine:3.16 AS builder

WORKDIR /tmp

RUN set -ex; \
    apk add --no-cache bash curl alpine-sdk ca-certificates findutils \
      findutils-locate; \
    wget https://github.com/coq/platform/archive/refs/tags/2022.04.1.tar.gz; \
    tar xvf 2022.04.1.tar.gz; \
    rm -vf 2022.04.1.tar.gz;

WORKDIR /tmp/platform-2022.04.1

ENV OPAMROOT=/opt/coq \
    OPAMYES=1 \
    OCAML_VERSION=default \
    COQ_PLATFORM_EXTENT=f \
    COQ_PLATFORM_PACKAGE_PICK_FILE=package_picks/package-pick-8.15~2022.04.sh \
    COQ_PLATFORM_COMPCERT=n \
    COQ_PLATFORM_PARALLEL=p \
    COQ_PLATFORM_JOBS=4 \
    COQ_PLATFORM_SET_SWITCH=y

RUN set -ex; \
    echo "" > stdin; \
    echo "d" >> stdin; \
    ./coq_platform_make.sh < stdin;

# ... (additional details elided as they are deemed non-relevant)

When building the image, I get stuck at the following error:

===== INSTALL OPAM PACKAGES (PARALLEL) =====
[WARNING] Running as root is not recommended
[ERROR] Package conflict!
  * Missing dependency:
    - conf-findutils
    depends on the unavailable system package 'findutils'. Use `--no-depexts' to attempt installation anyway, or it is possible that a depext package name in the opam file is incorrect.

No solution found, exiting
[2/2] STEP 1/11: FROM docker.io/library/alpine:3.16
Error: error building at STEP "RUN set -ex;     echo "" > stdin;     echo "d" >> stdin;     ./coq_platform_make.sh < stdin;": error while running runtime: exit status 1

The error suggests that I don't have findutils installed. But in lines 6-7 of my Dockerfile I've already installed the packages findutils and findutils-locate. Am I misunderstanding the error message?

Paolo Giarrusso (Jul 18 2022 at 14:23):

Hm, the opam package should list which system packages it depends on, but it seems to be set up correctly for alpine?
https://github.com/ocaml/opam-repository/blob/master/packages/conf-findutils/conf-findutils.1/opam#L12

Paolo Giarrusso (Jul 18 2022 at 14:23):

what happens if you do opam install conf-findutils?

Notification Bot (Jul 18 2022 at 14:32):

This topic was moved here from #Coq users > Coq Platform scripts on Alpine 3.16 by Karl Palmskog.

Donald Sebastian Leung (Jul 18 2022 at 14:38):

Thanks, at which stage should I execute this command though? The platform scripts handle the installation of opam at line 58 so it seems I have to patch the script itself to add this command in. Or should I manually install opam and execute the command before running the platform script?

Donald Sebastian Leung (Jul 18 2022 at 14:53):

Okay, I've updated the Dockerfile as follows:

FROM docker.io/library/alpine:3.16 AS builder

WORKDIR /tmp

RUN set -ex; \
    apk add --no-cache bash curl alpine-sdk ca-certificates findutils \
      findutils-locate opam; \
    wget https://github.com/coq/platform/archive/refs/tags/2022.04.1.tar.gz; \
    tar xvf 2022.04.1.tar.gz; \
    rm -vf 2022.04.1.tar.gz;

WORKDIR /tmp/platform-2022.04.1

ENV OPAMROOT=/opt/coq \
    OPAMYES=1 \
    OCAML_VERSION=default \
    COQ_PLATFORM_EXTENT=f \
    COQ_PLATFORM_PACKAGE_PICK_FILE=package_picks/package-pick-8.15~2022.04.sh \
    COQ_PLATFORM_COMPCERT=n \
    COQ_PLATFORM_PARALLEL=p \
    COQ_PLATFORM_JOBS=4 \
    COQ_PLATFORM_SET_SWITCH=y

RUN set -ex; \
    opam init; \
    opam install conf-findutils; \
    echo "" > stdin; \
    echo "d" >> stdin; \
    ./coq_platform_make.sh < stdin;

# ... (elided)

Basically, I now install opam through the system package manager beforehand and run opam install conf-findutils myself. Here's the new error message:

+ opam install conf-findutils
[WARNING] Running as root is not recommended
[ERROR] Package conf-findutils depends on the unavailable system package 'findutils'. You can use `--no-depexts' to attempt installation anyway.
[2/2] STEP 1/11: FROM docker.io/library/alpine:3.16
Error: error building at STEP "RUN set -ex;     opam init;     opam install conf-findutils;     echo "" > stdin;     echo "d" >> stdin;     ./coq_platform_make.sh < stdin;": error while running runtime: exit status 5

So it seems that opam fails to detect the presence of package findutils on Alpine even though it's there (since I explicitly installed findutils with apk already and it succeeded)

Théo Zimmermann (Jul 18 2022 at 14:59):

In principle, even if you hadn't installed findutils, opam should have taken care of installing it. Here the "unavailable system package" message is strange. This might be a bug to report to the opam-repository issues.

Donald Sebastian Leung (Jul 19 2022 at 12:00):

Thanks, I'll consider creating a MWE and submitting an issue ticket to the appropriate repo

Michael Soegtrop (Jul 20 2022 at 09:49):

I don't have time to look at it right now, but if the installtion of a system package does not work, it means the opam package is wrong. Coq Platform comes with a opam patch repo, which is always registered when coq platform creates a switch. So all you need to do is to put a patched opam file into your local copy of (https://github.com/coq/platform/tree/main/opam/opam-repository/packages) and it should work then. The package you need to patch is (https://github.com/ocaml/opam-repository/tree/master/packages/conf-findutils/conf-findutils.1)

Paolo Giarrusso (Jul 20 2022 at 11:19):

FWIW the answer is on https://github.com/ocaml/opam/issues/5186

Last updated: Jun 03 2023 at 03:01 UTC