Merge pull request #1 from monadius/lean-3.39.1

Author: kazk

Dockerfile

@@ -17,14 +17,14 @@ RUN set -ex; \
         python3-wheel \
     ; \
 # Install `leanproject`
-    pip3 install -Iv mathlibtools==0.0.10; \
+    pip3 install -Iv mathlibtools==1.1.0; \
     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; \
+    wget -q https://github.com/leanprover/elan/releases/download/v1.3.1/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; \

README.md

@@ -13,7 +13,8 @@ C=$(docker container create --rm -w $W ghcr.io/codewars/lean:latest lean test/So
 # src/Solution.lean
 # src/Preloaded.lean
 # test/SolutionTest.lean
-docker container cp ./. $C:$W
+docker container cp src $C:$W
+docker container cp test $C:$W
 
 # Run tests
 docker container start --attach $C

bin/run

@@ -0,0 +1,14 @@
+W=/workspace/
+# Create container
+C=$(docker container create --rm -w $W ghcr.io/codewars/lean:latest lean test/SolutionTest.lean)
+# C=$(docker container create --rm -w $W cw_lean lean test/SolutionTest.lean)
+
+# Copy files from the current directory
+# src/Solution.lean
+# src/Preloaded.lean
+# test/SolutionTest.lean
+docker container cp src $C:$W
+docker container cp test $C:$W
+
+# Run tests
+docker container start --attach $C

leanpkg.toml

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

src/Solution.lean

@@ -1,5 +1,4 @@
 import Preloaded tactic
-open classical
 
 -- Task 1: Prove that n + m = n + m
 theorem immediate : ∀ n m : ℕ, n + m = n + m :=
@@ -10,4 +9,4 @@ 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
+theorem excluded_middle : ∀ p : Prop, p ∨ ¬p := classical.em