Add basic CI (#2)

Author: kazk

.github/workflows/ci.yml

@@ -0,0 +1,30 @@
+name: CI
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    if: ${{ github.repository == 'codewars/agda' }}
+    steps:
+      - uses: actions/checkout@v2
+      - uses: docker/setup-buildx-action@v2
+
+      - name: Build image
+        uses: docker/build-push-action@v3
+        with:
+          context: .
+          push: false
+          # Make the image available in next step
+          load: true
+          tags: ghcr.io/codewars/agda:latest
+          cache-from: type=gha
+          cache-to: type=gha,mode=max
+
+      - name: Run Passing Example
+        run: bin/run passing
+      - name: Run Failing Example
+        run: bin/run failing | grep 'b != a of type A'

bin/run

@@ -8,7 +8,7 @@ C=$(docker container create --rm -w $W ghcr.io/codewars/agda:latest agda --verbo
 # Copy files from the current directory
 # example/Example.agda
 # example/ExampleTest.agda
-docker container cp example/. $C:$W
+docker container cp examples/${1:-passing}/. $C:$W
 
 # Run tests
 docker container start --attach $C

examples/failing/Example.agda

@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+module Example where
+open import Agda.Builtin.Equality
+
+_⇆_ : {A : Set} {a : A} → a ≡ a → a ≡ a → a ≡ a
+refl ⇆ refl = refl

example/ExampleTest.agda renamed to examples/failing/ExampleTest.agda

@@ -0,0 +1,7 @@
+{-# OPTIONS --safe #-}
+module ExampleTest where
+open import Agda.Builtin.Equality
+open import Example
+
+check : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
+check = _⇆_