Coq 8.15.2

Using the same versions as Coq Platform 2022.04.1 for Coq 8.15.

https://github.com/coq/platform/blob/main/package_picks/package-pick-8.15%7E2022.04.sh

Author: kazk

.github/workflows/ci.yml

@@ -26,3 +26,8 @@ jobs:
 
       - name: Run Passing Example
         run: bin/run passing
+
+      - name: Report Image Size
+        run: |
+          echo "## Image Size" >> $GITHUB_STEP_SUMMARY
+          docker image inspect --format '{{.Size}}' ghcr.io/codewars/coq:latest | numfmt --to=si --suffix=B >> $GITHUB_STEP_SUMMARY

Dockerfile

@@ -1,80 +1,59 @@
-FROM alpine:3.11 AS builder
-
-RUN apk add --no-cache \
-      bash \
-      bubblewrap \
-      build-base \
-      ca-certificates \
-      coreutils \
-      curl \
-      git \
-      m4 \
-      ncurses-dev \
-      opam \
-      ocaml \
-      ocaml-compiler-libs \
-      patch \
-      rsync \
-      tar \
-      xz \
-    ;
-
-# Disable sandboxing
-RUN set -ex; \
-    echo 'wrap-build-commands: []' > ~/.opamrc; \
-    echo 'wrap-install-commands: []' >> ~/.opamrc; \
-    echo 'wrap-remove-commands: []' >> ~/.opamrc; \
-    echo 'required-tools: []' >> ~/.opamrc;
+FROM alpine:3.16
 
 ENV OPAMROOT=/opt/coq \
     OPAMYES=1 \
     OCAML_VERSION=default
-
-RUN set -ex; \
-    mkdir -p /opt/coq; \
-    opam init --no-setup -j 4; \
-    opam repo add coq-released http://coq.inria.fr/opam/released; \
-    opam install -j 4 coq.8.12.0; \
-    opam pin add coq 8.12.0; \
-    opam install \
-      -j 4 \
-      coq-equations.1.2.3+8.12 \
-      coq-mathcomp-ssreflect.1.11.0 \
-    ;
-
 ENV OPAM_SWITCH_PREFIX=/opt/coq/default
 ENV CAML_LD_LIBRARY_PATH=$OPAM_SWITCH_PREFIX/lib/stublibs:$OPAM_SWITCH_PREFIX/lib/ocaml/stublibs:$OPAM_SWITCH_PREFIX/lib/ocaml \
     OCAML_TOPLEVEL_PATH=$OPAM_SWITCH_PREFIX/lib/stublibs/lib/toplevel \
     PATH=$OPAM_SWITCH_PREFIX/bin:$PATH
+
 RUN set -ex; \
+    mkdir -p /opt/coq; \
+    # Work around https://github.com/ocaml/opam/issues/5186 by doing
+    # `apk update` then cleaning up the cache in the same layer.
+    apk update; \
+    apk add \
+        ocaml \
+    ; \
+    apk add --virtual .build-deps \
+        bash \
+        build-base \
+        bubblewrap \
+        ca-certificates \
+        curl \
+        git \
+        m4 \
+        ocaml-ocamldoc \
+        ocaml-compiler-libs \
+        opam \
+        tar \
+    ; \
+    opam init -y --disable-sandboxing; \
+    opam repo add coq-released http://coq.inria.fr/opam/released; \
+    opam install -j 4 \
+    # Let opam install system packages
+        --confirm-level=unsafe-yes \
+    # Use the same versions as Coq Platform so users can easily get the same versions.
+    # https://github.com/coq/platform/blob/main/package_picks/package-pick-8.15%7E2022.04.sh
+        coq.8.15.2 \
+        coq-equations.1.3+8.15 \
+        coq-mathcomp-ssreflect.1.14.0 \
+    ; \
     cd /opt; \
-    git clone --depth 1 --branch v2.0.0 https://github.com/codewars/coq_codewars.git; \
+    mkdir /opt/coq_codewars; \
+    curl -sSL https://github.com/codewars/coq_codewars/archive/refs/tags/v2.0.0.tar.gz | tar xz -C /opt/coq_codewars --strip-components=1; \
     cd coq_codewars; \
     coq_makefile -f _CoqProject -o Makefile; \
-    make;
-
-
-FROM alpine:3.11
+    make; \
+    opam clean --repo-cache; \
+    apk del .build-deps; \
+    rm -rf /var/cache/apk/*;
 
 RUN adduser -D codewarrior
-RUN apk add --no-cache \
-      build-base \
-      ncurses-dev \
-      ocaml \
-    ;
-COPY --from=builder /opt/coq /opt/coq
-COPY --from=builder /opt/coq_codewars/src /opt/coq_codewars/src
-COPY --from=builder /opt/coq_codewars/theories/Loader.vo /opt/coq_codewars/theories/Loader.vo
 RUN set -ex; \
     mkdir -p /workspace; \
-    chown codewarrior:codewarrior /workspace;
+    chown -R codewarrior: /workspace;
 
 USER codewarrior
-ENV OPAM_SWITCH_PREFIX=/opt/coq/default
-ENV USER=codewarrior \
-    HOME=/home/codewarrior \
-    CAML_LD_LIBRARY_PATH=$OPAM_SWITCH_PREFIX/lib/stublibs:$OPAM_SWITCH_PREFIX/lib/ocaml/stublibs:$OPAM_SWITCH_PREFIX/lib/ocaml \
-    OCAML_TOPLEVEL_PATH=$OPAM_SWITCH_PREFIX/lib/stublibs/lib/toplevel \
-    PATH=$OPAM_SWITCH_PREFIX/bin:$PATH
-
 WORKDIR /workspace