Merge branch 'main' into AdvMultiplication

.devcontainer/Dockerfile

@@ -2,21 +2,27 @@ FROM node:20
 
 WORKDIR /
 
-ENV ELAN_HOME=/usr/local/elan \
-  PATH=/usr/local/elan/bin:$PATH \
-  LEAN_VERSION=leanprover/lean4:v4.1.0
-  # TODO: read toolchain from `lean-toolchain`
-
-SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]
-
-RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
-  chmod -R a+w $ELAN_HOME; \
-  elan --version; \
-  lean --version; \
-  leanc --version; \
-  lake --version;
+COPY ./lean-toolchain /lean-toolchain
 
 USER node
 
 WORKDIR /home/node
-RUN git clone https://github.com/leanprover-community/lean4game.git
+
+RUN export LEAN_VERSION="$(cat /lean-toolchain | grep -oE '[^:]+$')" && git clone --depth 1 --branch $LEAN_VERSION https://github.com/leanprover-community/lean4game.git
+
+WORKDIR /
+
+USER root
+
+ENV ELAN_HOME=/usr/local/elan \
+  PATH=/usr/local/elan/bin:$PATH
+
+SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]
+
+RUN export LEAN_VERSION="$(cat /lean-toolchain)" && \
+  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
+    chmod -R a+w $ELAN_HOME; \
+    elan --version; \
+    lean --version; \
+    leanc --version; \
+    lake --version;

.devcontainer/devcontainer.json

@@ -13,9 +13,11 @@
   "overrideCommand": true,
   "onCreateCommand": {
     "npm_install": "(cd ~/lean4game && npm install)",
-    "lake_build": "(cd ~/game && lake update && lake exe cache get && lake build)"
+    // BUG: Apparently `&& lake exe cache get` was needed here because the update hook was broken.
+    // should been fixed in https://github.com/leanprover-community/mathlib4/pull/8755
+    "lake_build": "(cd ~/game && lake update -R && lake exe cache get && lake build)"
   },
-  "postStartCommand": "cd ~/lean4game && export LEAN4GAME_SINGLE_GAME=true && npm start",
+  "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
   "customizations": {
     "vscode": {
       "settings": {

.devcontainer/docker-compose.yml

@@ -3,8 +3,8 @@ version: "3.9"
 services:
   game:
     build:
-      context: .
-      dockerfile: Dockerfile
+      context: ..
+      dockerfile: .devcontainer/Dockerfile
     volumes:
       - ..:/home/node/game
     ports:

.github/workflows/build.yml

@@ -9,15 +9,57 @@ jobs:
     runs-on: ubuntu-latest
     steps:
 
-      - uses: actions/checkout@v2
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: build docker image
-        run: docker build . --file Dockerfile --tag game:latest
+      - uses: actions/checkout@v4
 
-      - name: Store docker container as an artifact
-        uses: ishworkh/docker-image-artifact-upload@v1
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
+        # Note: this would also happen in the lake post-update-hook
+      - name: get mathlib cache
+        continue-on-error: true
+        run: |
+          lake exe cache clean
+          # We've been seeing many failures at this step recently because of network errors.
+          # As a band-aid, we try twice.
+          # The 'sleep 1' is small pause to let the network recover.
+          lake exe cache get || (sleep 1; lake exe cache get)
+
+      - name: create timestamp file
+        run: touch tmp_timestamp
+
+        # Note: this would also happen in the lake post-update-hook
+      - name: build gameserver executable
+        run: env LEAN_ABORT_ON_PANIC=1 lake build gameserver
+
+      - name: building game
+        run: env LEAN_ABORT_ON_PANIC=1 lake build
+
+      - name: delete unused mathlib cache
+        continue-on-error: true
+        run: find . -type d \( -name "*/.git" \) -delete -print && find ./.lake/ -type f \( -name "*.c" -o -name "*.hash" -o -name "*.trace" \) -delete -print && find ./.lake/ -type f \( -name "*.olean" \) \! -neweraa ./tmp_timestamp -delete -print
+
+      - name: delete timestamp file
+        run: rm ./tmp_timestamp
+
+      - name: compress built game
+        #run: tar -czvf ../game.tar.gz .
+        run: zip game.zip * .lake/ -r
+
+      - name: upload compressed game folder
+        uses: actions/upload-artifact@v3
         with:
-          image: "game:latest"
+          name: build-for-server-import
+          path: |
+            game.zip
 
       - name: What next?
         run: echo "To export the game to the Game Server, open https://adam.math.hhu.de/import/trigger/${GITHUB_REPOSITORY,,} \n Afterwards, you can play the game at https://adam.math.hhu.de/#/g/${GITHUB_REPOSITORY,,}"

.github/workflows/build_non_main.yml

@@ -10,7 +10,28 @@ jobs:
     runs-on: ubuntu-latest
     steps:
 
-      - uses: actions/checkout@v2
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: build docker image
-        run: docker build . --file Dockerfile --tag game:latest
+      - uses: actions/checkout@v4
+
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
+      - name: get mathlib cache
+        continue-on-error: true
+        run: |
+          lake exe cache clean
+          # We've been seeing many failures at this step recently because of network errors.
+          # As a band-aid, we try twice.
+          # The 'sleep 1' is small pause to let the network recover.
+          lake exe cache get || (sleep 1; lake exe cache get)
+
+      - name: building game
+        run: env LEAN_ABORT_ON_PANIC=1 lake build

.gitignore

@@ -1,4 +1,4 @@
 build/
 lake-packages/
-lakefile.olean
+.lake/
 **/.DS_Store

Game.lean

@@ -98,16 +98,16 @@ Alternatively, if you experience issues / bugs you can also open github issues:
 
 "
 
--- Here's where we show how to glue the worlds together
-Dependency Addition → Multiplication → Power
---Dependency Addition → AdvAddition → AdvMultiplication → Inequality → Prime → Hard
---Dependency Multiplication → AdvMultiplication
---Dependency AdvAddition → EvenOdd → Inequality → StrongInduction
-Dependency Addition → Implication → AdvAddition → LessOrEqual
-Dependency AdvAddition → Algorithm
--- The game automatically computes connections between worlds based on introduced
--- tactics and theorems, but for example it cannot detect introduced definitions
-
 -- Dependency Implication → Power -- `Power` uses `≠` which is introduced in `Implication`
 
+/-! Information to be displayed on the servers landing page. -/
+Languages "English"
+CaptionShort "The classical introduction game for Lean."
+CaptionLong "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,
+learning the basics about theorem proving in Lean.
+
+This is a good first introduction to Lean!"
+CoverImage "images/cover.png"
+
+/-! Build the game. Show's warnings if it found a problem with your game. -/
 MakeGame

Game/Doc/Definitions.lean

@@ -13,7 +13,7 @@ import GameServer.Commands
 -- This notation is for our own version of the natural numbers, called `MyNat`.
 -- The natural numbers implemented in Lean's core are called `Nat`.
 
--- If you end up getting someting of type `Nat` in this game, you probably
+-- If you end up getting something of type `Nat` in this game, you probably
 -- need to write `(4 : ℕ)` to force it to be of type `MyNat`.
 
 -- *Write with `\\N`.*

Game/Levels/Addition/L01zero_add.lean

@@ -45,7 +45,8 @@ Statement zero_add (n : ℕ) : 0 + n = n := by
     This first goal is the base case $n = 0$.
 
     Recall that you can rewrite the proof of any lemma which is visible
-    in your inventory, or of any assumption displayed above the goal."
+    in your inventory, or of any assumption displayed above the goal,
+    as long as it is of the form `X = Y`."
     Hint (hidden := true) "try rewriting `add_zero`."
     rw [add_zero]
     rfl

Game/Levels/Addition/L05add_right_comm.lean

@@ -45,4 +45,6 @@ You can begin the journey towards this boss by entering Multiplication World.
 Or you can go off the beaten track and learn some new tactics in Implication
 World. These tactics let you prove more facts about addition, such as
 how to deduce `a = 0` from `x + a = x`.
+
+Click \"Leave World\" and make your choice.
 "

Game/Levels/AdvAddition.lean

@@ -3,8 +3,8 @@ import Game.Levels.AdvAddition.L02add_right_cancel
 import Game.Levels.AdvAddition.L03add_left_cancel
 import Game.Levels.AdvAddition.L04add_left_eq_self
 import Game.Levels.AdvAddition.L05add_right_eq_self
-import Game.Levels.AdvAddition.L06eq_zero_of_add_right_eq_zero
-import Game.Levels.AdvAddition.L07eq_zero_of_add_left_eq_zero
+import Game.Levels.AdvAddition.L06add_right_eq_zero
+import Game.Levels.AdvAddition.L07add_left_eq_zero
 
 World "AdvAddition"
 Title "Advanced Addition World"

Game/Levels/AdvAddition/L06add_right_eq_zero.lean

@@ -0,0 +1,90 @@
+import Game.Levels.AdvAddition.L05add_right_eq_self
+import Game.Tactic.Cases
+
+World "AdvAddition"
+Level 6
+Title "add_right_eq_zero"
+
+LemmaTab "Peano"
+
+namespace MyNat
+
+Introduction
+"The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.
+Let's prove one of these facts in this level, and the other in the next.
+
+## A new tactic: `cases`
+
+The `cases` tactic will split an object or hypothesis up into the possible ways
+that it could have been created.
+
+For example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,
+but don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.
+In this situation you can use `cases b with d` instead. There are two ways to make
+a number: it's either zero or a successor. So you will end up with two goals, one
+with `b = 0` and one with `b = succ d`.
+
+Another example: if you have a hypothesis `h : False` then you are done, because a false statement implies
+any statement. Here `cases h` will close the goal, because there are *no* ways to
+make a proof of `False`! So you will end up with no goals, meaning you have proved everything.
+
+"
+
+TacticDoc cases "
+## Summary
+
+If `n` is a number, then `cases n with d` will break the goal into two goals,
+one with `n = 0` and the other with `n = succ d`.
+
+If `h` is a proof (for example a hypothesis), then `cases h with...` will break the
+proof up into the pieces used to prove it.
+
+## Example
+
+If `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,
+one with `n` replaced by 0 and the other with `n` replaced by `succ d`. This
+corresponds to the mathematical idea that every natural number is either `0`
+or a successor.
+
+## Example
+
+If `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal
+into two goals, one with a hypothesis `hp : P` and the other with a
+hypothesis `hq : Q`.
+
+## Example
+
+If `h : False` is a hypothesis, then `cases h` will turn one goal into no goals,
+because there are no ways to make a proof of `False`! And if you have no goals left,
+you have finished the level.
+
+## Example
+
+If `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`
+and a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is
+`∃ c, b = a + c`.
+"
+NewTactic cases
+
+LemmaDoc MyNat.add_right_eq_zero as "add_right_eq_zero" in "+" "
+  A proof that $a+b=0 \\implies a=0$.
+"
+
+-- **TODO** why `add_eq_zero_right` and not `add_right_eq_zero`?
+-- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/eq_zero_of_add_eq_zero_right/near/395716874
+
+/-- If $a+b=0$ then $a=0$. -/
+Statement add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
+  Hint "Here we want to deal with the cases `b = 0` and `b ≠ 0` separately,
+  so start with `cases b with d`."
+  cases b with d
+  intro h
+  rw [add_zero] at h
+  exact h
+  intro h
+  rw [add_succ] at h
+  symm at h
+  apply zero_ne_succ at h
+  cases h
+
+Conclusion "Well done!"