Skip to content

Commit f35ecb5

Browse files
kazkkazk
committed
Add files
1 parent b3bcf66 commit f35ecb5

File tree

11 files changed

+237
-0
lines changed

11 files changed

+237
-0
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
name: CI
2+
on:
3+
push:
4+
branches:
5+
- main
6+
pull_request:
7+
8+
jobs:
9+
build:
10+
runs-on: ubuntu-latest
11+
if: ${{ github.repository == 'codewars/coq' }}
12+
steps:
13+
- uses: actions/checkout@v2
14+
- uses: docker/setup-buildx-action@v2
15+
16+
- name: Build image
17+
uses: docker/build-push-action@v3
18+
with:
19+
context: .
20+
push: false
21+
# Make the image available in next step
22+
load: true
23+
tags: ghcr.io/codewars/coq:latest
24+
cache-from: type=gha
25+
cache-to: type=gha,mode=max
26+
27+
- name: Run Passing Example
28+
run: bin/run passing

‎.github/workflows/push-image.yml‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# Build and push a Docker image to GitHub Container Registry when
2+
# a new tag is pushed.
3+
name: Push Image
4+
5+
on:
6+
push:
7+
tags:
8+
- "*"
9+
10+
jobs:
11+
build-and-push-image:
12+
if: ${{ github.repository == 'codewars/coq' }}
13+
runs-on: ubuntu-latest
14+
permissions:
15+
contents: read
16+
packages: write
17+
steps:
18+
- uses: actions/checkout@v2
19+
20+
- name: Set up Docker Buildx
21+
uses: docker/setup-buildx-action@v2
22+
23+
- name: Login to GitHub Container Registry
24+
uses: docker/login-action@v2
25+
with:
26+
registry: ghcr.io
27+
username: ${{ github.repository_owner }}
28+
password: ${{ secrets.GITHUB_TOKEN }}
29+
30+
- name: Build and push image
31+
uses: docker/build-push-action@v3
32+
with:
33+
context: .
34+
push: true
35+
tags: |
36+
ghcr.io/${{ github.repository_owner }}/coq:latest
37+
ghcr.io/${{ github.repository_owner }}/coq:${{ github.ref_name }}
38+
cache-from: type=gha
39+
cache-to: type=gha,mode=max

‎.gitignore‎

Whitespace-only changes.

‎Dockerfile‎

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
FROM alpine:3.11 AS builder
2+
3+
RUN apk add --no-cache \
4+
bash \
5+
bubblewrap \
6+
build-base \
7+
ca-certificates \
8+
coreutils \
9+
curl \
10+
git \
11+
m4 \
12+
ncurses-dev \
13+
opam \
14+
ocaml \
15+
ocaml-compiler-libs \
16+
patch \
17+
rsync \
18+
tar \
19+
xz \
20+
;
21+
22+
# Disable sandboxing
23+
RUN set -ex; \
24+
echo 'wrap-build-commands: []' > ~/.opamrc; \
25+
echo 'wrap-install-commands: []' >> ~/.opamrc; \
26+
echo 'wrap-remove-commands: []' >> ~/.opamrc; \
27+
echo 'required-tools: []' >> ~/.opamrc;
28+
29+
ENV OPAMROOT=/opt/coq \
30+
OPAMYES=1 \
31+
OCAML_VERSION=default
32+
33+
RUN set -ex; \
34+
mkdir -p /opt/coq; \
35+
opam init --no-setup -j 4; \
36+
opam repo add coq-released http://coq.inria.fr/opam/released; \
37+
opam install -j 4 coq.8.12.0; \
38+
opam pin add coq 8.12.0; \
39+
opam install \
40+
-j 4 \
41+
coq-equations.1.2.3+8.12 \
42+
coq-mathcomp-ssreflect.1.11.0 \
43+
;
44+
45+
ENV OPAM_SWITCH_PREFIX=/opt/coq/default
46+
ENV CAML_LD_LIBRARY_PATH=$OPAM_SWITCH_PREFIX/lib/stublibs:$OPAM_SWITCH_PREFIX/lib/ocaml/stublibs:$OPAM_SWITCH_PREFIX/lib/ocaml \
47+
OCAML_TOPLEVEL_PATH=$OPAM_SWITCH_PREFIX/lib/stublibs/lib/toplevel \
48+
PATH=$OPAM_SWITCH_PREFIX/bin:$PATH
49+
RUN set -ex; \
50+
cd /opt; \
51+
git clone --depth 1 --branch v2.0.0 https://github.com/codewars/coq_codewars.git; \
52+
cd coq_codewars; \
53+
coq_makefile -f _CoqProject -o Makefile; \
54+
make;
55+
56+
57+
FROM alpine:3.11
58+
59+
RUN adduser -D codewarrior
60+
RUN apk add --no-cache \
61+
build-base \
62+
ncurses-dev \
63+
ocaml \
64+
;
65+
COPY --from=builder /opt/coq /opt/coq
66+
COPY --from=builder /opt/coq_codewars/src /opt/coq_codewars/src
67+
COPY --from=builder /opt/coq_codewars/theories/Loader.vo /opt/coq_codewars/theories/Loader.vo
68+
RUN set -ex; \
69+
mkdir -p /workspace; \
70+
chown codewarrior:codewarrior /workspace;
71+
72+
USER codewarrior
73+
ENV OPAM_SWITCH_PREFIX=/opt/coq/default
74+
ENV USER=codewarrior \
75+
HOME=/home/codewarrior \
76+
CAML_LD_LIBRARY_PATH=$OPAM_SWITCH_PREFIX/lib/stublibs:$OPAM_SWITCH_PREFIX/lib/ocaml/stublibs:$OPAM_SWITCH_PREFIX/lib/ocaml \
77+
OCAML_TOPLEVEL_PATH=$OPAM_SWITCH_PREFIX/lib/stublibs/lib/toplevel \
78+
PATH=$OPAM_SWITCH_PREFIX/bin:$PATH
79+
80+
WORKDIR /workspace

‎LICENSE‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MIT License
2+
3+
Copyright (c) 2022 Qualified
4+
5+
Permission is hereby granted, free of charge, to any person obtaining a copy
6+
of this software and associated documentation files (the "Software"), to deal
7+
in the Software without restriction, including without limitation the rights
8+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+
copies of the Software, and to permit persons to whom the Software is
10+
furnished to do so, subject to the following conditions:
11+
12+
The above copyright notice and this permission notice shall be included in all
13+
copies or substantial portions of the Software.
14+
15+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21+
SOFTWARE.

‎README.md‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
# Coq
2+
3+
Container image for Coq used by CodeRunner.
4+
5+
## Usage
6+
7+
```bash
8+
W=/workspace
9+
# Create container
10+
C=$(docker container create --rm -w $W ghcr.io/codewars/coq:latest sh -c "coqc Solution.v && coqc -I /opt/coq_codewars/src -Q /opt/coq_codewars/theories CW SolutionTest.v")
11+
12+
# Copy files from the current directory
13+
# ./Solution.v
14+
# ./SolutionTest.v
15+
docker container cp ./. $C:$W
16+
17+
# Start
18+
docker container start --attach $C
19+
```
20+
21+
## Building
22+
23+
```bash
24+
docker build -t ghcr.io/codewars/coq:latest .
25+
```

‎bin/run‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#!/usr/bin/env bash
2+
set -eu
3+
4+
W=/workspace
5+
# Create container
6+
C=$(docker container create --rm -w $W ghcr.io/codewars/coq:latest sh -c "coqc Solution.v && coqc -I /opt/coq_codewars/src -Q /opt/coq_codewars/theories CW SolutionTest.v")
7+
8+
# Copy files from the current directory
9+
# example/Solution.v
10+
# example/SolutionTest.v
11+
docker container cp examples/${1:-passing}/. $C:$W
12+
13+
# Run tests
14+
docker container start --attach $C

‎examples/failing/Solution.v‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Theorem thm4 : 1 = 1. Proof. reflexivity. Qed.

‎examples/failing/SolutionTest.v‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
Require Import Solution.
2+
3+
Theorem thm1 : 1 = 1 + 0. Proof. admit. Admitted.
4+
Print Assumptions thm1.
5+
6+
Parameter thm2 : 1 + 0 = 0 + 1.
7+
Print Assumptions thm2.
8+
9+
Theorem thm3 : 1 = 0 + 1. Proof. rewrite <- thm2. exact thm1. Qed.
10+
Print Assumptions thm3.
11+
12+
Theorem thm4_check : 1 = 1.
13+
Proof.
14+
exact thm4.
15+
Print Assumptions thm4.
16+
Qed.

‎examples/passing/Solution.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
Theorem plus_n_O : forall n:nat, n = n + 0.
2+
Proof.
3+
intros n.
4+
induction n.
5+
- reflexivity.
6+
- simpl. rewrite <- IHn. reflexivity.
7+
Qed.

0 commit comments

Comments
 (0)