Merge pull request #3 from codewars/coq-8.15.2

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

examples/failing/Solution.v

@@ -1 +1 @@
-Theorem thm4 : 1 = 1. Proof. reflexivity. Qed.
+Theorem thm4 : 1 = 1. Proof. Admitted.

examples/failing/SolutionTest.v

@@ -1,16 +1,9 @@
-Require Import Solution.
-
-Theorem thm1 : 1 = 1 + 0. Proof. admit. Admitted.
-Print Assumptions thm1.
-
-Parameter thm2 : 1 + 0 = 0 + 1.
-Print Assumptions thm2.
-
-Theorem thm3 : 1 = 0 + 1. Proof. rewrite <- thm2. exact thm1. Qed.
-Print Assumptions thm3.
-
-Theorem thm4_check : 1 = 1.
-Proof.
-  exact thm4.
-  Print Assumptions thm4.
-Qed.
+Require Solution.
+From CW Require Import Loader.
+
+CWGroup "Solution.thm4".
+  CWTest "should have the correct type".
+    CWAssert Solution.thm4 : (1 = 1).
+  CWTest "should be closed under the global context".
+    CWAssert Solution.thm4 Assumes.
+CWEndGroup.

examples/passing/Solution.v

@@ -1,7 +1 @@
-Theorem plus_n_O : forall n:nat, n = n + 0.
-Proof.
-  intros n.
-  induction n.
-  - reflexivity.
-  - simpl. rewrite <- IHn. reflexivity.
-Qed.
+Theorem thm4 : 1 = 1. Proof. reflexivity. Qed.

examples/passing/SolutionTest.v

@@ -1,6 +1,9 @@
-Require Import Solution.
-Theorem plus_n_O_check : forall n:nat, n = n + 0.
-Proof.
-  exact plus_n_O.
-  Print Assumptions plus_n_O.
-Qed.
+Require Solution.
+From CW Require Import Loader.
+
+CWGroup "Solution.thm4".
+  CWTest "should have the correct type".
+    CWAssert Solution.thm4 : (1 = 1).
+  CWTest "should be closed under the global context".
+    CWAssert Solution.thm4 Assumes.
+CWEndGroup.