added fork info to readme

feat: add game `Knights and Knaves` by JadAbouHawili

.dockerignore

@@ -0,0 +1,8 @@
+node_modules
+client/dist
+games/
+server/.lake
+**/.DS_Store
+logs/
+relay/prev_cpu_metric
+test.ecosystem.config.cjs

.gitignore

@@ -4,3 +4,5 @@ games/
 server/.lake
 **/.DS_Store
 logs/
+relay/prev_cpu_metric
+test.ecosystem.config.cjs

Dockerfile

@@ -0,0 +1,29 @@
+FROM node:23-bookworm
+
+RUN apt update && apt upgrade -y
+RUN apt install -y bubblewrap
+
+WORKDIR /app
+
+# Install elan
+RUN 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
+
+ENV PATH="/root/.elan/bin:${PATH}"
+
+# Copy package files
+COPY package.json package-lock.json ./
+
+# Install dependencies
+RUN npm install
+
+# Copy project files
+COPY . .
+
+# Build the project
+RUN npm run build
+
+EXPOSE 8080
+
+# Set the entrypoint
+CMD ["npm", "run", "production"]

README.md

@@ -1,3 +1,35 @@
+# lean4game fork
+
+Questo è un fork di **lean4game** con supporto per essere self-hostato con Docker.
+
+## Deployment con Docker Compose
+
+Dopo aver clonato questa repo, per prima cosa serve creare [un token di API per GitHub](https://github.com/settings/developers) per permettere a lean4game di importare da solo i vari "game". Possiamo mettere questo token ed il nostro nome utente in un file `.env` come segue
+
+```
+export LEAN4GAME_GITHUB_USER='...'
+export LEAN4GAME_GITHUB_TOKEN='...'
+```
+
+poi per lanciare tutto con docker compose basta eseguire
+
+```bash
+$ source .env
+$ docker compose up -d
+```
+
+Questo comando lancierà lean4game su `http://locahost:8080`.
+
+### Aggiungere Giochi
+
+Per scaricare nuovi giochi basta fare una chiamata al seguente url
+
+- `https://{host}/import/trigger/{org}/{repo}` 
+
+Ad esempio per scaricare <https://github.com/leanprover-community/nng4> basta andare all'indirizzo `https://{host}/import/trigger/leanprover-community/nng4` per aggiungere _Natural Number Game_.
+
+---
+
 # Lean 4 Game
 
 This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).

client/public/locales/de/translation.json

@@ -1,22 +1,22 @@
 {
   "Tactics": "Taktiken",
-  "Lean Game Server": "Lean-Spielserver",
+  "Lean Game Server": "Lean-Lern-Spiel-Server",
   "<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Die Spielregeln bestimmen ob es erlaubt ist, Levels zu überspringen und ob das Spiel überprüft welche Taktiken und Theoreme freigeschaltet sind und nur diese im Beweis akzeptiert.</p><1>Bemerkung: \"Freigeschaltete\" Taktiken (und Theoreme) werden durch zwei Faktoren bestimmt: The Menge der Taktiken die minimal notwending sind um den Level zu lösen und dazu die Menge aller Taktiken, die in einem anderen Level freigeschaltet wurden. Das bedeutet wenn <1>simp</1> in einem Level freigeschaltet wird, kann diese Taktik danach in jeglichen Levels verwendet werden.",
   "Game Rules": "Spielregeln",
-  "levels": "Levels",
+  "levels": "Level",
   "tactics": "Taktiken",
   "regular": "regulär",
   "relaxed": "relaxed",
   "none": "keine",
   "Rules": "Regeln",
-  "Intro": "Inführung",
+  "Intro": "Prolog",
-  "Game Introduction": "Spieleinführung",
+  "Game Introduction": "Prolog",
-  "World selection": "Weltenauswahl",
+  "World selection": "Übersicht",
   "Start": "Start",
   "Inventory": "Inventar",
   "next level": "nächstes Level",
   "Next": "Weiter",
-  "back to world selection": "Zurück zur Weltenauswahl",
+  "back to world selection": "Zurück zur Übersicht",
   "Leave World": "Welt verlassen",
   "previous level": "voheriges Level",
   "Previous": "Zurück",
@@ -31,64 +31,69 @@
   "Erase": "Löschen",
   "Download Progress": "Spielstand herunterladen",
   "Download": "Herunterladen",
-  "Load Progress from JSON": "Spielstand von JSON laden",
+  "Load Progress from JSON": "Spielstand aus JSON laden",
   "Upload": "Laden",
   "Home": "Home",
   "back to games selection": "Zurück zur Spielauswahl",
-  "close inventory": "Inventar schliessen",
+  "close inventory": "Inventar schließen",
   "show inventory": "Inventar öffnen",
   "World": "Welt",
   "Show more help!": "Mehr Hilfe",
-  "Goal": "Goal",
+  "Goal": "Beweisziel",
-  "Current Goal": "Aktuelles Goal",
+  "Current Goal": "Aktuelles Beweisziel",
   "Objects": "Objekte",
   "Assumptions": "Annahmen",
-  "Further Goals": "Weitere Goals",
+  "Further Goals": "Weitere Ziele",
-  "No Goals": "Keine Goals",
+  "No Goals": "Keine Beweisziele",
-  "Loading goal…": "Goal wird geladen…",
+  "Loading goal…": "Beweisziel wird geladen…",
   "Click somewhere in the Lean file to enable the infoview.": "Ein Klick in den Lean-Code aktiviert den Infoview.",
-  "Waiting for Lean server to start…": "Warte auf das Starten des Lean-Servers…",
+  "Waiting for Lean server to start…": "Warte auf den Lean-Server …",
   "Level completed! 🎉": "Level gelöst! 🎉",
   "Level completed with warnings 🎭": "Level mit Warnungen abgeschlossen 🎭",
-  "Active Goal": "Aktuelles Goal",
+  "Active Goal": "Aktuelles Ziel",
-  "Crashed! Go to editor mode and fix your proof! Last server response:": "",
+  "Crashed! Go to editor mode and fix your proof! Last server response:": "Abgestürzt! Wechsle in den Editor-Modus, um deinen Beweis zu repariaeren.  Letzte Meldung vom Server:",
   "Line": "Zeile",
   "Character": "Charakter",
-  "Loading messages…": "",
+  "Loading messages…": "Lade Meldungen …",
   "Execute": "Ausführen",
   "Definitions": "Definitionen",
   "Theorems": "Theoreme",
   "Not unlocked yet": "Noch nicht verfügbar",
   "Not available in this level": "In diesem Level nicht verfügbar",
   "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean</1> <i>(Lean 4)</i> und dessen mathematische Bibliothek <5>mathlib</5>",
-  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen. öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt von einem lokalen Ordner zu laden.",
+  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen.  Öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt aus einem lokalen Ordner zu laden.",
-  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
-  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
   "Prerequisites": "Voraussetzungen",
   "Worlds": "Welten",
-  "Levels": "Levels",
+  "Levels": "Level",
-  "Language": "Sprachen",
+  "Language": "Sprache",
-  "Development notes": "Entwicklungshinweis",
+  "Development notes": "Entwicklungsstand",
   "Adding new games": "Neue Spiele hinzufügen",
   "Funding": "Finanzierung",
   "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>Soll der Spielstand unwiderruflich gelöscht werden?</p><p>(Dies löscht sämtliche Beweise und das gesammelte Inventar. Spielstände anderer Spiele werden nicht gelöscht.)</p>",
   "Delete Progress?": "Spielstand löschen?",
   "Delete": "Löschen",
-  "Download & Delete": "Herunterladen & Löschen",
+  "Download & Delete": "Herunterladen & löschen",
   "Cancel": "Abbrechen",
   "Layout": "Seitenlayout",
   "Always visible": "Immer sichtbar",
   "Save my settings (in the browser store)": "Einstellungen im Browser speichern.",
-  "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Wähle eine JSON-Datei mit dem Spielstand um diesen zu laden.</p><1><0>Achtung:</0> Diese Aktion überschreibt den aktuellen Spielstand! Es wird empfohlen zuerst den <2>aktuellen Spielstand herunterzuladen</2>!</1>",
+    "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Wähle eine JSON-Datei mit einem Spielstand, um diesen zu laden.</p><1><0>Achtung:</0> Deraktuelle Spielstand wird dabei überschrieben! Wenn du noch einmal zum aktuellen Spielstand zurückkehren möchtest, solltest du zunächst den <2>aktuellen Spielstand herunterladen</2>!</1>",
   "Upload Saved Progress": "Spielstand hochladen",
   "Load selected file": "Ausgewählte Datei hochladen",
   "Mobile": "Mobil",
   "Auto": "Auto",
   "Desktop": "Desktop",
-  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
+    "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>Für alle, die selbst Spiel entwickeln möchten, gibt es ein <1>GameSkeleton Github Repo</1> als Vorlage und die Anleitung <3>How to Create a Game</3>.</0><1>Die <1>Anleitung</1> erklärt auch, wie ein solches Spiel mittels einer passenden URL auf den Sever geladen und gespiel werden kann. Fragen dazu beantworten wir gern.</1><p>Als Kacheln sichtbar ist auf dieser Seite nur eine kuratierte Auswahl an existierenden Spielen. Wir erweitern diese Auswahl auf Anfrage sehr gerne.</p>",
-  "Level": "",
+  "Level": "Level",
-  "Introduction": "",
+  "Introduction": "Prolog",
-  "Retry proof from here": "",
+  "Retry proof from here": "Ab hier neu ansetzen",
-  "Retry": "",
+  "Retry": "Noch einmal",
-  "Failed command": ""
+  "Failed command": "Gescheiterter Befehl",
+    "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "Diese Server läuft auf universitäter Infrastruktur mit begrenzten Kapazitäten.  Wir schätzen, dass die Belastungsgrenze bei rund 70 gleichzeitig laufenden Spielen besteht.",
+    "<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "Der Spieleserver und die alle Spiele befinden sich in fortlaufender Entwicklung.  Wir bitten darum, Fehler und Ungereimtheiten als <1>GitHub Issue</1> zu melden.",
+    "This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "Die Lean-Spiele-Software und dieser Spiele-Server werden als Teils der Projekts <1>ADAM: Anticipating the Digital Age of Mathematics</1> an der Heinrich-Heine-Universität Düsseldorf entwickelt.",
+  "Server capacity": "Server-Auslastung",
+  "RAM": "RAM",
+  " used": "",
+  "CPU": "CPU"
 }

client/public/locales/en/translation.json

@@ -62,12 +62,13 @@
   "Not available in this level": "Not available in this level",
   "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>",
   "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.",
-  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>",
-  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.",
   "Prerequisites": "Prerequisites",
   "Worlds": "Worlds",
   "Levels": "Levels",
   "Language": "Language",
+  "Server capacity": "Server capacity",
+  "RAM": "RAM",
+  "CPU": "CPU",
   "Development notes": "Development notes",
   "Adding new games": "Adding new games",
   "Funding": "Funding",
@@ -90,5 +91,9 @@
   "Introduction": "Introduction",
   "Retry proof from here": "Retry proof from here",
   "Retry": "Retry",
-  "Failed command": "Failed command"
+  "Failed command": "Failed command",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>",
+  "<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>",
+  "This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.",
+  " used": " used"
 }

client/public/locales/es/translation.json

@@ -1,4 +1,4 @@
- {
+{
   "Intro": "Introducción",
   "Game Introduction": "Introducción del juego",
   "World selection": "Seleccionar mundo",
@@ -56,9 +56,7 @@
   "Not available in this level": "No disponible en este nivel",
   "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Un repositorio de juegos para aprender el asistente de demostración <1>Lean</1>, <i>(Lean 4)</i> y su biblioteca matemática <5>mathlib</5> ",
   "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No se ha cargado ningún juego. Use <1>http://localhost:3000/#/g/local/FOLDER</1> para abrir un juego directamente desde una carpeta local",
-  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "<p>Como este servidor corre en máquinas de nuestra universidad, tiene una capacidad limitada. Nuestra estimación actual es de unos 70 juegos simultaneos. Esperamos afrontar y comprobar mejor esta limitación en el futuro.</p>. <1>Muchos aspectos de los juegos y la infrastructura están aún en desarrollo. No dude en abrir una <1>GitHub Issue</1> sobre cualquier problema que experimente.</1>",
   "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>Si está considerando escribir su propio juego, use el <1>GameSkeleton Github Repo</1> como plantilla y lea <3>How to Create a Game</3>.</0><1>Puede cargar directamente los juegos en el servidor y jugarlo usando la URL adecuada. Las <1>instrucciones anteriores</1> también explican los detalles sobre cómo cargar su juego en el servidor. Le animamos a ponerse en contacto con nosotros si tiene preguntas.</1><p>Los juegos incluidos en esta página son añadidos manualmente. Por favor, contactenos y añadiremos el suyo encantados.</p>",
-  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "Este  servidor se ha desarrollado como parte del proyecto <1>ADAM : Anticipating the Digital Age of Mathematics</1> en la Heinrich-Heine-Universität de Düsseldorf.",
   "Prerequisites": "Requisitos previos",
   "Worlds": "Mundos",
   "Levels": "Niveles",
@@ -69,7 +67,7 @@
   "Funding": "Financiación",
   "Level": "Nivel",
   "Introduction": "Introducción",
-  "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>" : "<p>¿Desea eliminar su progreso guardado definitivamente?</p><p>(Esto elimina sus pruebas y su inventario recopilado. Los progresos guardados de otros juegos no se eliminan.)</p>",
+  "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>¿Desea eliminar su progreso guardado definitivamente?</p><p>(Esto elimina sus pruebas y su inventario recopilado. Los progresos guardados de otros juegos no se eliminan.)</p>",
   "Delete Progress?": "¿Borrar Progreso?",
   "Delete": "Borrar",
   "Download & Delete": "Descargar y Borrar",
@@ -90,5 +88,12 @@
   "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Seleccione un archivo JSON con el progreso del juego guardado para cargar su progreso.</p><1><0>Advertencia:</0> Esto borrará su progreso actual en el juego. Considere <2>descargar su progreso actual</2> antes</1>",
   "Upload Saved Progress": "Subir progreso guardado",
   "Load selected file": "Cargar archivo seleccionado",
-  "Rules": "Reglas"
+  "Rules": "Reglas",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "<p>Como este servidor corre en máquinas de nuestra universidad, tiene una capacidad limitada. Nuestra estimación actual es de unos 70 juegos simultaneos.</p>.",
+  "<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "<1>Muchos aspectos de los juegos y la infrastructura están aún en desarrollo. No dude en abrir una <1>GitHub Issue</1> sobre cualquier problema que experimente.</1>",
+  "This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "Este  servidor se ha desarrollado como parte del proyecto <1>ADAM: Anticipating the Digital Age of Mathematics</1> en la Heinrich-Heine-Universität de Düsseldorf.",
+  "Server capacity": "",
+  "RAM": "",
+  " used": "",
+  "CPU": ""
 }

client/public/locales/ko/.gitignore

@@ -0,0 +1,8 @@
+/ko-level1.tmx
+/ko-level2.tmx
+/ko-omegat.tmx
+/**/*.bak
+/omegat/last_entry.properties
+/omegat/files_order.txt
+/omegat/project_stats.txt
+/tm/*.tmx

client/public/locales/ko/README.ko.md

@@ -0,0 +1,15 @@
+# 린 4 게임
+
+[English (영어)](./README.md) | 한국어
+
+## 기여하기
+
+`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
+
+### 한국어 번역
+
+저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
+
+[bc]: https://github.com/chabulhwi
+[omt]: https://omegat.org/
+[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT

client/public/locales/ko/README.md

@@ -0,0 +1,18 @@
+# Lean 4 Game
+
+English | [한국어[Korean]](./README.ko.md)
+
+## Contributing
+
+Contributions to the Korean translation of `lean4game` are always welcome!
+
+### Korean Translation
+
+I ([Bulhwi Cha][bc]) use [OmegaT][omt] to translate English documentation into
+Korean. The OmegaT project is in this directory, that is,
+`client/public/locales/ko`. You need to install the [Okapi filters plugin for
+OmegaT][okapi] to make OmegaT parse JSON files.
+
+[bc]: https://github.com/chabulhwi
+[omt]: https://omegat.org/
+[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT

client/public/locales/ko/glossary/glossary.txt

@@ -0,0 +1,167 @@
+# Glossary in tab-separated format -*- coding: utf-8 -*-
+St. Anselm	안셀무스
+ontological	존재론적
+argument	논증
+argument	인수
+Lean	린
+Lean community	린 커뮤니티
+God	신
+Alvin Plantinga	앨빈 플랜팅아
+exist	존재하다
+existence	존재
+the understanding	지성
+reality	현실
+assumption	가정
+reductio	귀류법
+great	큰
+premise	전제
+being	존재자
+conceive	생각하다
+definition	정의
+true	참
+true	참인
+false	거짓
+false	거짓인
+formulate	정식화하다
+formulation	정식화
+formalize	형식화하다
+formalization	형식화
+property	속성
+redundant	불필요한
+sentence	문장
+state	진술하다
+statement	진술
+proposition	명제
+negation	부정
+axiom	공리
+theorem	정리
+theory	이론
+conclude	결론하다
+prove	증명하다
+SEP	스탠퍼드 철학 백과사전
+Eric Wieser	에릭 비저
+Alistair Tucker	앨리스터 터커
+philosophy	철학
+Owl of Sogang	서강올빼미
+type theory	유형론
+universe level	유형 세계 변수
+type	유형
+type	입력하다
+type check	유형을 확인하다
+type check	유형이 확인되다
+type check	유형 확인이 잘되다
+type class	유형 클래스
+instance	사례
+category mistake	범주 실수
+class	클래스
+example	보기
+example	예
+inductive type	귀납형
+define	정의하다
+constructor	구성자
+Apache License, Version 2.0	아파치 라이선스, 버전 2.0
+under the terms of	의 조건에 따라
+OmegaT	오메가T
+symbolic link	심벌릭 링크
+directory	디렉터리
+root directory	최상위 디렉터리
+documentation	문서
+English	영어
+Korean	한국어
+chapter	장
+quiz	퀴즈
+question	문제
+command	명령어
+error	오류
+code	코드
+evaluate	계산하다
+keyword	핵심어
+declare	선언하다
+constant	상수
+reference	참고 문헌
+universe-polymorphic	세계 다형적
+parametrically polymorphic	매개 변수 다형적
+function	함수
+identifier	식별자
+definitionally equal	정의상 같은
+natural number	자연수
+input	입력값
+return	반환하다
+non-zero	영이 아닌
+zero	영
+alpha-equivalent	알파 동등한
+less-than-or-equal-to sign	작거나 같음 부호
+dependent function	의존 함수
+dependent function type	의존 함수형
+dependent product	의존곱
+dependent product type	의존곱형
+underscore	밑줄
+implicit	암시적
+explicit	명시적
+sigma type	시그마
+propositional logic	명제 논리
+term	항
+contemporary	동시대
+term	용어
+truth-value	진릿값
+bearer	담지자
+propositional attitudes	명제적 태도
+believe	믿다
+doubt	의심하다
+South Korea	한국
+school mathematics	학교 수학
+sentence	문장
+high school mathematics	고등학교 수학
+teacher	교사
+Stanford Encyclopedia of Philosophy	스탠퍼드 철학 백과사전
+ordered triple	순서세짝
+conjecture	추측
+Goldbach's conjecture	골드바흐의 추측
+interactive theorem prover	상호 작용 정리 증명기
+truth	참
+falsity	거짓
+rule of inference	추론 규칙
+introduction rule	도입 규칙
+elimination rule	제거 규칙
+ex falso quodlibet	엑스 팔소 세퀴투르 쿠오들리베트
+principle of explosion	폭발 원리
+propositional connective	명제 연결사
+symbol	기호
+refutation by contradiction	모순에 따른 부인
+contradiction	모순
+conjunction	연언
+disjunction	선언(選言)
+implication	함의
+material implication	내용적 함의
+conditional	조건문
+modus ponens	긍정 논법[모더스 포넨스]
+necessary condition	필요조건
+conversion	역
+inversion	이(裏)
+contraposition	대우(對偶)
+equivalence	동등
+biconditional	쌍조건문
+abbreviation	준말
+if and only if	…일 때 그리고 그럴 때만
+editor	편집기
+shortcut	단축키
+Theorem Proving in Lean 4	린 4로 하는 정리 증명
+exercise	연습 문제
+repository	저장소
+Jeremy Avigad	제러미 아비가드
+Leonardo de Moura	레오나르두 지 모라
+Soonho Kong	공순호
+Sebastian Ullrich	제바스티안 울리히
+file	파일
+Markdown	마크다운
+quiz	퀴즈
+translation	번역
+contribute	기여하다
+progress	진도
+capacity	이용량
+GitHub	깃허브
+repo	저장소
+game rule	게임 규칙
+unlocked	잠금 해제가 된
+unlock	잠금 해제를 하다
+Markdown	마크다운

client/public/locales/ko/omegat.project

@@ -0,0 +1,33 @@
+<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
+<omegat>
+    <project version="1.0">
+        <source_dir>__DEFAULT__</source_dir>
+        <source_dir_excludes>
+            <mask>**/.svn/**</mask>
+            <mask>**/CVS/**</mask>
+            <mask>**/.cvs/**</mask>
+            <mask>**/.git/**</mask>
+            <mask>**/.hg/**</mask>
+            <mask>**/.repositories/**</mask>
+            <mask>**/desktop.ini</mask>
+            <mask>**/Thumbs.db</mask>
+            <mask>**/.DS_Store</mask>
+            <mask>**/~$*</mask>
+        </source_dir_excludes>
+        <target_dir>__DEFAULT__</target_dir>
+        <tm_dir>__DEFAULT__</tm_dir>
+        <glossary_dir>__DEFAULT__</glossary_dir>
+        <glossary_file>__DEFAULT__</glossary_file>
+        <dictionary_dir>__DEFAULT__</dictionary_dir>
+        <export_tm_dir>__DEFAULT__</export_tm_dir>
+        <export_tm_levels>omegat level1 level2</export_tm_levels>
+        <source_lang>en</source_lang>
+        <target_lang>ko</target_lang>
+        <source_tok>org.omegat.tokenizer.LuceneEnglishTokenizer</source_tok>
+        <target_tok>org.omegat.tokenizer.HunspellTokenizer</target_tok>
+        <sentence_seg>true</sentence_seg>
+        <support_default_translations>true</support_default_translations>
+        <remove_tags>false</remove_tags>
+        <external_command></external_command>
+    </project>
+</omegat>

client/public/locales/ko/source/README.md

@@ -0,0 +1 @@
+../README.md

client/public/locales/ko/source/translation.json

@@ -0,0 +1 @@
+../../en/translation.json

client/public/locales/ko/target/README.md

@@ -0,0 +1,15 @@
+# 린 4 게임
+
+[English (영어)](./README.md) | 한국어
+
+## 기여하기
+
+`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
+
+### 한국어 번역
+
+저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
+
+[bc]: https://github.com/chabulhwi
+[omt]: https://omegat.org/
+[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT

client/public/locales/ko/target/translation.json

@@ -0,0 +1,99 @@
+{
+  "Tactics": "전략",
+  "Lean Game Server": "린 게임 서버",
+  "<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>게임 규칙에 따라, 단계들을 건너뛰어도 되는지 그리고 증명을 작성할 때 잠금 해제가 된 전략과 정리만 이용할 수 있는지가 정해집니다.</p><1>\n\n참고: '잠금 해제'가 된 전략이나 정리는 다음 두 부류로 정해집니다. (1) 해당 단계를 푸는 데 필요한 최소한의 전략이나 정리의 모임, (2) 다른 단계에서 잠금 해제를 한 전략이나 정리. 따라서 여러분이 <1>simp</1> 전략을 잠금 해제 하면, 그 뒤로 어느 단계에서든 이 전략을 이용할 수 있습니다.</1><p>선택할 수 있는 게임 규칙은 다음과 같습니다.</p>",
+  "Game Rules": "게임 규칙",
+  "levels": "단계",
+  "tactics": "전략",
+  "regular": "일반",
+  "relaxed": "완화됨",
+  "none": "없음",
+  "Rules": "규칙",
+  "Intro": "소개",
+  "Game Introduction": "게임 소개",
+  "World selection": "세계 선택",
+  "Start": "시작하기",
+  "Inventory": "인벤토리",
+  "next level": "다음 단계",
+  "Next": "다음",
+  "back to world selection": "세계 선택하러 돌아가기",
+  "Leave World": "세계에서 나가기",
+  "previous level": "이전 단계",
+  "Previous": "이전",
+  "Editor mode is enforced!": "편집기 모드가 강제됐습니다!",
+  "Editor mode": "편집기 모드",
+  "Typewriter mode": "타자기 모드",
+  "information, Impressum, privacy policy": "정보, 관리자 정보, 사생활 정책",
+  "Preferences": "기본 설정",
+  "Game Info & Credits": "게임 정보 및 제작자 명단",
+  "Game Info": "게임 정보",
+  "Clear Progress": "진도 없애기",
+  "Erase": "지우기",
+  "Download Progress": "진도 내려받기",
+  "Download": "내려받기",
+  "Load Progress from JSON": "JSON에서 진도 불러오기",
+  "Upload": "업로드",
+  "Home": "홈",
+  "back to games selection": "게임 선택하러 돌아가기",
+  "close inventory": "인벤토리 닫기",
+  "show inventory": "인벤토리 보기",
+  "World": "세계",
+  "Show more help!": "도움말 더 보기!",
+  "Goal": "목표",
+  "Current Goal": "현재 목표",
+  "Objects": "객체",
+  "Assumptions": "가정",
+  "Further Goals": "이후 목표",
+  "No Goals": "목표 없음",
+  "Loading goal…": "목표 불러오는 중…",
+  "Click somewhere in the Lean file to enable the infoview.": "린 파일의 아무 곳이나 눌러 정보창을 여십시오.",
+  "Waiting for Lean server to start…": "린 서버가 시작하기를 기다리는 중…",
+  "Level completed! 🎉": "단계 완료! 🎉",
+  "Level completed with warnings 🎭": "경고 있는 채로 단계 완료 🎭",
+  "Active Goal": "활성화된 목표",
+  "Crashed! Go to editor mode and fix your proof! Last server response:": "시스템 다운됨! 편집기 모드에서 증명을 고치십시오! 마지막 서버 응답:",
+  "Line": "줄",
+  "Character": "문자",
+  "Loading messages…": "메시지 불러오는 중…",
+  "Execute": "실행하기",
+  "Definitions": "정의",
+  "Theorems": "정리",
+  "Not unlocked yet": "아직 잠금 해제가 안 됨",
+  "Not available in this level": "이 단계에서 쓸 수 없음",
+  "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "<1>린(Lean 4)</1> 증명 보조기와 그 수학 라이브러리 <5>매스리브(mathlib)</5>를 학습하기 위한 게임들의 저장소",
+  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "불러온 게임 없음. <1>http://localhost:3000/#/g/local/FOLDER</1>를 이용해 지역[로컬] 폴더에서 게임을 직접 여십시오.",
+  "Prerequisites": "선행 요건",
+  "Worlds": "세계",
+  "Levels": "단계",
+  "Language": "언어",
+  "Server capacity": "서버 이용량",
+  "RAM": "램",
+  "CPU": "CPU",
+  "Development notes": "개발 노트",
+  "Adding new games": "새 게임 추가하기",
+  "Funding": "재정 지원",
+  "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>저장된 진도를 불가역적으로 삭제하시겠습니까?</p><p>(이를 선택하시면 증명과 인벤토리 안의 수집 항목들이 삭제됩니다. 다른 게임에 저장된 정보는 삭제되지 않습니다.)</p>",
+  "Delete Progress?": "진도를 삭제하시겠습니까?",
+  "Delete": "삭제하기",
+  "Download & Delete": "내려받고 삭제하기",
+  "Cancel": "취소하기",
+  "Layout": "레이아웃",
+  "Always visible": "항상 보임",
+  "Save my settings (in the browser store)": "(브라우저에) 설정 저장하기",
+  "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>저장된 게임 진도가 있는 JSON 파일을 선택해 진도를 불러오십시오.</p><1><0>경고:</0> 이를 실행하면 현재의 게임 진도가 삭제됩니다! <2>현재의 게임 진도</2>를 먼저 내려받을지 판단하십시오!</1>",
+  "Upload Saved Progress": "저장된 진도 업로드",
+  "Load selected file": "선택한 파일 열기",
+  "Mobile": "모바일",
+  "Auto": "자동",
+  "Desktop": "데스크톱",
+  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>여러분이 직접 게임을 작성할 생각이 있다면, <1>GameSkeleton 깃허브 저장소</1>를 양식[템플릿]으로 이용하고 <3>'게임 만들기(Creating a Game)'</3> 문서를 읽으십시오.</0><1>여러분이 작성한 게임을 직접 서버에서 불러오고, 정확한 URL을 이용해 그 게임을 하실 수 있습니다. 여러분의 게임을 서버에서 불러오는 방법에 관한 세부 사항도 위의 <1>설명서</1>에 나와 있습니다. 궁금한 점이 있으면 저희에게 연락해 주십시오.</1><p>이 페이지에 실린 게임들은 수동으로 추가됐습니다. 저희에게 연락하시면 여러분의 게임을 기꺼이 추가하겠습니다.",
+  "Level": "단계",
+  "Introduction": "소개",
+  "Retry proof from here": "여기부터 증명 다시 시도하기",
+  "Retry": "다시 시도하기",
+  "Failed command": "실패한 명령",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "",
+  "<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "",
+  "This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "",
+  " used": ""
+}

client/public/locales/ko/translation.json

@@ -0,0 +1 @@
+target/translation.json

client/public/locales/kr/translation.json

@@ -1,94 +0,0 @@
-{
-  "Intro": "",
-  "Game Introduction": "",
-  "World selection": "",
-  "Start": "",
-  "Inventory": "",
-  "next level": "",
-  "Next": "",
-  "back to world selection": "",
-  "Leave World": "",
-  "previous level": "",
-  "Previous": "",
-  "Editor mode is enforced!": "",
-  "Editor mode": "",
-  "Typewriter mode": "",
-  "information, Impressum, privacy policy": "",
-  "Preferences": "",
-  "Game Info & Credits": "",
-  "Game Info": "",
-  "Clear Progress": "",
-  "Erase": "",
-  "Download Progress": "",
-  "Download": "",
-  "Load Progress from JSON": "",
-  "Upload": "",
-  "Home": "",
-  "back to games selection": "",
-  "close inventory": "",
-  "show inventory": "",
-  "World": "",
-  "Show more help!": "",
-  "Goal": "",
-  "Objects": "",
-  "Assumptions": "",
-  "Current Goal": "",
-  "Further Goals": "",
-  "No Goals": "",
-  "Loading goal…": "",
-  "Click somewhere in the Lean file to enable the infoview.": "",
-  "Waiting for Lean server to start…": "",
-  "Level completed! 🎉": "",
-  "Level completed with warnings 🎭": "",
-  "Failed command": "",
-  "Retry proof from here": "",
-  "Retry": "",
-  "Active Goal": "",
-  "Crashed! Go to editor mode and fix your proof! Last server response:": "",
-  "Line": "",
-  "Character": "",
-  "Loading messages…": "",
-  "Execute": "",
-  "Tactics": "",
-  "Definitions": "",
-  "Theorems": "",
-  "Not unlocked yet": "",
-  "Not available in this level": "",
-  "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "",
-  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "",
-  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
-  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
-  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
-  "Prerequisites": "",
-  "Worlds": "",
-  "Levels": "",
-  "Language": "",
-  "Lean Game Server": "",
-  "Development notes": "",
-  "Adding new games": "",
-  "Funding": "",
-  "Level": "",
-  "Introduction": "",
-  "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "",
-  "Delete Progress?": "",
-  "Delete": "",
-  "Download & Delete": "",
-  "Cancel": "",
-  "Mobile": "",
-  "Auto": "",
-  "Desktop": "",
-  "Layout": "",
-  "Always visible": "",
-  "Save my settings (in the browser store)": "",
-  "<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "",
-  "Game Rules": "",
-  "levels": "",
-  "tactics": "",
-  "regular": "",
-  "relaxed": "",
-  "none": "",
-  "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "",
-  "Upload Saved Progress": "",
-  "Load selected file": "",
-  "Rules": ""
-}

client/public/locales/zh/translation.json

@@ -63,10 +63,7 @@
   "Not available in this level": "本关卡不提供",
   "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "这是一个为证明助手 <1>Lean</1> <i>(Lean 4)</i> 及其数学库 <5>mathlib</5> 设计的学习游戏库",
   "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "未加载游戏。访问 <1>http://localhost:3000/#/g/local/FOLDER</1> 从本地文件夹打开游戏。",
-  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "<p>这个服务器部署在我们大学的机器上，运行能力有限，目前估计最多可同时支持约 70 个游戏。我们希望将来能更有效地解决并测试这些限制。</p><1>游戏和基础设施的许多方面仍在开发之中。如果您遇到任何问题，欢迎在 <1>GitHub</1> 上提交问题反馈。</1>",
   "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>如果你打算编写自己的游戏，可以使用 <1>GameSkeleton Github Repo</1> 作为模板，并参阅 <3>如何创建游戏</3>。</0><1>你可以直接将游戏上传至服务器，并通过正确的 URL 进行游戏。上面的 <1>说明</1> 已详细介绍了如何将游戏加载到服务器的步骤。如果你有任何疑问，请随时联系我们。</1><p>本页上的精选游戏都是手动添加的。如果你想添加你的游戏，请与我们联系，我们非常欢迎。</p>",
-
-  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "此服务器是 Heinrich-Heine-Universität Düsseldorf 项目 <1>ADAM：预见数学的数字时代</1> 的一部分。",
   "Prerequisites": "前置条件",
   "Worlds": "世界",
   "Levels": "关卡",
@@ -91,5 +88,12 @@
   "Level": "关卡",
   "Introduction": "介绍",
   "Retry": "重试",
-  "Failed command": "命令失败"
+  "Failed command": "命令失败",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "",
+  "<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "",
+  "This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "",
+  "Server capacity": "",
+  "RAM": "",
+  " used": "",
+  "CPU": ""
 }

client/src/components/landing_page.tsx

@@ -122,25 +122,10 @@ function LandingPage() {
 
   /** Parse `games/stats.csv` if present and display server capacity. */
   React.useEffect(() => {
-    fetch(`${window.location.origin}/data/stats`)
+    const interval = setInterval(() => {
-    .then(response => {if (response.ok) {
+      fetch_stats();
-      return response.text() } else {throw ""}})
+    }, 2000)
-    .then(data => {
+    return () => clearInterval(interval)
-      // Parse the CSV content
-      const lines = data.split('\n');
-      const [header, line2] = lines;
-      if (!(header.replace(' ', '').startsWith("CPU,MEM"))) {
-        console.info("Not displaying server stats: received unexpected: ", header)
-      }
-      if (line2) {
-        let values = line2.split(',')
-        setUsageCPU(100 * Number(values[0]));
-        setUsageMem(100 * Number(values[1]));
-      }
-    }).catch(err => {
-      console.info('server stats unavailable')
-      console.debug(err)
-    })
   }, [])
 
   return <div className="landing-page">
@@ -186,9 +171,15 @@ function LandingPage() {
       <section>
         <div className="wrapper">
           <h2>{t("Server capacity")}</h2>
+          <Trans>
+            <p>
+              As this server runs lean on our university machines, it has a limited capacity.
+              Our current estimate is about 70 simultaneous games.
+            </p>
+          </Trans>
           <p>
-            { usageMem >= 0 && <> {t("RAM")}: <strong>{usageMem} % </strong> {t("used")}.<br/></> }
+            { usageMem >= 0 && <> {t("RAM")}: <strong>{usageMem.toFixed(2)} %</strong>{t(" used")}.<br/></> }
-            { usageCPU >= 0 && <> {t("CPU")}: <strong>{usageCPU} % </strong> {t("used")}. </> }
+            { usageCPU >= 0 && <> {t("CPU")}: <strong>{usageCPU.toFixed(2)} %</strong>{t(" used")}. </> }
           </p>
         </div>
       </section>
@@ -197,11 +188,6 @@ function LandingPage() {
       <div className="wrapper">
         <h2>{t("Development notes")}</h2>
         <Trans>
-          <p>
-            As this server runs lean on our university machines, it has a limited capacity.
-            Our current estimate is about 70 simultaneous games.
-            We hope to address and test this limitation better in the future.
-          </p>
           <p>
             Most aspects of the games and the infrastructure are still in development. Feel free to
             file a <a target="_blank" href="https://github.com/leanprover-community/lean4game/issues">GitHub Issue</a> about
@@ -239,8 +225,8 @@ function LandingPage() {
         <p>
           <Trans>
             This server has been developed as part of the
-            project <a target="_blank" href="https://hhu-adam.github.io">ADAM : Anticipating the Digital Age of Mathematics</a> at
+            project <a target="_blank" href="https://hhu-adam.github.io">ADAM: Anticipating the Digital Age of Mathematics</a> at
-            Heinrich-Heine-Universität in Düsseldorf.
+            Heinrich Heine University Düsseldorf.
           </Trans>
         </p>
       </div>
@@ -253,6 +239,31 @@ function LandingPage() {
     </footer>
   </div>
 
+
+  function fetch_stats() {
+    fetch(`${window.location.origin}/data/stats`)
+      .then(response => {
+        if (response.ok) {
+          return response.text();
+        } else { throw ""; }
+      })
+      .then(data => {
+        // Parse the CSV content
+        const lines = data.split('\n');
+        const [header, line2] = lines;
+        if (!(header.replace(' ', '').startsWith("CPU,MEM"))) {
+          console.info("Not displaying server stats: received unexpected: ", header);
+        }
+        if (line2) {
+          let values = line2.split(',');
+          setUsageCPU(100 * parseFloat(values[0]));
+          setUsageMem(100 * parseFloat(values[1]));
+        }
+      }).catch(err => {
+        console.info('server stats unavailable');
+        console.debug(err);
+      });
+  }
 }
 
 export default LandingPage

client/src/config.json

@@ -3,7 +3,8 @@
     "leanprover-community/nng4",
     "hhu-adam/robo",
     "djvelleman/stg4",
-    "trequetrum/lean4game-logic"
+    "trequetrum/lean4game-logic",
+    "jadabouhawili/knightsandknaves-lean4game"
   ],
 
   "languages": [
@@ -28,7 +29,7 @@
       "name": "Español"
     },
     {
-      "iso": "kr",
+      "iso": "ko",
       "flag": "KR",
       "name": "한국어"
     }

client/src/index.tsx

@@ -36,12 +36,12 @@ const router = createHashRouter([
   {
     // For backwards compatibility
     path: "/game/nng",
-    loader: () => redirect("/g/hhu-adam/NNG4")
+    loader: () => redirect("/g/leanprover-community/nng4")
   },
   {
     // For backwards compatibility
     path: "/g/hhu-adam/NNG4",
-    loader: () => redirect("/g/leanprover-community/NNG4")
+    loader: () => redirect("/g/leanprover-community/nng4")
   },
   {
     path: "/g/:owner/:repo",

doc/publish_game.md

@@ -24,7 +24,11 @@ You should see a white screen which shows import updates and eventually reports
 
 Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`!
 
-## 4. Main page
+## 4. Update
+
+To upload a new version of the game you will have to repeat 1. and 2. whenever you want to publish the updated version.
+
+## 5. Main page
 
 Adding games to the main page happens manually by the server maintainers. Tell us if you want us
 to add a tile for your game!

docker-compose.yml

@@ -0,0 +1,14 @@
+services:
+  lean4game:
+    build: .
+    privileged: true # needed to run bubblewrap inside docker
+    environment:
+      - LEAN4GAME_GITHUB_USER=${LEAN4GAME_GITHUB_USER}
+      - LEAN4GAME_GITHUB_TOKEN=${LEAN4GAME_GITHUB_TOKEN}
+    ports:
+      - "8080:8080"
+    volumes:
+      - games_data:/app/games
+
+volumes:
+  games_data:

relay/cpu_usage.py

@@ -0,0 +1,43 @@
+import time
+
+def measure_proc_stat() -> dict[str, int]:
+  proc_stat_header = open("/proc/stat", "r").readline()
+  proc_stat = proc_stat_header.split(' ')[2:]
+  proc_stat[-1] = proc_stat[-1].removesuffix('\n')
+  proc_stat = list(map(int, proc_stat))
+
+  proc_stat_dict= {'user': proc_stat[0],
+                   'nice': proc_stat[1],
+                   'system': proc_stat[2],
+                   'idle': proc_stat[3],
+                   'iowait': proc_stat[4],
+                   'irq': proc_stat[5],
+                   'softirq': proc_stat[6],
+                   'steal': proc_stat[7],
+                   'guest': proc_stat[8],
+                   'guest_nice': proc_stat[9]}
+
+  return proc_stat_dict
+
+if __name__ == "__main__":
+  """
+  Script emulates htop calculation of CPU at the
+  moment of calling.
+  """
+  prev = measure_proc_stat()
+  prev_idle = prev.get('idle') + prev.get('iowait')
+  prev_non_idle = prev.get('user') + prev.get('nice') + prev.get('system') + prev.get('irq') + prev.get('softirq') + prev.get('steal')
+  prev_total = prev_idle + prev_non_idle
+
+  time.sleep(0.1)
+
+  curr = measure_proc_stat()
+  curr_idle = curr.get('idle') + curr.get('iowait')
+  curr_non_idle = curr.get('user') + curr.get('nice') + curr.get('system') + curr.get('irq') + curr.get('softirq') + curr.get('steal')
+  curr_total = curr_idle + curr_non_idle
+
+  d_total = curr_total - prev_total
+  d_idle = curr_idle - prev_idle
+
+  cpu_usage = ((d_total - d_idle)/d_total)
+  print(cpu_usage)

relay/index.mjs

@@ -20,9 +20,9 @@ import { spawn } from 'child_process'
 */
 const queueLength = {
   "g/hhu-adam/robo": 2,
-  "g/hhu-adam/nng4": 5,
+  "g/leanprover-community/nng4": 5,
-  "g/djvelleman/stg4": 0,
+  "g/djvelleman/stg4": 2,
-  "g/trequetrum/lean4game-logic": 0,
+  "g/trequetrum/lean4game-logic": 2,
 }
 
 const __filename = url.fileURLToPath(import.meta.url);
@@ -71,15 +71,7 @@ const server = app
     express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next);
   })
   .use('/data/stats', (req, res, next) => {
-    // Returns a CSV of the form
-    //
-    // CPU,Mem
-    // 0.21,0.65
-    //
-    // which contains the current server usage.
-
     const statsProcess = spawn('/bin/bash', [path.join(__dirname, "stats.sh"), process.pid])
-
     let outputData = ''
     let errorData = ''
     statsProcess.stdout.on('data', (data) => {

relay/stats.sh

@@ -1,10 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# first argument is the process ID
+# Load python interpreter
-pid="$1"
+python=/usr/bin/python3
+# Load python script
+cpu_usage=relay/cpu_usage.py
+# Execute python script
+cpu=$($python $cpu_usage)
+# Calculate memory usage by computing 1 - %free_memory
+mem=$(free | sed '2q;d' | awk '{print 1 - ($4/$2)}')
 
-# number of CPUs available
+printf "CPU, MEM\n%f, %f\n" $cpu $mem
-nproc=$(nproc --all)
-
-# hacky way to print the content of a CSV file containing CPU/Mem usage of the process
-top -bn2 -p $pid | awk -v nproc=$nproc 'NR > 16 {$12=substr($0,72); printf "CPU, MEM\n%.2f, %.2f\n", $9/nproc, $10}'