Skip to content

Commit 4ed3e27

Browse files
committed
Add files
1 parent 72b4499 commit 4ed3e27

File tree

6 files changed

+159
-0
lines changed

6 files changed

+159
-0
lines changed

.github/workflows/push-image.yml

+39
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/agda' }}
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@v1
22+
23+
- name: Login to GitHub Container Registry
24+
uses: docker/login-action@v1
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@v2
32+
with:
33+
context: .
34+
push: true
35+
tags: |
36+
ghcr.io/${{ github.repository_owner }}/agda:latest
37+
ghcr.io/${{ github.repository_owner }}/agda:${{ github.ref_name }}
38+
cache-from: type=gha
39+
cache-to: type=gha,mode=max

.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
*.agdai

Dockerfile

+60
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
FROM alpine:3.9 AS builder
2+
RUN apk add --no-cache \
3+
libffi-dev \
4+
ncurses-dev \
5+
alpine-sdk \
6+
musl-dev \
7+
zlib-dev \
8+
ghc \
9+
cabal
10+
COPY rootfs/root/.cabal/config /root/.cabal/config
11+
RUN set -ex; \
12+
mkdir -p /opt/agda; \
13+
cabal update; \
14+
cabal install \
15+
alex \
16+
happy \
17+
Agda-2.6.0.1 \
18+
;
19+
20+
ENV PATH=/opt/agda/bin:$PATH
21+
# Install standard-library and cubical
22+
RUN set -ex; \
23+
git clone --depth 1 --branch v1.0.1 https://github.com/agda/agda-stdlib.git /opt/agda/agda-stdlib; \
24+
cd /opt/agda/agda-stdlib; \
25+
cabal install; \
26+
# Type check all files in standard-library so that it doesn't need to be checked on every user submission.
27+
dist/build/GenerateEverything/GenerateEverything; \
28+
agda -i. -isrc Everything.agda; \
29+
git clone https://github.com/agda/cubical /opt/agda/cubical; \
30+
cd /opt/agda/cubical; \
31+
# Use a version before the change incompatible with v2.6.0. https://github.com/agda/cubical/issues/145
32+
git checkout b1fddc15b80ed9569224b8a1461ae5f879dab826; \
33+
make;
34+
35+
36+
FROM alpine:3.9
37+
RUN apk add --no-cache \
38+
libffi \
39+
ncurses \
40+
gmp-dev \
41+
;
42+
COPY --from=builder /opt/agda/bin/agda /opt/agda/bin/agda
43+
COPY --from=builder /opt/agda/share /opt/agda/share
44+
COPY --from=builder /opt/agda/agda-stdlib /opt/agda/agda-stdlib
45+
COPY --from=builder /opt/agda/cubical /opt/agda/cubical
46+
47+
RUN set -ex; \
48+
adduser -D codewarrior; \
49+
mkdir /workspace; \
50+
chown -R codewarrior:codewarrior /workspace;
51+
52+
USER codewarrior
53+
ENV USER=codewarrior HOME=/home/codewarrior PATH=/opt/agda/bin:$PATH
54+
55+
RUN set -ex; \
56+
mkdir -p /workspace/agda; \
57+
mkdir -p $HOME/.agda; \
58+
echo '/opt/agda/agda-stdlib/standard-library.agda-lib' > $HOME/.agda/libraries; \
59+
echo '/opt/agda/cubical/cubical.agda-lib' >> $HOME/.agda/libraries;
60+
WORKDIR /workspace/agda

LICENSE

+21
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

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
# Agda
2+
3+
Container image for Agda used by CodeRunner.
4+
5+
## Usage
6+
7+
```bash
8+
W=/workspace/agda
9+
# Create container
10+
C=$(docker container create --rm -w $W ghcr.io/codewars/agda:latest agda --verbose=0 --include-path=. --library=standard-library --library=cubical ExampleTest.agda)
11+
12+
# Copy files from the current directory
13+
# Example.agda
14+
# ExampleTest.agda
15+
docker container cp ./. $C:$W
16+
17+
# Run tests
18+
docker container start --attach $C
19+
```
20+
21+
## Building
22+
23+
```bash
24+
$ docker build -t ghcr.io/codewars/agda:latest .
25+
```

rootfs/root/.cabal/config

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
repository hackage.haskell.org
2+
url: http://hackage.haskell.org/
3+
4+
remote-repo-cache: /root/.cabal/packages
5+
world-file: /root/.cabal/world
6+
extra-prog-path: /opt/agda/bin
7+
symlink-bindir: /opt/agda/bin
8+
build-summary: /root/.cabal/logs/build.log
9+
remote-build-reporting: anonymous
10+
jobs: $ncpus
11+
12+
install-dirs user
13+
prefix: /opt/agda

0 commit comments

Comments
 (0)