Initial commit

.devcontainer/Dockerfile

@@ -0,0 +1,28 @@
+FROM node:20
+
+WORKDIR /
+
+COPY ./lean-toolchain /lean-toolchain
+
+USER node
+
+WORKDIR /home/node
+
+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

@@ -0,0 +1,32 @@
+{
+  "dockerComposeFile": "./docker-compose.yml",
+  "service": "game",
+  "workspaceFolder": "/home/node/game",
+  "forwardPorts": [3000],
+  // These settings make sure that the created files (lake-packages etc.) are owned
+  // by the user and not `root`.
+  // see also https://containers.dev/implementors/json_reference/
+  // and https://code.visualstudio.com/remote/advancedcontainers/add-nonroot-user
+  "remoteUser": "node",
+  "updateRemoteUserUID": true,
+  // I don't know why I need this, but I did...
+  "overrideCommand": true,
+  "onCreateCommand": {
+    "npm_install": "(cd ~/lean4game && npm install) || echo \"ERROR: `cd ~/lean4game && npm install` failed\", try running it manually in your dev-container!",
+    "lake_build": "(cd ~/game && lake update -R && lake build) || echo \"ERROR: `cd ~/game && lake update -R && lake exe cache get && lake build` failed!, try running it manually in your dev-container!\""
+  },
+  "postStartCommand": "(cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start) || echo \"ERROR: Did not start game server! See if you have warnings above, then try to start it manually using `cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start`!\"",
+  "customizations": {
+    "vscode": {
+      "settings": {
+        "remote.autoForwardPorts": false
+      },
+      "extensions": [
+        "leanprover.lean4"
+      ]
+    },
+    "codespaces": {
+      "openFiles": ["Game.lean"]
+    }
+  }
+}

.devcontainer/docker-compose.yml

@@ -0,0 +1,11 @@
+version: "3.9"
+
+services:
+  game:
+    build:
+      context: ..
+      dockerfile: .devcontainer/Dockerfile
+    volumes:
+      - ..:/home/node/game
+    ports:
+      - "3000:3000"

.docker/gitpod/Dockerfile

@@ -0,0 +1,37 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+
+# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
+# so we just install everything in one go
+FROM ubuntu:22.04
+
+USER root
+
+RUN apt-get update && apt-get --assume-yes install sudo git curl git bash-completion python3 -y && apt-get clean
+
+RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
+    # passwordless sudo for users in the 'sudo' group
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.github/workflows/build.yml

@@ -0,0 +1,65 @@
+name: Build
+run-name: Build the game and save artifact
+on:
+  workflow_dispatch:
+  push:
+    branches: [ "main" ]
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+
+      - 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
+
+      - uses: actions/checkout@v4
+
+      - 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/ .i18n/ -r
+
+      - name: upload compressed game folder
+        uses: actions/upload-artifact@v3
+        with:
+          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

@@ -0,0 +1,37 @@
+name: Build non-main branch
+run-name: Build non-main branch
+on:
+  workflow_dispatch:
+  push:
+    branches-ignore:
+    - 'main'
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+
+      - 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
+
+      - 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

@@ -0,0 +1,5 @@
+build/
+lake-packages/
+.lake/
+**/.DS_Store
+.i18n/**/*.mo

.gitpod.yml

@@ -0,0 +1,12 @@
+image:
+  file: .docker/gitpod/Dockerfile
+
+vscode:
+  extensions:
+    - leanprover.lean4
+
+tasks:
+  - init: |
+      lake exe cache get
+  - command: |
+      sudo apt-get --assume-yes install gcc

.i18n/config.json

@@ -0,0 +1,4 @@
+{
+  "sourceLang": "en",
+  "translationContactEmail": ""
+}

.i18n/de/Game.json

@@ -0,0 +1,23 @@
+{"level completed! 🎉": "Level gelöst! 🎉",
+ "level completed with warnings… 🎭": "Level mit Warnungen beendet… 🎭",
+ "intermediate goal solved! 🎉": "Zwischenziel gelöst! 🎉",
+ "You should use this game as a template for your own game and add your own levels.":
+ "Dieses Spiel sollte als Grundgerüst für eigene Spiele verwendet und eigene Levels hinzugefügt werden.",
+ "You should use `«{h}»` now.": "Jetzt sollte `«{h}»` verwendet werden.",
+ "You should use `«{g}»` now.": "Jetzt sollte `«{g}»` verwendet werden.",
+ "You can either start using `«{h}»` or `«{g}»`.":
+ "Anfangen kann man mit der Benützung von `«{h}»` oder `«{g}»`.",
+ "This text is shown as first message when the level is played.\nYou can insert hints in the proof below. They will appear in this side panel\ndepending on the proof a user provides.":
+ "Dieser Text erscheint als erste Nachricht beim Spielen des Levels.\n\"Hints\" können in den folgenden Beweis eingefügt werden. Diese erscheinen hier in diesem Side-Panel,\nabhängig von dem Beweisstand des Spielers.",
+ "This text appears on the starting page where one selects the world/level to play.\nYou can use markdown.":
+ "Dieser Text erscheint auf der Startseite, wo man Welten/Levels zum spielen auswählt.\nMan kann Markdown verwenden.",
+ "This last message appears if the level is solved.":
+ "Diese letzte Nachricht erscheint beim erfolgreichen lösen eines Levels.",
+ "This introduction is shown before one enters level 1 of the demo world. Use markdown.":
+ "Diese Einführung wird gezeigt, bevor man Level 1 der Beispielwelt öffnet. Man kann Markdown verwenden.",
+ "Here you can put additional information about the game. It is accessible\nfrom the starting through the drop-down menu.\n\nFor example: Game version, Credits, Link to Github and Zulip, etc.\n\nUse markdown.":
+ "Hier können zusätzliche Inforamtionen über das Spiel hingeschrieben werden. Man erreicht diese\nvon der Startseite via Dropdown-Menü.\n\nZum Beispiel: Spielversion, Credits, Link auf Github und Zulip, etc.\n\nMan kann Markdown verwenden.",
+ "Hello World Game": "Hallo-Welt-Spiel",
+ "Hello World": "Hallo Welt",
+ "Game Template": "Spiel-Grundgerüst",
+ "Demo World": "Beispielwelt"}

.i18n/de/Game.po

@@ -0,0 +1,114 @@
+msgid ""
+msgstr ""
+"Project-Id-Version: Game v4.7.0\n"
+"Report-Msgid-Bugs-To: \n"
+"POT-Creation-Date: Wed Apr 10 15:31:40 2024\n"
+"PO-Revision-Date: \n"
+"Last-Translator: \n"
+"Language-Team: none\n"
+"Language: de\n"
+"MIME-Version: 1.0\n"
+"Content-Type: text/plain; charset=UTF-8\n"
+"Content-Transfer-Encoding: 8bit\n"
+"Plural-Forms: nplurals=2; plural=(n != 1);\n"
+"X-Generator: Poedit 3.0.1\n"
+
+#: GameServer.RpcHandlers
+msgid "level completed! 🎉"
+msgstr "Level gelöst! 🎉"
+
+#: GameServer.RpcHandlers
+msgid "level completed with warnings… 🎭"
+msgstr "Level mit Warnungen beendet… 🎭"
+
+#: GameServer.RpcHandlers
+msgid "intermediate goal solved! 🎉"
+msgstr "Zwischenziel gelöst! 🎉"
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "Hello World"
+msgstr "Hallo Welt"
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid ""
+"This text is shown as first message when the level is played.\n"
+"You can insert hints in the proof below. They will appear in this side "
+"panel\n"
+"depending on the proof a user provides."
+msgstr ""
+"Dieser Text erscheint als erste Nachricht beim Spielen des Levels.\n"
+"\"Hints\" können in den folgenden Beweis eingefügt werden. Diese erscheinen "
+"hier in diesem Side-Panel,\n"
+"abhängig von dem Beweisstand des Spielers."
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "You can either start using `«{h}»` or `«{g}»`."
+msgstr "Anfangen kann man mit der Benützung von `«{h}»` oder `«{g}»`."
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "You should use `«{h}»` now."
+msgstr "Jetzt sollte `«{h}»` verwendet werden."
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "You should use `«{g}»` now."
+msgstr "Jetzt sollte `«{g}»` verwendet werden."
+
+#: Game.Levels.DemoWorld.L01_HelloWorld
+msgid "This last message appears if the level is solved."
+msgstr ""
+"Diese letzte Nachricht erscheint beim erfolgreichen lösen eines Levels."
+
+#: Game.Levels.DemoWorld
+msgid "Demo World"
+msgstr "Beispielwelt"
+
+#: Game.Levels.DemoWorld
+msgid ""
+"This introduction is shown before one enters level 1 of the demo world. Use "
+"markdown."
+msgstr ""
+"Diese Einführung wird gezeigt, bevor man Level 1 der Beispielwelt öffnet. "
+"Man kann Markdown verwenden."
+
+#: Game
+msgid "Hello World Game"
+msgstr "Hallo-Welt-Spiel"
+
+#: Game
+msgid ""
+"This text appears on the starting page where one selects the world/level to "
+"play.\n"
+"You can use markdown."
+msgstr ""
+"Dieser Text erscheint auf der Startseite, wo man Welten/Levels zum spielen "
+"auswählt.\n"
+"Man kann Markdown verwenden."
+
+#: Game
+msgid ""
+"Here you can put additional information about the game. It is accessible\n"
+"from the starting through the drop-down menu.\n"
+"\n"
+"For example: Game version, Credits, Link to Github and Zulip, etc.\n"
+"\n"
+"Use markdown."
+msgstr ""
+"Hier können zusätzliche Inforamtionen über das Spiel hingeschrieben werden. "
+"Man erreicht diese\n"
+"von der Startseite via Dropdown-Menü.\n"
+"\n"
+"Zum Beispiel: Spielversion, Credits, Link auf Github und Zulip, etc.\n"
+"\n"
+"Man kann Markdown verwenden."
+
+#: Game
+msgid "Game Template"
+msgstr "Spiel-Grundgerüst"
+
+#: Game
+msgid ""
+"You should use this game as a template for your own game and add your own "
+"levels."
+msgstr ""
+"Dieses Spiel sollte als Grundgerüst für eigene Spiele verwendet und eigene "
+"Levels hinzugefügt werden."