From 31adb77fe8efb647bf41afa7b56bfd2756e072de Mon Sep 17 00:00:00 2001 From: kazk Date: Wed, 10 Aug 2022 18:49:23 -0700 Subject: [PATCH 1/2] 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 --- .github/workflows/ci.yml | 5 ++ Dockerfile | 101 ++++++++++++++++----------------------- 2 files changed, 45 insertions(+), 61 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 35beaba..60622fe 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Dockerfile b/Dockerfile index 0533034..8c1a4de 100644 --- a/Dockerfile +++ b/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 From 481e8542b30194f85d26f7d098d0bdc16b2fd6e2 Mon Sep 17 00:00:00 2001 From: kazk Date: Wed, 10 Aug 2022 20:00:21 -0700 Subject: [PATCH 2/2] Update examples to use coq_codewars --- examples/failing/Solution.v | 2 +- examples/failing/SolutionTest.v | 25 +++++++++---------------- examples/passing/Solution.v | 8 +------- examples/passing/SolutionTest.v | 15 +++++++++------ 4 files changed, 20 insertions(+), 30 deletions(-) diff --git a/examples/failing/Solution.v b/examples/failing/Solution.v index 86b34a6..01d5f11 100644 --- a/examples/failing/Solution.v +++ b/examples/failing/Solution.v @@ -1 +1 @@ -Theorem thm4 : 1 = 1. Proof. reflexivity. Qed. +Theorem thm4 : 1 = 1. Proof. Admitted. diff --git a/examples/failing/SolutionTest.v b/examples/failing/SolutionTest.v index 61a123c..daf5b4b 100644 --- a/examples/failing/SolutionTest.v +++ b/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. diff --git a/examples/passing/Solution.v b/examples/passing/Solution.v index 487879b..86b34a6 100644 --- a/examples/passing/Solution.v +++ b/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. diff --git a/examples/passing/SolutionTest.v b/examples/passing/SolutionTest.v index dce7d63..daf5b4b 100644 --- a/examples/passing/SolutionTest.v +++ b/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.