Add line of contact for upload issues and set reserve disc space as environment variable.

feat: add game `Knights and Knaves` by JadAbouHawili

.gitignore

@@ -3,3 +3,6 @@ client/dist
 games/
 server/.lake
 **/.DS_Store
+logs/
+relay/prev_cpu_metric
+test.ecosystem.config.cjs

README.md

@@ -8,7 +8,7 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
 
 * Step 5: [How to Run Games Locally](doc/running_locally.md)
 * Step 7: [How to Update an existing Game](doc/update_game.md)
-* Step 8: [How to Publishing a Game](doc/publish_game.md)
+* Step 9: [How to Publishing a Game](doc/publish_game.md)
 * [Troubleshooting](doc/troubleshoot.md)
 
 ## Documentation
@@ -37,13 +37,24 @@ not fully written yet.
 
 Contributions to `lean4game` are always welcome!
 
+### Translation
+
+The interface can be translated to various languages. For adding a translation, one needs to do the following:
+
+1. In `client/src/config.json`, add your new language. The "iso" key is the ISO language code, i.e. it should be accepted by "i18next" and "GNU gettext"; the "flag" key is once accepted by [react-country-flag](https://www.npmjs.com/package/react-country-flag).
+2. Run `npm run translate`. This should create a new file `client/public/locales/{language}/translation.json`. (alternatively you can copy-paste `client/public/locales/en/translation.json`)
+3. Add all translations.
+4. Commit the changes you made to `config.json` together with the new `translation.json`.
+
+For translating games, see [Translating a game](doc/translate.md).
+
 ## Security
 
 Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.
 
 ## Credits
 
-The project has pimarily been developed by Alexander Bentkamp and Jon Eugster.
+The project has primarily been developed by Alexander Bentkamp and Jon Eugster.
 
 It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)

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

@@ -0,0 +1,99 @@
+{
+  "Intro": "Introducción",
+  "Game Introduction": "Introducción del juego",
+  "World selection": "Seleccionar mundo",
+  "Start": "Empezar",
+  "Inventory": "Inventario",
+  "next level": "siguiente nivel",
+  "Next": "Siguiente",
+  "back to world selection": "volver a la selección de mundos",
+  "Leave World": "Abandonar mundo",
+  "previous level": "nivel anterior",
+  "Previous": "Anterior",
+  "Editor mode is enforced!": "¡El modo editor es obligatorio!",
+  "Editor mode": "Modo editor",
+  "Typewriter mode": "Modo línea a línea",
+  "information, Impressum, privacy policy": "información, Impressum, política de privacidad",
+  "Preferences": "Preferencias",
+  "Game Info & Credits": "Información del juego y reconocimientos",
+  "Game Info": "Información del juego",
+  "Clear Progress": "Limpiar el progreso",
+  "Erase": "Borrar",
+  "Download Progress": "Descargar progreso",
+  "Download": "Descargar",
+  "Load Progress from JSON": "Cargar progreso desde JSON",
+  "Upload": "Subir",
+  "Home": "Inicio",
+  "back to games selection": "volver a la selección de juegos",
+  "close inventory": "cerrar inventario",
+  "show inventory": "mostrar inventario",
+  "World": "Mundo",
+  "Show more help!": "¡Mostrar más ayuda!",
+  "Goal": "Objetivo",
+  "Objects": "Objetos",
+  "Assumptions": "Hipótesis",
+  "Current Goal": "Objetivo actual",
+  "Further Goals": "Objetivos pendientes",
+  "No Goals": "Sin objetivos",
+  "Loading goal…": "Cargando objetivo…",
+  "Click somewhere in the Lean file to enable the infoview.": "Pulsa en algún lugar del archivo Lean para habilitar la vista de información.",
+  "Waiting for Lean server to start…": "Esperando a que el servidor Lean se inicie…",
+  "Level completed! 🎉": "Nivel completado 🎉",
+  "Level completed with warnings 🎭": "Nivel completado con advertencias 🎭",
+  "Failed command": "Comando fallido",
+  "Retry proof from here": "Reintentar la prueba desde aquí",
+  "Retry": "Reintentar",
+  "Active Goal": "Objetivo activo",
+  "Crashed! Go to editor mode and fix your proof! Last server response:": "¡Error! Vaya al modo editor y corrija su prueba. Última respuesta del servidor:",
+  "Line": "Línea",
+  "Character": "Carácter",
+  "Loading messages…": "Cargando mensajes…",
+  "Execute": "Ejecutar",
+  "Tactics": "Tácticas",
+  "Definitions": "Definiciones",
+  "Theorems": "Teoremas",
+  "Not unlocked yet": "No desbloqueado aún",
+  "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",
+  "<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>",
+  "Prerequisites": "Requisitos previos",
+  "Worlds": "Mundos",
+  "Levels": "Niveles",
+  "Language": "Idioma",
+  "Lean Game Server": "Servidor de Juegos de Lean",
+  "Development notes": "Notas de desarrollo",
+  "Adding new games": "Añadir nuevos juegos",
+  "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>",
+  "Delete Progress?": "¿Borrar Progreso?",
+  "Delete": "Borrar",
+  "Download & Delete": "Descargar y Borrar",
+  "Cancel": "Cancelar",
+  "Mobile": "Móvil",
+  "Auto": "Automático",
+  "Desktop": "Escritorio",
+  "Layout": "Diseño",
+  "Always visible": "Siempre visible",
+  "Save my settings (in the browser store)": "Guardar mis ajustes (en el almacenamiento del navegador)",
+  "<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>Las reglas del juego determinan si se permite saltarse niveles y si el juego realiza comprobaciones para permitir únicamente tácticas y teoremas desbloqueados en las pruebas.</p><1>Nota: las tácticas (o teoremas) \"Desbloqueadas\" está determinadas por dos cosas: el conjunto mínimo de tácticas necesarias para resolver un nivel, más cualquier táctica que hayas desbloqueado en otro nivel. Esto significa que si desbloqueas <1>simp</1> en un nivel, puedes usarlo a partir de entonces en cualquier nivel.</1><p>Las opciones son:</p>",
+  "Game Rules": "Reglas del juego",
+  "levels": "niveles",
+  "tactics": "tácticas",
+  "regular": "normal",
+  "relaxed": "relajado",
+  "none": "ninguno",
+  "<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",
+  "<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/zh/translation.json

@@ -1,7 +1,7 @@
 {
   "Tactics": "策略",
-  "Lean Game Server": "",
+  "Lean Game Server": "LEAN 游戏服务器",
-  "<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>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在另一个关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp</1>，那么你可以在任何关卡中使用它。</1><p>选项是：</p>",
+  "<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>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在其他关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp</1>，你可以在任何关卡中使用它。</1><p>选项有：</p>",
   "Game Rules": "游戏规则",
   "levels": "关卡",
   "tactics": "策略",
@@ -20,11 +20,11 @@
   "Leave World": "离开世界",
   "previous level": "上一关",
   "Previous": "上一关",
-  "Editor mode is enforced!": "编辑器模式开启！",
+  "Editor mode is enforced!": "编辑器模式已启用！",
   "Editor mode": "编辑器模式",
   "Typewriter mode": "打字机模式",
-  "information, Impressum, privacy policy": "",
+  "information, Impressum, privacy policy": "信息、版权说明、隐私政策",
-  "Preferences": "",
+  "Preferences": "偏好设置",
   "Game Info & Credits": "游戏信息和荣誉",
   "Game Info": "游戏信息",
   "Clear Progress": "清除进度",
@@ -43,14 +43,14 @@
   "Current Goal": "当前目标",
   "Objects": "对象",
   "Assumptions": "假设",
-  "Further Goals": "Further Goals",
+  "Further Goals": "进一步目标",
   "No Goals": "无目标",
-  "Loading goal…": "加载目标。。。",
+  "Loading goal…": "加载目标中。。。",
-  "Click somewhere in the Lean file to enable the infoview.": "单击Lean文件中的某处以启用信息视图。",
+  "Click somewhere in the Lean file to enable the infoview.": "单击 Lean 文件中的某处以启用信息视图。",
-  "Waiting for Lean server to start…": "等待 Lean 服务器启动。。。",
+  "Waiting for Lean server to start…": "等待 Lean 服务器启动中…",
-  "Level completed! 🎉": "完成关卡！🎉",
+  "Level completed! 🎉": "关卡完成！🎉",
   "Level completed with warnings 🎭": "关卡完成（带有警告） 🎭",
-  "Retry proof from here": "从这里重新试着证明",
+  "Retry proof from here": "从这里重新尝试证明",
   "Active Goal": "当前目标",
   "Crashed! Go to editor mode and fix your proof! Last server response:": "程序崩溃！请转到编辑器模式，修复您的证明！最后一次服务器响应：",
   "Line": "行",
@@ -61,34 +61,39 @@
   "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>": "",
+  "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>直接从本地文件夹打开游戏。",
+  "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>": "",
+  "<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>",
-  "<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": "世界(Worlds)",
+  "Worlds": "世界",
   "Levels": "关卡",
   "Language": "语言",
-  "Development notes": "",
+  "Development notes": "开发笔记",
-  "Adding new games": "",
+  "Adding new games": "添加新游戏",
-  "Funding": "",
+  "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>",
+  "<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)": "",
+  "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>",
+  "<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": "桌面端",
-  "Level": "",
+  "Level": "关卡",
-  "Introduction": "",
+  "Introduction": "介绍",
-  "Retry": "",
+  "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

@@ -95,6 +95,9 @@ function LandingPage() {
   const closePreferencesPopup = () => setPreferencesPopup(false);
   const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup);
 
+  const [usageCPU, setUsageCPU] = React.useState<number>()
+  const [usageMem, setUsageMem] = React.useState<number>()
+
   const { t, i18n } = useTranslation()
 
   // Load the namespaces of all games
@@ -117,6 +120,14 @@ function LandingPage() {
     return q.data?.tile
   })
 
+  /** Parse `games/stats.csv` if present and display server capacity. */
+  React.useEffect(() => {
+    const interval = setInterval(() => {
+      fetch_stats();
+    }, 2000)
+    return () => clearInterval(interval)
+  }, [])
+
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
       <nav className="landing-page-nav">
@@ -155,15 +166,28 @@ function LandingPage() {
         ))
       }
     </div>
+    { // show server capacity from `games/stats.csv` if present
+      (usageMem >= 0 || usageCPU >= 0 ) &&
+      <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.toFixed(2)} %</strong>{t(" used")}.<br/></> }
+            { usageCPU >= 0 && <> {t("CPU")}: <strong>{usageCPU.toFixed(2)} %</strong>{t(" used")}. </> }
+          </p>
+        </div>
+      </section>
+    }
     <section>
       <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
@@ -201,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>
@@ -215,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": [
@@ -21,6 +22,16 @@
       "iso": "zh",
       "flag": "CN",
       "name": "中文"
+    },
+    {
+      "iso": "es",
+      "flag": "ES",
+      "name": "Español"
+    },
+    {
+      "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",

client/src/state/preferences.ts

@@ -18,8 +18,8 @@ export const AUTO_SWITCH_THRESHOLD = 800
 const initialState: PreferencesState = loadPreferences() ??{
     layout: "auto",
     isSavePreferences: false,
-    language: "en",
+    language: import.meta.env.VITE_CLIENT_DEFAULT_LANGUAGE || "en",
-}
+};
 
 export const preferencesSlice = createSlice({
   name: "preferences",

doc/create_game.md

@@ -6,11 +6,11 @@ This tutorial walks you through creating a new game for lean4. It covers from wr
 
 1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
 2. Clone the game repo.
-3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
+3. Call `lake update -R && lake build` to build the Lean project.
 
-Note that you need to host your game's code on github to publish it online later on. If you only
+### Running the game
-want to play it locally, you can simply clone the NNG repo and start modifying that one.
 
+Now you can open the game in VSCode (`cd YourGame/` and `code .`), and start modifying it like a regular Lean project. To run the game consult the section "**5. Testing the Game Locally**" below.
 
 ## 2. Game.lean
 
@@ -194,7 +194,7 @@ You can but a `Statement` inside namespaces like you would with `theorem`.
 
 #### Doc String / Exercise statement
 
-Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.
+Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. See [LaTeX in Games](latex.md) for more details on formatting.
 
 ```lean
 /-- The exercise statement in natural language using latex: $\iff$. -/
@@ -242,7 +242,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the
 
 In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md).
 
-## 8. Publish your game
+## 8. Add translation
+
+See [Translating a game](translate.md).
+
+## 9. Publish your game
 
 To publish your game on the official server, see [Publishing a game](publish_game.md)
 
@@ -261,13 +265,21 @@ CoverImage "images/cover.png"
 * `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
 * `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
 
-## Further Notes
+## 10. Advanced Topics
 
-Here are some random further things you should consider designing a new game:
+### Escaping
 
-* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
+Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
   would write `Introduction "some latex here: $\\iff$."` but
   `/-- some latex here: $\iff$. -/ Statement ...`
-* A world with more than 16 levels will be displayed with the levels spiraling outwards,
+
-  it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out
+### LaTeX support
-  of control.
+
+LaTeX is rendered using the [KaTeX library](https://katex.org/),
+see [Using LaTeX in the Game](latex.md) for details.
+
+### Number Of Levels Limit
+
+A world with more than 16 levels will be displayed with the levels spiraling outwards,
+it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out
+of control.

doc/hints.md

@@ -33,7 +33,7 @@ You can use `Branch` to place hints
 in dead ends or alternative proof strands.
 
 A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end
-so that no progress has been made on proofing the goal.
+so that no progress has been made on proving the goal.
 
 ```
 Statement .... := by
@@ -49,6 +49,9 @@ Statement .... := by
 Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
 the variable's name with the one the user actually used.
 
+*Note*: This means you need to escape any other uses of **opening** curly brackets (i.e. `\{`). See also [LaTeX in Games](latex.md) for
+examples of this.
+
 For example, if the sample proof contains
 
 ```
@@ -84,38 +87,19 @@ create new assumptions.
 
 ## 6. Formatting
 
-You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
+You can use Markdown to format your hints and you can
+use LaTeX. See [LaTeX in Games](latex.md) for more details.
 
-**Escaping**: Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
+### Images
-backslashes, but if you provide text inside a doc comment
-`/-- -/` (e.g. in the `Statement` description) you do not!
 
-TODO: Write a doc about latex/markdown options available.
+Hints and introductions/conclusions can also contain images.
 
-### Commutative diagrams
+For remote images, simply add:
-
-Here is an example of how to write a commutative diagram in KaTeX:
-
-$$
-\begin{CD}
-      A  @>{f}>> B @<{g}<< C    \\
-  @V{h}VV    @V{i}VV   @V{j}VV \\
-      D  @<{k}<< E @>{l}>> F    \\
-  @A{m}AA    @A{n}AA   @V{p}VV \\
-      G  @<{q}<< H @>{r}>> I
-\end{CD}
-$$
 
 ```
-$$
+<img src=\"https://url.com/to/image\"/>
-\\begin{CD}
-      A  @>{f}>> B @<{g}<< C    \\\\
-  @V{h}VV    @V{i}VV   @V{j}VV \\\\
-      D  @<{k}<< E @>{l}>> F    \\\\
-  @A{m}AA    @A{n}AA   @V{p}VV \\\\
-      G  @<{q}<< H @>{r}>> I
-\\end{CD}
-$$
 ```
 
-See https://www.jmilne.org/not/Mamscd.pdf
+Local images can currently only be included with a hack:
+
+Images in the game's `images/` folder will be accessible at `data/g/[user]/[repo]/[image].[png|jpg|…]` and thus can be included as if they were external images.

doc/latex.md

@@ -0,0 +1,78 @@
+There are multiple ways how to format the text content of your game. Notably Markdown with KaTeX.
+
+# Escaping
+Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
+backslashes, but if you provide text inside a doc comment
+`/-- -/` (e.g. in the `Statement` description) you do not!
+
+This means for example you'd write `/-- $\iff$ -/` but `"$\\iff$"`.
+
+Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
+
+# KaTeX
+
+LaTeX syntax is provided trough the [KaTeX library](https://katex.org). KateX supports most but not all of latex and its packages.
+See [supported](https://katex.org/docs/supported.html).
+
+## Examples
+
+### Commutative diagrams
+
+Here is an example of how to write a commutative diagram in KaTeX:
+
+$$
+\begin{CD}
+      A  @>{f}>> B @<{g}<< C    \\
+  @V{h}VV    @V{i}VV   @V{j}VV \\
+      D  @<{k}<< E @>{l}>> F    \\
+  @A{m}AA    @A{n}AA   @V{p}VV \\
+      G  @<{q}<< H @>{r}>> I
+\end{CD}
+$$
+
+```
+$$
+\begin{CD}
+      A  @>{f}>> B @<{g}<< C    \\
+  @V{h}VV    @V{i}VV   @V{j}VV \\
+      D  @<{k}<< E @>{l}>> F    \\
+  @A{m}AA    @A{n}AA   @V{p}VV \\
+      G  @<{q}<< H @>{r}>> I
+\end{CD}
+$$
+```
+
+Again, note that inside a string like `Hint`/`Introduction`/`Conclusion`/etc. you need to escape `\` and potentially `{`.
+
+E.g. `\begin` as `\\begin`, `\\` as `\\\\` and inside a
+`Hint`, `@>{f}>>` as `@>\{f}>>`.
+
+See https://www.jmilne.org/not/Mamscd.pdf
+
+### Truth Tables
+
+KaTeX does not support the tabular environment. You can use the array environment instead.
+
+$$
+\begin{array}{|c|c|}
+  \hline
+  P & ¬P \\
+  \hline
+  T & F  \\
+  F & T  \\
+  \hline
+\end{array}
+$$
+
+```
+$$
+\begin{array}{|c|c|}
+  \hline
+  P & ¬P \\
+  \hline
+  T & F  \\
+  F & T  \\
+  \hline
+\end{array}
+$$
+```

doc/npm_scripts.md

@@ -7,3 +7,13 @@ Internally, websocket requests to `ws://localhost:3000/websockets` will be forwa
 On the server side, the command will set up a docker image containing the Lean server. The two parts can be built separately using `npm run build_client` and `npm run build_server`.
 
 * `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specific port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the bubblewrapped Lean server via the web socket protocol.
+
+### Environment Variables
+
+The client and server ports, as well as the default language, can be configured using environment variables:
+
+* `PORT`: Sets the port for the backend server (default: `8080`).
+* `CLIENT_PORT`: Sets the port for the client server (default: `3000`).
+* `VITE_CLIENT_DEFAULT_LANGUAGE`: Sets the default language for the application (default: `en`).
+
+Ensure these environment variables are set appropriately in your environment to configure the project as needed.

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!

doc/server.md

@@ -26,3 +26,22 @@ where you replace:
 Everything downloaded remains in the folder `lean4game/games`.
 The subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
 The other folders should only contain the built lean-games, sorted by owner and repo.
+
+## Server capacity
+
+If you would like to display the server capacity on the landing page,
+you can create a file `lean4game/games/stats.csv` of the following form:
+
+```
+CPU,MEM
+0.1,0.8
+```
+
+These numbers will be displayed on the landing page ("CPU: 10 % used" and "RAM: 80 % used").
+
+If you only want one of the numbers, replace the number you don't want with `nan` (or anything
+else which does not parse as number).
+
+If you don't want to show either, simply do not create `stats.csv`
+
+Use your own script or cronjob to update the CSV file as desired.

doc/translate.md

@@ -0,0 +1,30 @@
+# Translation
+
+The game server supports internationalisation ("i18n") using [lean-i18n](https://github.com/hhu-adam/lean-i18n) and [i18next](https://www.npmjs.com/package/i18next).
+
+The intended workflow currently is the following:
+
+1. When you call `lake build` in your game, it should automatically create a template file `.i18n/en/Game.pot`. Alternatively you can call `lake exe i18n --template` to recreate it.
+2. Open the file `Game.pot` (the "t" stands for "template") with [Poedit](https://poedit.net/) (or a similar software) and translate all strings. Save your work as `.i18n/{language}/Game.po`.
+4. Call `lake exe i18n --export-json` to create all Json files `.i18n/{language}/Game.json` which the server needs.
+5. Add your translations (i.e. `.po` and `.json`, but not the `.mo` files) and push your results, and [publish the game](publish_game.md).
+
+If you choose the correct language in the "Preferences" of the game, you should see your translations.
+
+## Alternative: avoiding .po
+
+Note: This workflow is subject to change, and it might be that in future the server can directly read `.po` files. Until then, there is also an alternative workflow you might choose:
+
+0. Add `useJson: true` to `.i18n/config.json`
+1. `lake build` or `lake exe i18n --template` will now create a Json instead: `.i18n/en/Game.json`.
+2. Add translations to a copy of this Json an save it as `.i18n/{language}/Game.json`
+
+## Non-English games
+
+For games written in a language different than English, you should set the correct source language (`sourceLang`) in `.i18n/config.json`. Afterwards, on `lake build` the template should appear under the chosen language, and can be translated (e.g. into English) as described above.
+
+## New languages
+
+The server has a set number of languages one can select.
+If your game has been translated to a language not selectable, [open an issue at lean4game](https://github.com/leanprover-community/lean4game/issues) requesting this new language.
+Or, even better, create a PR to translate the [server interface](https://github.com/leanprover-community/lean4game/tree/main/client/public/locales) into that new language.

ecosystem.config.cjs

@@ -6,6 +6,8 @@ module.exports = {
     env: {
       LEAN4GAME_GITHUB_USER: "",
       LEAN4GAME_GITHUB_TOKEN: "",
+      RES_DISC_SPACE_PERCENTAGE: 1.0,
+      ISSUE_CONTACT: "",
       NODE_ENV: "production",
       PORT: 8002
     },

index.html

@@ -33,7 +33,7 @@
       </p>
     </div>
   </noscript>
-  <script type="module" src="/client/src/index.tsx"></script>
+  <script type="module" src="client/src/index.tsx"></script>
 </body>
 
 </html>

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/import.mjs

@@ -1,22 +1,26 @@
 import { spawn } from 'child_process'
-import fs from 'fs';
+import fs, { stat } from 'fs';
 import request from 'request'
 import requestProgress from 'request-progress'
 import { Octokit } from 'octokit';
 
 import { fileURLToPath } from 'url';
-import path from 'path';
+import path, { resolve } from 'path';
+import { error } from 'console';
 
 const __filename = fileURLToPath(import.meta.url);
 const __dirname = path.dirname(__filename);
 
 const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN
 const USERNAME = process.env.LEAN4GAME_GITHUB_USER
+const MEM_THRESHOLD = process.env.RES_DISC_SPACE_PERCENTAGE
+const CONTACT = process.env.ISSUE_CONTACT
 const octokit = new Octokit({
   auth: TOKEN
 })
 
 const progress = {}
+var exceedingMemoryLimit = false
 
 async function runProcess(id, cmd, args, cwd) {
   return new Promise((resolve, reject) => {
@@ -36,6 +40,28 @@ async function runProcess(id, cmd, args, cwd) {
   })
 }
 
+
+async function checkAgainstDiscMemory(artifact, maxPercentage) {
+  return new Promise((resolve, reject) => {
+  fs.statfs("/", (err, stats) => {
+    if (err) {
+      console.log(err);
+      reject()
+    }
+    let artifactBytes = artifact.size_in_bytes;
+    let totalBytes = stats.blocks * stats.bsize;
+    let freeBytes = stats.bfree * stats.bsize;
+    let usedBytes = totalBytes - freeBytes;
+    let maxUsedBytes = totalBytes * maxPercentage;
+    if (usedBytes + artifactBytes >= maxUsedBytes) {
+      exceedingMemoryLimit = true;
+    }
+    resolve()
+  });
+  })
+}
+
+
 async function download(id, url, dest) {
   return new Promise((resolve, reject) => {
     // The options argument is optional so you can omit it
@@ -49,7 +75,9 @@ async function download(id, url, dest) {
       }
     }))
     .on('progress', function (state) {
-      progress[id].output += `Downloaded ${Math.round(state.size.transferred/1024/1024)}MB\n`
+      console.log('progress', state);
+      transferredDataSize = Math.round(state.size.transferred/1024/1024)
+      progress[id].output += `Downloaded ${transferredDataSize}MB\n`
     })
     .on('error', function (err) {
       reject(err)
@@ -73,9 +101,16 @@ async function doImport (owner, repo, id) {
         'X-GitHub-Api-Version': '2022-11-28'
       }
     })
-    // choose latest artifact
     const artifact = artifacts.data.artifacts
       .reduce((acc, cur) => acc.created_at < cur.created_at ? cur : acc)
+
+    await checkAgainstDiscMemory(artifact, MEM_THRESHOLD);
+
+    if (exceedingMemoryLimit === true) {
+      throw new Error(`Uploading file of size ${Math.round(artifact.size_in_bytes / 1024 / 1024)} (MB) would exceed allocated memory on the server.\n
+      Please notify server admins via <a href=${CONTACT}>the LEAN zulip instance</a> to resolve this issue.`);
+    }
+
     artifactId = artifact.id
     const url = artifact.archive_download_url
     // Make sure the download folder exists
@@ -91,7 +126,6 @@ async function doImport (owner, repo, id) {
 
     await runProcess(id, "/bin/bash", [path.join(__dirname, "unpack.sh"), artifactId, owner.toLowerCase(), repo.toLowerCase()], path.join(__dirname, ".."))
 
-
     // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`);
     // manifest = JSON.parse(manifest);
     // if (manifest.length !== 1) {

relay/index.mjs

@@ -9,6 +9,8 @@ import os from 'os';
 import fs from 'fs';
 import anonymize from 'ip-anonymize';
 import { importTrigger, importStatus } from './import.mjs'
+import process from 'process';
+import { spawn } from 'child_process'
 // import fs from 'fs'
 
 /**
@@ -18,9 +20,9 @@ import { importTrigger, importStatus } from './import.mjs'
 */
 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);
@@ -41,6 +43,22 @@ const server = app
     const owner = req.params.owner;
     const repo = req.params.repo
     const lang = req.params.lang
+
+    const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
+    const log = `${process.cwd()}/logs/game-access.log`
+    const header = "date;anon-ip;game;lang\n"
+    const data = `${new Date()};${ip};${owner}/${repo};${lang}\n`
+
+    fs.writeFile(log, header.concat(data), { flag: 'ax' }, (file_exists) => {
+	    if (file_exists) {
+		fs.appendFile(log, data, (err) => {
+		  if (err) console.log("Failed to append to log!")
+		});
+	    }
+    });
+
+    console.log(`[${new Date()}] ${ip} requested translation for ${owner}/${repo} in ${lang}`)
+
     const filename = req.params[0];
     req.url = filename;
     express.static(path.join(getGameDir(owner,repo),".i18n",lang))(req, res, next);
@@ -52,6 +70,25 @@ const server = app
     req.url = filename;
     express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next);
   })
+  .use('/data/stats', (req, res, next) => {
+    const statsProcess = spawn('/bin/bash', [path.join(__dirname, "stats.sh"), process.pid])
+    let outputData = ''
+    let errorData = ''
+    statsProcess.stdout.on('data', (data) => {
+      outputData += data.toString();
+    })
+    statsProcess.stderr.on('data', (data) => {
+      errorData += data.toString();
+    })
+    statsProcess.on('close', (code) => {
+      if (code === 0) {
+        res.send(outputData);
+      } else {
+        res.status(500).send(`Error executing script: ${errorData}`)
+        console.error(`stats.sh exited with code ${code}. Error: ${errorData}`)
+      }
+    })
+  })
   .use('/', router)
   .listen(PORT, () => console.log(`Listening on ${PORT}`));
 
@@ -178,7 +215,9 @@ wss.addListener("connection", function(ws, req) {
 
     socketCounter += 1;
     const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
-    console.log(`[${new Date()}] Socket opened - ${ip}`)
+
+    // TODO (Matvey): extract further information from `req`, for example browser language.
+    console.log(`[${new Date()}] Socket opened - ${ip} - ${owner}/${repo}`)
 
     const socket = {
         onMessage: (cb) => { ws.on("message", cb) },

relay/stats.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+# Load python interpreter
+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)}')
+
+printf "CPU, MEM\n%f, %f\n" $cpu $mem

server/GameServer/AbstractCtx.lean

@@ -21,7 +21,7 @@ def abstractCtx (goal : MVarId) : MetaM AbstractCtxResult := do
 def openAbstractCtxResult (res : AbstractCtxResult) (k : Array Expr → Expr → MetaM α) : MetaM α := do
   let (_mvars, _binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult
   lambdaLetTelescope (← instantiateMVars expr) k
-  -- TODO: Unfornately, lambdaLetTelescope does not allow us to provide the number of arguments.
+  -- TODO: Unfortunately, lambdaLetTelescope does not allow us to provide the number of arguments.
   -- If the goal is a function, this will not work.
 
 end AbstractCtx

server/GameServer/Commands.lean

@@ -119,7 +119,7 @@ elab "Languages" t:str* : command => do
   modifyCurGame fun game => pure {game with
     tile := {game.tile with languages := t.map (·.getString) |>.toList}}
 
-/-- The Image of the game (optional). TODO: Not impementeds -/
+/-- The Image of the game (optional). TODO: Not implemented -/
 elab "CoverImage" t:str : command => do
   let file := t.getString
   if not <| ← System.FilePath.pathExists file then
@@ -610,7 +610,7 @@ where filterArgs (args : List Syntax) : List Syntax :=
     | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
     | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r =>
       filterArgs r
-    -- delete `Hint` and `Branch` occurence at the end of the tactic sequence.
+    -- delete `Hint` and `Branch` occurrence at the end of the tactic sequence.
     | Syntax.node _ `GameServer.Tactic.Hint _ :: []
     | Syntax.node _ `GameServer.Tactic.Branch _ :: [] =>
         []

server/GameServer/FileWorker.lean

@@ -187,7 +187,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
 
 where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
   -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
-  -- deppending on difficulty.
+  -- depending on difficulty.
   let difficulty := workerState.difficulty
   if difficulty > 0 then
     addMessage info inputCtx (if difficulty > 1 then .error else .warning) s
@@ -383,7 +383,7 @@ def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.Ini
   -- -- Should we get the diags from there?
   -- let diag : Array Widget.InteractiveDiagnostic := snap.interactiveDiags.toArray
 
-  -- -- Level is completed if there are no errrors or warnings
+  -- -- Level is completed if there are no errors or warnings
   -- let completed : Bool := ¬ diag.any (fun d =>
   --   d.severity? == some .error ∨ d.severity? == some .warning)
 

server/GameServer/RpcHandlers.lean

@@ -231,7 +231,7 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo
       -- Answer: The last snap only copied the diags from the end of this snap
       let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray
 
-      -- Level is completed if there are no errrors or warnings
+      -- Level is completed if there are no errors or warnings
       let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error)
       let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)
 

server/GameServer/Tactic/LetIntros.lean

@@ -44,7 +44,7 @@ def _root_.Lean.MVarId.letIntros (mvarId : MVarId) : MetaM (Array FVarId × MVar
     mvarId.introNP n
 
 /--
-`let_intros` introduces all `let` statements that are preceeding the proof. Concretely
+`let_intros` introduces all `let` statements that are preceding the proof. Concretely
 it does a subset of what `intros` does.
 
 If names are provided, it will introduce as many `let` statements as there are names.

vite.config.ts

@@ -3,6 +3,9 @@ import react from '@vitejs/plugin-react-swc'
 import { viteStaticCopy } from 'vite-plugin-static-copy'
 import svgr from "vite-plugin-svgr"
 
+const backendPort = process.env.PORT || 8080;
+const clientPort = process.env.CLIENT_PORT || 3000;
+
 // https://vitejs.dev/config/
 export default defineConfig({
   //root: 'client/src',
@@ -28,24 +31,25 @@ export default defineConfig({
     })
   ],
   publicDir: "client/public",
+  base: "/", // setting this to `/leangame/` means the server is now accessible at `localhost:3000/leangame`
   optimizeDeps: {
     exclude: ['games']
   },
   server: {
-    port: 3000,
+    port: Number(clientPort),
     proxy: {
       '/websocket': {
-        target: 'ws://localhost:8080',
+        target: `ws://localhost:${backendPort}`,
         ws: true
       },
       '/import': {
-        target: 'http://localhost:8080',
+        target: `http://localhost:${backendPort}`,
       },
       '/data': {
-        target: 'http://localhost:8080',
+        target: `http://localhost:${backendPort}`,
       },
       '/i18n': {
-        target: 'http://localhost:8080',
+        target: `http://localhost:${backendPort}`,
       },
     }
   },