Add files

Author: kazk

.github/workflows/push-image.yml

@@ -0,0 +1,39 @@
+# Build and push a Docker image to GitHub Container Registry when
+# a new tag is pushed.
+name: Push Image
+
+on:
+  push:
+    tags:
+      - "*"
+
+jobs:
+  build-and-push-image:
+    if: ${{ github.repository == 'codewars/lean' }}
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      packages: write
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v1
+
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@v1
+        with:
+          registry: ghcr.io
+          username: ${{ github.repository_owner }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Build and push image
+        uses: docker/build-push-action@v2
+        with:
+          context: .
+          push: true
+          tags: |
+            ghcr.io/${{ github.repository_owner }}/lean:latest
+            ghcr.io/${{ github.repository_owner }}/lean:${{ github.ref_name }}
+          cache-from: type=gha
+          cache-to: type=gha,mode=max

.gitignore

@@ -0,0 +1,3 @@
+*.olean
+/_target
+/leanpkg.path

Dockerfile

@@ -0,0 +1,44 @@
+FROM ubuntu:18.04
+
+RUN set -ex; \
+    useradd --create-home -u 9999 codewarrior; \
+    mkdir -p /workspace; \
+    chown -R codewarrior:codewarrior /workspace;
+
+ENV LC_ALL=C.UTF-8 LANG=C.UTF-8
+RUN set -ex; \
+    apt-get update; \
+    apt-get install -y --no-install-recommends \
+        wget \
+        ca-certificates \
+        git \
+        python3-pip \
+        python3-setuptools \
+    ; \
+# Install `leanproject`
+    pip3 install mathlibtools; \
+    rm -rf /tmp/* /var/lib/apt/lists/*;
+
+USER codewarrior
+# Install Elan to manage Lean versions
+RUN set -ex; \
+    cd /tmp; \
+    wget -q https://github.com/Kha/elan/releases/download/v0.10.2/elan-x86_64-unknown-linux-gnu.tar.gz; \
+    tar xf elan-x86_64-unknown-linux-gnu.tar.gz; \
+    rm elan-x86_64-unknown-linux-gnu.tar.gz; \
+    ./elan-init -y --no-modify-path; \
+    rm elan-init;
+ENV PATH=/home/codewarrior/.elan/bin:$PATH
+
+WORKDIR /workspace
+COPY --chown=codewarrior:codewarrior leanpkg.toml /workspace/leanpkg.toml
+RUN set -ex; \
+    cd /workspace; \
+# `leanproject` command requires git repository
+    git init -q; \
+    mkdir src; \
+    mkdir test; \
+# Get mathlib olean files
+    leanproject get-mathlib-cache; \
+# Check timestamps are correct
+    leanproject check;

LICENSE

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

README.md

@@ -0,0 +1,26 @@
+# Lean
+
+Container image for Lean used by CodeRunner.
+
+## Usage
+
+```bash
+W=/workspace/
+# Create container
+C=$(docker container create --rm -w $W ghcr.io/codewars/lean:latest lean test/SolutionTest.lean)
+
+# Copy files from the current directory
+# src/Solution.lean
+# src/Preloaded.lean
+# test/SolutionTest.lean
+docker container cp ./. $C:$W
+
+# Run tests
+docker container start --attach $C
+```
+
+## Building
+
+```bash
+$ docker build -t ghcr.io/codewars/lean:latest .
+```

leanpkg.toml

@@ -0,0 +1,8 @@
+[package]
+name = "lean-challenge"
+version = "1.0"
+lean_version = "leanprover-community/lean:3.20.0"
+path = "src"
+
+[dependencies]
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "da66bb81bf0466335bae82077f0c335dfe53aeb3"}

src/Preloaded.lean

@@ -0,0 +1,11 @@
+-- Task 1: no axioms required
+def TASK_1 := ∀ n m : ℕ, n + m = n + m
+notation `TASK_1` := TASK_1
+
+-- Task 2: using `simp` introduces `propext`
+def TASK_2 := ∀ n m : ℕ, n + m = m + n
+notation `TASK_2` := TASK_2
+
+-- Task 3: requires all 3 core axioms
+def TASK_3 := ∀ p : Prop, p ∨ ¬p
+notation `TASK_3` := TASK_3

src/Solution.lean

@@ -0,0 +1,13 @@
+import Preloaded tactic
+open classical
+
+-- Task 1: Prove that n + m = n + m
+theorem immediate : ∀ n m : ℕ, n + m = n + m :=
+  by intros; refl
+
+-- Task 2: Prove that n + m = m + n
+theorem plus_comm : ∀ n m : ℕ, n + m = m + n :=
+  by intros; apply add_comm
+
+-- Task 3: Prove excluded middle
+theorem excluded_middle : ∀ p : Prop, p ∨ ¬p := em

test/SolutionTest.lean

@@ -0,0 +1,10 @@
+import Preloaded Solution
+
+theorem task_1 : TASK_1 := immediate
+#print axioms task_1
+
+theorem task_2 : TASK_2 := plus_comm
+#print axioms task_2
+
+theorem task_3 : TASK_3 := excluded_middle
+#print axioms task_3