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/i18next-scanner.config.cjs

@@ -0,0 +1,152 @@
+const lean4gameConfig = require("./src/config.json")
+
+const typescriptTransform = require('i18next-scanner-typescript');
+
+const fs = require('fs');
+const chalk = require('chalk');
+const eol = require('eol');
+const path = require('path');
+const VirtualFile = require('vinyl');
+
+function flush(done) {
+  const { parser } = this;
+  const { options } = parser;
+
+  // Flush to resource store
+  const resStore = parser.get({ sort: options.sort });
+  const { jsonIndent } = options.resource;
+  const lineEnding = String(options.resource.lineEnding).toLowerCase();
+
+  Object.keys(resStore).forEach((lng) => {
+    const namespaces = resStore[lng];
+
+    Object.keys(namespaces).forEach((ns) => {
+      const resPath = parser.formatResourceSavePath(lng, ns);
+      let resContent;
+      try {
+        resContent = JSON.parse(
+          fs.readFileSync(
+            fs.realpathSync(path.join('public', 'locales', resPath))
+          ).toString('utf-8')
+        );
+      } catch (e) {
+        console.log("no previous translation found!")
+        resContent = {};
+      }
+      const obj = { ...namespaces[ns], ...resContent };
+      let text = JSON.stringify(obj, null, jsonIndent) + '\n';
+
+      if (lineEnding === 'auto') {
+        text = eol.auto(text);
+      } else if (lineEnding === '\r\n' || lineEnding === 'crlf') {
+        text = eol.crlf(text);
+      } else if (lineEnding === '\n' || lineEnding === 'lf') {
+        text = eol.lf(text);
+      } else if (lineEnding === '\r' || lineEnding === 'cr') {
+        text = eol.cr(text);
+      } else { // Defaults to LF
+        text = eol.lf(text);
+      }
+
+      let contents = null;
+
+      try {
+        // "Buffer.from(string[, encoding])" is added in Node.js v5.10.0
+        contents = Buffer.from(text);
+      } catch (e) {
+        // Fallback to "new Buffer(string[, encoding])" which is deprecated since Node.js v6.0.0
+        contents = new Buffer(text);
+      }
+
+      this.push(new VirtualFile({
+        path: resPath,
+        contents: contents
+      }));
+    });
+  });
+
+  done();
+}
+
+
+module.exports = {
+  input: [
+    'client/src/**/*.{tsx,ts}',
+    // Use ! to filter out files or directories
+    '!client/i18n/**',
+    '!**/node_modules/**',
+  ],
+  options: {
+    debug: true,
+    removeUnusedKeys: true,
+    func: {
+      list: ['i18next.t', 'i18n.t', 't'],
+      extensions: ['.js', '.jsx'] // not .ts or .tsx since we use i18next-scanner-typescript!
+    },
+    trans: {
+      component: 'Trans',
+      i18nKey: 'i18nKey',
+      defaultsKey: 'defaults',
+      extensions: ['.js', '.jsx'], // not .ts or .tsx since we use i18next-scanner-typescript!
+      fallbackKey: (ns, value) => {return value},
+
+      // https://react.i18next.com/latest/trans-component#usage-with-simple-html-elements-like-less-than-br-greater-than-and-others-v10.4.0
+      supportBasicHtmlNodes: true, // Enables keeping the name of simple nodes (e.g. <br/>) in translations instead of indexed keys.
+      keepBasicHtmlNodesFor: ['br', 'strong', 'i', 'p'], // Which nodes are allowed to be kept in translations during defaultValue generation of <Trans>.
+
+      // // https://github.com/acornjs/acorn/tree/master/acorn#interface
+      // acorn: {
+      //     ecmaVersion: 2020,
+      //     sourceType: 'module', // defaults to 'module'
+      // }
+    },
+    lngs: lean4gameConfig.languages.map(e => e.iso),
+    ns: [],
+    defaultLng: 'en',
+    defaultNs: 'translation',
+    defaultValue: (lng, ns, key) => {
+      if (lng === 'en') {
+        return key; // Use key as value for base language
+      }
+      return ''; // Return empty string for other languages
+    },
+    resource: {
+      loadPath: './client/public/locales/{{lng}}/{{ns}}.json',
+      savePath: './client/public/locales/{{lng}}/{{ns}}.json',
+      jsonIndent: 2,
+      lineEnding: '\n'
+    },
+    nsSeparator: false, // namespace separator
+    keySeparator: false, // key separator
+    plurals: false,
+    interpolation: {
+      prefix: '{{',
+      suffix: '}}'
+    },
+    metadata: {},
+    allowDynamicKeys: false,
+  },
+
+  transform: typescriptTransform(
+    // options
+    {
+      // default value for extensions
+      extensions: [".ts", ".tsx"],
+      // optional ts configuration
+      tsOptions: {
+        target: "es2017",
+      },
+    },
+
+    function(outputText, file, enc, done) {
+      'use strict';
+      const parser = this.parser;
+
+      parser.parseTransFromString(outputText);
+      parser.parseFuncFromString(outputText);
+
+      done();
+    }
+  ),
+
+};

client/public/locales/de/translation.json

@@ -0,0 +1,99 @@
+{
+  "Tactics": "Taktiken",
+  "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": "Level",
+  "tactics": "Taktiken",
+  "regular": "regulär",
+  "relaxed": "relaxed",
+  "none": "keine",
+  "Rules": "Regeln",
+  "Intro": "Prolog",
+  "Game Introduction": "Prolog",
+  "World selection": "Übersicht",
+  "Start": "Start",
+  "Inventory": "Inventar",
+  "next level": "nächstes Level",
+  "Next": "Weiter",
+  "back to world selection": "Zurück zur Übersicht",
+  "Leave World": "Welt verlassen",
+  "previous level": "voheriges Level",
+  "Previous": "Zurück",
+  "Editor mode is enforced!": "Editor kann nicht verlassen werden!",
+  "Editor mode": "Editor",
+  "Typewriter mode": "Schreibmaschine",
+  "information, Impressum, privacy policy": "Informationen, Impressum, Privacy Policy",
+  "Preferences": "Einstellungen",
+  "Game Info & Credits": "Spielinfo & Credits",
+  "Game Info": "Spielinfo",
+  "Clear Progress": "Spielstand löschen",
+  "Erase": "Löschen",
+  "Download Progress": "Spielstand herunterladen",
+  "Download": "Herunterladen",
+  "Load Progress from JSON": "Spielstand aus JSON laden",
+  "Upload": "Laden",
+  "Home": "Home",
+  "back to games selection": "Zurück zur Spielauswahl",
+  "close inventory": "Inventar schließen",
+  "show inventory": "Inventar öffnen",
+  "World": "Welt",
+  "Show more help!": "Mehr Hilfe",
+  "Goal": "Beweisziel",
+  "Current Goal": "Aktuelles Beweisziel",
+  "Objects": "Objekte",
+  "Assumptions": "Annahmen",
+  "Further Goals": "Weitere Ziele",
+  "No Goals": "Keine Beweisziele",
+  "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 den Lean-Server …",
+  "Level completed! 🎉": "Level gelöst! 🎉",
+  "Level completed with warnings 🎭": "Level mit Warnungen abgeschlossen 🎭",
+  "Active Goal": "Aktuelles Ziel",
+  "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…": "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 aus einem lokalen Ordner zu laden.",
+  "Prerequisites": "Voraussetzungen",
+  "Worlds": "Welten",
+  "Levels": "Level",
+  "Language": "Sprache",
+  "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",
+  "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 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>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",
+  "Introduction": "Prolog",
+  "Retry proof from here": "Ab hier neu ansetzen",
+  "Retry": "Noch einmal",
+  "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

@@ -0,0 +1,99 @@
+{
+  "Tactics": "Tactics",
+  "Lean Game Server": "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>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": "Game Rules",
+  "levels": "levels",
+  "tactics": "tactics",
+  "regular": "regular",
+  "relaxed": "relaxed",
+  "none": "none",
+  "Rules": "Rules",
+  "Intro": "Intro",
+  "Game Introduction": "Game Introduction",
+  "World selection": "World selection",
+  "Start": "Start",
+  "Inventory": "Inventory",
+  "next level": "next level",
+  "Next": "Next",
+  "back to world selection": "back to world selection",
+  "Leave World": "Leave World",
+  "previous level": "previous level",
+  "Previous": "Previous",
+  "Editor mode is enforced!": "Editor mode is enforced!",
+  "Editor mode": "Editor mode",
+  "Typewriter mode": "Typewriter mode",
+  "information, Impressum, privacy policy": "information, Impressum, privacy policy",
+  "Preferences": "Preferences",
+  "Game Info & Credits": "Game Info & Credits",
+  "Game Info": "Game Info",
+  "Clear Progress": "Clear Progress",
+  "Erase": "Erase",
+  "Download Progress": "Download Progress",
+  "Download": "Download",
+  "Load Progress from JSON": "Load Progress from JSON",
+  "Upload": "Upload",
+  "Home": "Home",
+  "back to games selection": "back to games selection",
+  "close inventory": "close inventory",
+  "show inventory": "show inventory",
+  "World": "World",
+  "Show more help!": "Show more help!",
+  "Goal": "Goal",
+  "Current Goal": "Current Goal",
+  "Objects": "Objects",
+  "Assumptions": "Assumptions",
+  "Further Goals": "Further Goals",
+  "No Goals": "No Goals",
+  "Loading goal…": "Loading goal…",
+  "Click somewhere in the Lean file to enable the infoview.": "Click somewhere in the Lean file to enable the infoview.",
+  "Waiting for Lean server to start…": "Waiting for Lean server to start…",
+  "Level completed! 🎉": "Level completed! 🎉",
+  "Level completed with warnings 🎭": "Level completed with warnings 🎭",
+  "Active Goal": "Active Goal",
+  "Crashed! Go to editor mode and fix your proof! Last server response:": "Crashed! Go to editor mode and fix your proof! Last server response:",
+  "Line": "Line",
+  "Character": "Character",
+  "Loading messages…": "Loading messages…",
+  "Execute": "Execute",
+  "Definitions": "Definitions",
+  "Theorems": "Theorems",
+  "Not unlocked yet": "Not unlocked yet",
+  "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.",
+  "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",
+  "<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>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 Progress?",
+  "Delete": "Delete",
+  "Download & Delete": "Download & Delete",
+  "Cancel": "Cancel",
+  "Layout": "Layout",
+  "Always visible": "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>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": "Upload Saved Progress",
+  "Load selected file": "Load selected file",
+  "Mobile": "Mobile",
+  "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>",
+  "Level": "Level",
+  "Introduction": "Introduction",
+  "Retry proof from here": "Retry proof from here",
+  "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>": "<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

@@ -0,0 +1,99 @@
+{
+  "Tactics": "策略",
+  "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>",
+  "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.": "单击 Lean 文件中的某处以启用信息视图。",
+  "Waiting for Lean server to start…": "等待 Lean 服务器启动中…",
+  "Level completed! 🎉": "关卡完成！🎉",
+  "Level completed with warnings 🎭": "关卡完成（带有警告） 🎭",
+  "Retry proof from here": "从这里重新尝试证明",
+  "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</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> 从本地文件夹打开游戏。",
+  "<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>",
+  "Prerequisites": "前置条件",
+  "Worlds": "世界",
+  "Levels": "关卡",
+  "Language": "语言",
+  "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": "桌面端",
+  "Level": "关卡",
+  "Introduction": "介绍",
+  "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.": "",
+  "Server capacity": "",
+  "RAM": "",
+  " used": "",
+  "CPU": ""
+}

client/src/app.tsx

@@ -10,6 +10,7 @@ import './css/reset.css';
 import './css/app.css';
 import { PreferencesContext} from './components/infoview/context';
 import UsePreferences from "./state/hooks/use_preferences"
+import i18n from './i18n';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
@@ -18,13 +19,19 @@ function App() {
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo
 
-  const {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences} = UsePreferences()
+  const {mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = UsePreferences()
+
+  React.useEffect(() => {
+    i18n.changeLanguage(language)
+  }, [language])
 
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-          <PreferencesContext.Provider value={{mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}}>
+          <PreferencesContext.Provider value={{mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage}}>
+            <React.Suspense>
               <Outlet />
+            </React.Suspense>
           </PreferencesContext.Provider>
       </GameIdContext.Provider>
     </div>

client/src/components/app_bar.tsx

@@ -5,7 +5,7 @@ import * as React from 'react'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
   faArrowRight, faArrowLeft, faXmark, faBars, faCode,
-  faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons'
+  faCircleInfo, faTerminal, faGear } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
 import { InputModeContext, PreferencesContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
@@ -13,22 +13,24 @@ import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress }
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { Button } from './button'
 import { downloadProgress } from './popup/erase'
+import { useTranslation } from 'react-i18next'
 
 /** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */
 function MobileNavButtons({pageNumber, setPageNumber}:
   { pageNumber: number,
     setPageNumber: any}) {
   const gameId = React.useContext(GameIdContext)
+  const { t } = useTranslation()
   const dispatch = useAppDispatch()
 
   // if `prevText` or `prevIcon` is set, show a button to go back
-  let prevText  = {0: null, 1: "Intro", 2: null}[pageNumber]
+  let prevText  = {0: null, 1: t("Intro"), 2: null}[pageNumber]
   let prevIcon  = {0: null, 1: null, 2: faBookOpen}[pageNumber]
-  let prevTitle = {0: null, 1: "Game Introduction", 2: "World selection"}[pageNumber]
+  let prevTitle = {0: null, 1: t("Game Introduction"), 2: t("World selection")}[pageNumber]
   // if `nextText` or `nextIcon` is set, show a button to go forward
-  let nextText  = {0: "Start", 1: null, 2: null}[pageNumber]
+  let nextText  = {0: t("Start"), 1: null, 2: null}[pageNumber]
   let nextIcon  = {0: null, 1: faBook, 2: null}[pageNumber]
-  let nextTitle = {0: "World selection", 1: "Inventory", 2: null}[pageNumber]
+  let nextTitle = {0: t("World selection"), 1: t("Inventory"), 2: null}[pageNumber]
 
   return <>
     {(prevText || prevIcon) &&
@@ -53,7 +55,7 @@ function MobileNavButtons({pageNumber, setPageNumber}:
 }
 
 /** button to toggle dropdown menu. */
-function MenuButton({navOpen, setNavOpen}) {
+export function MenuButton({navOpen, setNavOpen}) {
   return <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}}>
     {navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
   </Button>
@@ -63,18 +65,19 @@ function MenuButton({navOpen, setNavOpen}) {
  * for the last level, this button turns into a button going back to the welcome page.
  */
 function NextButton({worldSize, difficulty, completed, setNavOpen}) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
   return (levelId < worldSize ?
     <Button inverted="true"
-        to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
+        to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title={t("next level")}
         disabled={difficulty >= 2 && !(completed || levelId == 0)}
         onClick={() => setNavOpen(false)}>
-      <FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? "Next" : "Start"}
+      <FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? t("Next") : t("Start")}
     </Button>
     :
-    <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
+    <Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
-      <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
+      <FontAwesomeIcon icon={faHome} />&nbsp;{t("Leave World")}
     </Button>
   )
 }
@@ -83,56 +86,106 @@ function NextButton({worldSize, difficulty, completed, setNavOpen}) {
  * only renders if the current level id is > 0.
  */
 function PreviousButton({setNavOpen}) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
   return (levelId > 0 && <>
     <Button disabled={levelId <= 0} inverted="true"
         to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
-        title="previous level"
+        title={t("previous level")}
         onClick={() => setNavOpen(false)}>
-      <FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
+      <FontAwesomeIcon icon={faArrowLeft} />&nbsp;{t("Previous")}
     </Button>
   </>)
 }
 
 /** button to toggle between editor and typewriter */
 function InputModeButton({setNavOpen, isDropdown}) {
+  const { t } = useTranslation()
   const {levelId} = React.useContext(WorldLevelIdContext)
-  const {typewriterMode, setTypewriterMode, lockInputMode} = React.useContext(InputModeContext)
+  const {typewriterMode, setTypewriterMode, lockEditorMode} = React.useContext(InputModeContext)
 
   /** toggle input mode if allowed */
   function toggleInputMode(ev: React.MouseEvent) {
-    if (!lockInputMode){
+    if (!lockEditorMode){
       setTypewriterMode(!typewriterMode)
       setNavOpen(false)
     }
   }
 
   return <Button
-      className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockInputMode}
+      className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockEditorMode}
       inverted="true" to=""
       onClick={(ev) => toggleInputMode(ev)}
-      title={lockInputMode ? "Editor mode is enforced!" : typewriterMode ? "Editor mode" : "Typewriter mode"}>
+      title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")}>
-    <FontAwesomeIcon icon={typewriterMode ? faCode : faTerminal} />
+    <FontAwesomeIcon icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal} />
-    {isDropdown && (typewriterMode ? <>&nbsp;Editor mode</> : <>&nbsp;Typewriter mode</>)}
+    {isDropdown && ((typewriterMode && !lockEditorMode) ? <>&nbsp;{t("Editor mode")}</> : <>&nbsp;{t("Typewriter mode")}</>)}
   </Button>
 }
 
-/** button to toggle iimpressum popup */
+/** button to toggle iimpressum popup
-function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
+ *
-  return <Button className="btn btn-inverted toggle-width"
+ * Note: Do not translate the word "Impressum"! German GDPR needs this.
-    title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
+*/
+export function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
+  const { t } = useTranslation()
+  return <Button className="btn btn-inverted"
+    title={t("information, Impressum, privacy policy")} inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
     <FontAwesomeIcon icon={faCircleInfo} />
-    {isDropdown && <>&nbsp;Info &amp; Impressum</>}
+    {isDropdown && <>&nbsp;Impressum</>}
+  </Button>
+}
+
+export function PreferencesButton({setNavOpen, togglePreferencesPopup}) {
+  const { t } = useTranslation()
+  return <Button title={t("Preferences")} inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
+    <FontAwesomeIcon icon={faGear} />&nbsp;{t("Preferences")}
+  </Button>
+}
+
+function GameInfoButton({setNavOpen, toggleInfo}) {
+  const { t } = useTranslation()
+  return <Button className="btn btn-inverted"
+    title={t("Game Info & Credits")} inverted="true" to="" onClick={() => {toggleInfo(); setNavOpen(false)}}>
+    <FontAwesomeIcon icon={faCircleInfo} />&nbsp;{t("Game Info")}
+  </Button>
+}
+
+function EraseButton ({setNavOpen, toggleEraseMenu}) {
+  const { t } = useTranslation()
+  return <Button title={t("Clear Progress")} inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
+    <FontAwesomeIcon icon={faEraser} />&nbsp;{t("Erase")}
+  </Button>
+}
+
+function DownloadButton ({setNavOpen, gameId, gameProgress}) {
+  const { t } = useTranslation()
+  return <Button title={t("Download Progress")} inverted="true" to="" onClick={(ev) => {downloadProgress(gameId, gameProgress, ev); setNavOpen(false)}}>
+    <FontAwesomeIcon icon={faDownload} />&nbsp;{t("Download")}
+  </Button>
+}
+
+function UploadButton ({setNavOpen, toggleUploadMenu}) {
+  const { t } = useTranslation()
+  return <Button title={t("Load Progress from JSON")} inverted="true" to="" onClick={() => {toggleUploadMenu(); setNavOpen(false)}}>
+    <FontAwesomeIcon icon={faUpload} />&nbsp;{t("Upload")}
   </Button>
 }
 
 /**  button to go back to welcome page */
 function HomeButton({isDropdown}) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
-  return <Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
+  return <Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
     <FontAwesomeIcon icon={faHome} />
-    {isDropdown && <>&nbsp;Home</>}
+    {isDropdown && <>&nbsp;{t("Home")}</>}
+  </Button>
+}
+
+function LandingPageButton() {
+  const { t } = useTranslation()
+  return <Button inverted="false" title={t("back to games selection")} to="/">
+    <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
     </Button>
 }
 
@@ -140,9 +193,10 @@ function HomeButton({isDropdown}) {
  * only displays a button if `setPageNumber` is set.
  */
 function InventoryButton({pageNumber, setPageNumber}) {
+  const { t } = useTranslation()
   return (setPageNumber &&
     <Button to="" className="btn btn-inverted toggle-width"
-      title={pageNumber ? "close inventory" : "show inventory"}
+      title={pageNumber ? t("close inventory") : t("show inventory")}
       inverted="true" onClick={() => {setPageNumber(pageNumber ? 0 : 1)}}>
       <FontAwesomeIcon icon={pageNumber ? faBookOpen : faBook} />
     </Button>
@@ -160,6 +214,7 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
   toggleInfo: any,
   togglePreferencesPopup: () => void;
 }) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const gameProgress = useAppSelector(selectProgress(gameId))
   const {mobile} = React.useContext(PreferencesContext)
@@ -167,49 +222,38 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
 
   return <div className="app-bar">
     <div className='app-bar-left'>
-      <Button inverted="false" title="back to games selection" to="/">
+      <LandingPageButton />
-        <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
-      </Button>
       <span className="app-bar-title"></span>
     </div>
     <div>
-      {!mobile && <span className="app-bar-title">{gameInfo?.title}</span>}
+      {!mobile && <span className="app-bar-title">{t(gameInfo?.title, {ns: gameId})}</span>}
     </div>
     <div className="nav-btns">
       {mobile && <MobileNavButtons pageNumber={pageNumber} setPageNumber={setPageNumber} />}
       <MenuButton navOpen={navOpen} setNavOpen={setNavOpen} />
     </div>
     <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
-      <Button title="Game Info & Credits" inverted="true" to="" onClick={() => {toggleInfo(); setNavOpen(false)}}>
+      <GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
-        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Game Info
+      <EraseButton setNavOpen={setNavOpen} toggleEraseMenu={toggleEraseMenu}/>
-      </Button>
+      <DownloadButton setNavOpen={setNavOpen} gameId={gameId} gameProgress={gameProgress}/>
-      <Button title="Clear Progress" inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
+      <UploadButton setNavOpen={setNavOpen} toggleUploadMenu={toggleUploadMenu}/>
-        <FontAwesomeIcon icon={faEraser} />&nbsp;Erase
+      <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
-      </Button>
+      <PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
-      <Button title="Download Progress" inverted="true" to="" onClick={(ev) => {downloadProgress(gameId, gameProgress, ev); setNavOpen(false)}}>
-        <FontAwesomeIcon icon={faDownload} />&nbsp;Download
-      </Button>
-      <Button title="Load Progress from JSON" inverted="true" to="" onClick={() => {toggleUploadMenu(); setNavOpen(false)}}>
-        <FontAwesomeIcon icon={faUpload} />&nbsp;Upload
-      </Button>
-      <Button title="Impressum, privacy policy" inverted="true" to="" onClick={() => {toggleImpressum(); setNavOpen(false)}}>
-        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Impressum
-      </Button>
-      <Button title="Preferences" inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
-         <FontAwesomeIcon icon={faGear} />&nbsp;Preferences
-       </Button>
     </div>
   </div>
 }
 
 /** the navigation bar in a level */
-export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=undefined, setPageNumber=undefined} : {
+export function LevelAppBar({isLoading, levelTitle, toggleImpressum, toggleInfo, togglePreferencesPopup, pageNumber=undefined, setPageNumber=undefined} : {
   isLoading: boolean,
   levelTitle: string,
   toggleImpressum: any,
+  toggleInfo: any,
+  togglePreferencesPopup: any,
   pageNumber?: number,
   setPageNumber?: any,
 }) {
+  const { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
   const {mobile} = React.useContext(PreferencesContext)
@@ -236,14 +280,16 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
           <PreviousButton setNavOpen={setNavOpen} />
           <HomeButton isDropdown={true} />
           <InputModeButton setNavOpen={setNavOpen} isDropdown={true}/>
+          <GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
           <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
+          <PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
         </div>
       </> :
       <>
         {/* DESKTOP VERSION */}
         <div className='app-bar-left'>
           <HomeButton isDropdown={false} />
-          <span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
+          <span className="app-bar-title">{worldTitle && `${t("World")}: ${t(worldTitle, {ns: gameId})}`}</span>
         </div>
         <div>
           <span className="app-bar-title">{levelTitle}</span>
@@ -252,7 +298,12 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
           <PreviousButton setNavOpen={setNavOpen} />
           <NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
           <InputModeButton setNavOpen={setNavOpen} isDropdown={false}/>
-          <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={false} />
+          <MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
+        </div>
+        <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
+          <GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
+          <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
+          <PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
         </div>
       </>
     }

client/src/components/hints.tsx

@@ -4,22 +4,26 @@ import Markdown from './markdown';
 import { DeletedChatContext, ProofContext } from "./infoview/context";
 import { lastStepHasErrors } from "./infoview/goals";
 import { Button } from "./button";
+import { useTranslation } from "react-i18next";
+import { GameIdContext } from "../app";
 
 /** Plug-in the variable names in a hint. We do this client-side to prepare
  * for i18n in the future. i.e. one should be able translate the `rawText`
  * and have the variables substituted just before displaying.
  */
 function getHintText(hint: GameHint): string {
+  const gameId = React.useContext(GameIdContext)
+  let { t } = useTranslation()
   if (hint.rawText) {
     // Replace the variable names used in the hint with the ones used by the player
     // variable names are marked like `«{g}»` inside the text.
-    return hint.rawText.replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
+    return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
       // `hint.varNames` contains tuples `[oldName, newName]`
       (hint.varNames.find(x => x[0] == v))[1]))
   } else {
     // hints created in the frontend do not have a `rawText`
     // TODO: `hint.text` could be removed in theory.
-    return hint.text
+    return t(hint.text, {ns: gameId})
   }
 }
 
@@ -88,6 +92,8 @@ function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
 
 export function MoreHelpButton({selected=null} : {selected?: number}) {
 
+  const { t } = useTranslation()
+
   const {proof, setProof} = React.useContext(ProofContext)
   const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
 
@@ -113,7 +119,7 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
 
   if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
     return <Button to="" onClick={activateHiddenHints}>
-      Show more help!
+      {t("Show more help!")}
     </Button>
   }
 }

client/src/components/infoview/context.ts

@@ -79,15 +79,18 @@ export interface ProofStateProps {
 export interface IPreferencesContext extends PreferencesState{
   mobile: boolean, // The variables that actually control the page 'layout' can only be changed through layout.
   setLayout: React.Dispatch<React.SetStateAction<PreferencesState["layout"]>>;
-  setIsSavePreferences: React.Dispatch<React.SetStateAction<Boolean>>;
+  setIsSavePreferences: React.Dispatch<React.SetStateAction<PreferencesState["isSavePreferences"]>>;
+  setLanguage: React.Dispatch<React.SetStateAction<PreferencesState["language"]>>;
 }
 
 export const PreferencesContext = React.createContext<IPreferencesContext>({
   mobile: false,
   layout: "auto",
   isSavePreferences: false,
+  language: "en",
   setLayout: () => {},
-  setIsSavePreferences: () => {}
+  setIsSavePreferences: () => {},
+  setLanguage: () => {},
 })
 
 export const WorldLevelIdContext = React.createContext<{
@@ -125,13 +128,13 @@ export const InputModeContext = React.createContext<{
   setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
   typewriterInput: string,
   setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
-  lockInputMode: boolean,
+  lockEditorMode: boolean,
-  setLockInputMode: React.Dispatch<React.SetStateAction<boolean>>,
+  setLockEditorMode: React.Dispatch<React.SetStateAction<boolean>>,
 }>({
   typewriterMode: true,
   setTypewriterMode: () => {},
   typewriterInput: "",
   setTypewriterInput: () => {},
-  lockInputMode: false,
+  lockEditorMode: false,
-  setLockInputMode: () => {},
+  setLockEditorMode: () => {},
 });

client/src/components/infoview/goals.tsx

@@ -14,6 +14,7 @@ import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, Interacti
 import { RpcSessionAtPos } from '@leanprover/infoview/*';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { DiagnosticSeverity } from 'vscode-languageserver-protocol';
+import { useTranslation } from 'react-i18next';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -134,16 +135,12 @@ interface GoalProps {
     typewriter: boolean
 }
 
-interface ProofDisplayProps {
-  proof: string
-}
-
-
 /**
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
     const { goal, filter, showHints, typewriter } = props
+    let { t } = useTranslation()
 
     // TODO: Apparently `goal` can be `undefined`
     if (!goal) {return <></>}
@@ -157,7 +154,7 @@ export const Goal = React.memo((props: GoalProps) => {
             undefined,
         [locs, goal.mvarId])
     const goalLi = <div key={'goal'}>
-        <div className="goal-title">Goal: </div>
+        <div className="goal-title">{t("Goal")}:</div>
         <LocationsContext.Provider value={goalLocs}>
             <InteractiveCode fmt={goal.type} />
         </LocationsContext.Provider>
@@ -170,24 +167,23 @@ export const Goal = React.memo((props: GoalProps) => {
     // const hints = <Hints hints={goal.hints} key={goal.mvarId} />
     const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
     const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
-    const {typewriterMode} = React.useContext(InputModeContext)
 
     return <div>
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
         {filter.reverse && goalLi}
         {! typewriter && objectHyps.length > 0 &&
-            <div className="hyp-group"><div className="hyp-group-title">Objects:</div>
+            <div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div>
             {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
         {!typewriter && assumptionHyps.length > 0 &&
-            <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
+            <div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {/* {typewriter && typewriterMode && <Typewriter />} */}
         {!filter.reverse && goalLi}
         {/* {showHints && hints} */}
     </div>
 })
 
 export const MainAssumptions = React.memo((props: GoalProps2) => {
+  let { t } = useTranslation()
   const { goals, filter } = props
 
   const goal = goals[0]
@@ -202,7 +198,7 @@ export const MainAssumptions = React.memo((props: GoalProps2) => {
       [locs, goal.mvarId])
 
   const goalLi = <div key={'goal'}>
-    <div className="goal-title">Goal: </div>
+    <div className="goal-title">{t("Goal") + ":"}</div>
     <LocationsContext.Provider value={goalLocs}>
       <InteractiveCode fmt={goal.type} />
     </LocationsContext.Provider>
@@ -212,25 +208,26 @@ export const MainAssumptions = React.memo((props: GoalProps2) => {
   const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
 
   return <div id="main-assumptions">
-    <div className="goals-section-title">Current Goal</div>
+    <div className="goals-section-title">{t("Current Goal")}</div>
     {filter.reverse && goalLi}
     { objectHyps.length > 0 &&
-      <div className="hyp-group"><div className="hyp-group-title">Objects:</div>
+      <div className="hyp-group"><div className="hyp-group-title">{t("Objects") + ":"}</div>
       {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
     { assumptionHyps.length > 0 &&
       <div className="hyp-group">
-        <div className="hyp-group-title">Assumptions:</div>
+        <div className="hyp-group-title">{t("Assumptions") + ":"}</div>
         {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
       </div> }
   </div>
 })
 
 export const OtherGoals = React.memo((props: GoalProps2) => {
+  let { t } = useTranslation()
   const { goals, filter } = props
   return <>
     {goals && goals.length > 1 &&
       <div id="other-goals" className="other-goals">
-        <div className="goals-section-title">Further Goals</div>
+        <div className="goals-section-title">{t("Further Goals")}</div>
         {goals.slice(1).map((goal, i) =>
           <details key={i}>
             <summary>
@@ -242,25 +239,6 @@ export const OtherGoals = React.memo((props: GoalProps2) => {
   </>
 })
 
-// TODO: deprecated
-export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
-  const { proof } = props
-  const steps = proof.match(/.+/g)
-  return <>
-    { steps &&
-      <div id="current-proof">
-        <div className="goals-section-title">Proof history</div>
-        <div className="proof-display-wrapper">
-          <div className="proof-display">
-            {steps.map((s) =>
-              <div>{s}</div>
-            )}
-          </div>
-        </div>
-      </div>}
-  </>
-})
-
 interface GoalsProps {
     goals: InteractiveGoalsWithHints
     filter: GoalFilterState

client/src/components/infoview/info.tsx

@@ -13,9 +13,10 @@ import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-i
 import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'
 
 import { AllMessages, lspDiagToInteractive } from './messages'
-import { goalsToString, Goal, MainAssumptions, OtherGoals, ProofDisplay } from './goals'
+import { goalsToString, Goal, MainAssumptions, OtherGoals } from './goals'
 import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api'
 import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from './context'
+import { useTranslation } from 'react-i18next'
 
 // TODO: All about pinning could probably be removed
 type InfoKind = 'cursor' | 'pin'
@@ -87,6 +88,7 @@ interface InfoDisplayContentProps extends PausableProps {
 }
 
 const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
+    let { t } = useTranslation()
     const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props
 
     const hasWidget = userWidgets.length > 0
@@ -131,7 +133,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
           <div>
             { goals && (goals.goals.length > 0
               ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
-              : <div className="goals-section-title">No Goals</div>
+              : <div className="goals-section-title">{t("No Goals")}</div>
             )}
           </div>
         </LocationsContext.Provider>
@@ -150,7 +152,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     {' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false) }}>resume updating</a>
                     {' '}to see information.
                 </span> :
-                <><CircularProgress /><div>Loading goal...</div></>)}
+                <><CircularProgress /><div>{t("Loading goal…")}</div></>)}
         <AllMessages />
         {/* <LocationsContext.Provider value={locs}>
             {goals && goals.goals.length > 1 && <div className="goals-section other-goals">

client/src/components/infoview/infos.tsx

@@ -6,9 +6,11 @@ import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, TextDocumentCo
 import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { DocumentPosition, Keyed, PositionHelpers, useClientNotificationEffect, useClientNotificationState, useEvent, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { Info, InfoProps } from './info';
+import { useTranslation } from 'react-i18next';
 
 /** Manages and displays pinned infos, as well as info for the current location. */
 export function Infos() {
+    let { t } = useTranslation()
     const ec = React.useContext(EditorContext);
 
     // Update pins when the document changes. In particular, when edits are made
@@ -126,6 +128,6 @@ export function Infos() {
 
     return <div>
         {infoProps.map (ps => <Info {...ps} />)}
-        {!curPos && <p>Click somewhere in the Lean file to enable the infoview.</p> }
+        {!curPos && <p>{t("Click somewhere in the Lean file to enable the infoview.")}</p> }
     </div>;
 }

client/src/components/infoview/main.tsx

@@ -20,7 +20,7 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 
 import { GameIdContext } from '../../app';
 import { useAppDispatch, useAppSelector } from '../../hooks';
-import { LevelInfo } from '../../state/api';
+import { LevelInfo, useGetGameInfoQuery } from '../../state/api';
 import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress';
 import Markdown from '../markdown';
 
@@ -37,15 +37,18 @@ import { store } from '../../state/store';
 import { Hints, MoreHelpButton, filterHints } from '../hints';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { DiagnosticSeverity } from 'vscode-languageclient';
+import { useTranslation } from 'react-i18next';
+import path from 'path';
+
 
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
  * always present, or the monaco editor cannot start.
  */
 export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize }) {
   const ec = React.useContext(EditorContext)
-  const { typewriterMode } = React.useContext(InputModeContext)
+  const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
   return <>
-    <div className={typewriterMode ? 'hidden' : ''}>
+    <div className={(typewriterMode && !lockEditorMode) ? 'hidden' : ''}>
       <ExerciseStatement data={level} showLeanStatement={true} />
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
@@ -61,7 +64,7 @@ export function DualEditor({ level, codeviewRef, levelId, worldId, worldSize })
 function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: string, levelId: number, level: LevelInfo, worldSize: number }) {
   const ec = React.useContext(EditorContext)
   const gameId = React.useContext(GameIdContext)
-  const { typewriterMode } = React.useContext(InputModeContext)
+  const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
 
   const {proof, setProof} = React.useContext(ProofContext)
 
@@ -111,7 +114,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
         <WithRpcSessions>
           <WithLspDiagnosticsContext>
             <ProgressContext.Provider value={allProgress}>
-              {typewriterMode ?
+              {(typewriterMode && !lockEditorMode) ?
                 <TypewriterInterfaceWrapper world={worldId} level={levelId} data={level} worldSize={worldSize}/>
                 :
                 <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} data={level} />
@@ -133,12 +136,15 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
  * If `showLeanStatement` is true, it will additionally display the lean code.
  */
 function ExerciseStatement({ data, showLeanStatement = false }) {
+  let { t } = useTranslation()
+  const gameId = React.useContext(GameIdContext)
+
   if (!(data?.descrText || data?.descrFormat)) { return <></> }
   return <>
     <div className="exercise-statement">
       {data?.descrText &&
         <Markdown>
-          {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : '') + data?.descrText}
+          {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})}
         </Markdown>
       }
       {data?.descrFormat && showLeanStatement &&
@@ -151,6 +157,7 @@ function ExerciseStatement({ data, showLeanStatement = false }) {
 // TODO: This is only used in `EditorInterface`
 // while `TypewriterInterface` has this copy-pasted in.
 export function Main(props: { world: string, level: number, data: LevelInfo}) {
+  let { t } = useTranslation()
   const ec = React.useContext(EditorContext);
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
@@ -228,14 +235,14 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
   // that we want to persist.
   let ret
   if (!serverVersion) {
-    ret = <p>Waiting for Lean server to start...</p>
+    ret = <p>{t("Waiting for Lean server to start…")}</p>
   } else if (serverStoppedResult) {
     ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
   } else {
     ret = <div className="infoview vscode-light">
       {proof?.completedWithWarnings &&
         <div className="level-completed">
-          {proof?.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
+          {proof?.completed ? t("Level completed! 🎉") : t("Level completed with warnings 🎭")}
         </div>
       }
       <Infos />
@@ -260,6 +267,8 @@ const goalFilter = {
 
 /** The display of a single entered lean command */
 function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) {
+  let {t} = useTranslation()
+
   // The first step will always have an empty command
   if (!proof?.steps[i]?.command) { return <></> }
 
@@ -267,13 +276,13 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
     // If the last step has errors, we display the command in a different style
     // indicating that it will be removed on the next try.
     return <div className="failed-command">
-      <i>Failed command</i>: {proof?.steps[i].command}
+      <i>{t("Failed command")}</i>: {proof?.steps[i].command}
     </div>
   } else {
     return <div className="command">
       <div className="command-text">{proof?.steps[i].command}</div>
-      <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
+      <Button to="" className="undo-button btn btn-inverted" title={t("Retry proof from here")} onClick={deleteProof}>
-        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
+        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;{t("Retry")}
       </Button>
     </div>
   }
@@ -332,7 +341,7 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
 
 /** The tabs of goals that lean ahs after the command of this step has been processed */
 function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
-
+  let { t } = useTranslation()
   const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
 
   if (proofStep.goals.length == 0) {
@@ -344,7 +353,7 @@ function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofSte
       {proofStep.goals.map((goal, i) => (
         // TODO: Should not use index as key.
         <div key={`proof-goal-${i}`} className={`tab ${i == (selectedGoal) ? "active" : ""}`} onClick={(ev) => { onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}>
-          {i ? `Goal ${i + 1}` : "Active Goal"}
+          {i ? t("Goal") + ` ${i + 1}` : t("Active Goal")}
         </div>
       ))}
     </div>
@@ -389,12 +398,18 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number
 
 /** The interface in command line mode */
 export function TypewriterInterface({props}) {
+  let { t } = useTranslation()
   const ec = React.useContext(EditorContext)
   const gameId = React.useContext(GameIdContext)
   const editor = React.useContext(MonacoEditorContext)
   const model = editor.getModel()
   const uri = model.uri.toString()
 
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+  const {worldId, levelId} = React.useContext(WorldLevelIdContext)
+  let image: string = gameInfo.data?.worlds.nodes[worldId].image
+
+
   const [disableInput, setDisableInput] = React.useState<boolean>(false)
   const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
   const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
@@ -423,6 +438,9 @@ export function TypewriterInterface({props}) {
       })
       setDeletedChat(deletedChat)
 
+      // delete showHelp for deleted steps
+      setShowHelp(new Set(Array.from(showHelp).filter(i => i < line - 1)))
+
       editor.executeEdits("typewriter", [{
         range: monaco.Selection.fromPositions(
           { lineNumber: line, column: 1 },
@@ -492,13 +510,21 @@ export function TypewriterInterface({props}) {
   return <div className="typewriter-interface">
     <RpcContext.Provider value={rpcSess}>
     <div className="content">
+      <div className='world-image-container empty'>
+        {image &&
+          <img className="contain" src={path.join("data", gameId, image)} alt="" />
+        }
+
+      </div>
       <div className="tmp-pusher">
+        {/* <div className="world-image-container empty">
+
+        </div> */}
       </div>
       <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
         {crashed ? <div>
-          <p className="crashed_message">Crashed! Go to editor mode and fix your proof!
+          <p className="crashed_message">{t("Crashed! Go to editor mode and fix your proof! Last server response:")}</p>
-          Last server response:</p>
           {interimDiags.map(diag => {
             const severityClass = diag.severity ? {
               [DiagnosticSeverity.Error]: 'error',
@@ -509,7 +535,7 @@ export function TypewriterInterface({props}) {
 
             return <div>
               <div className={`${severityClass} ml1 message`}>
-                <p className="mv2">Line {diag.range.start.line}, Character {diag.range.start.character}</p>
+                <p className="mv2">{t("Line")}&nbsp;{diag.range.start.line}, {t("Character")}&nbsp;{diag.range.start.character}</p>
                 <pre className="font-code pre-wrap">
                   {diag.message}
                 </pre>
@@ -576,7 +602,7 @@ export function TypewriterInterface({props}) {
               <div className="button-row mobile">
                 {props.level >= props.worldSize ?
                   <Button to={`/${gameId}`}>
-                    <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
+                    <FontAwesomeIcon icon={faHome} />&nbsp;{t("Leave World")}
                   </Button>
                 :
                   <Button to={`/${gameId}/world/${props.world}/level/${props.level + 1}`}>

client/src/components/infoview/messages.tsx

@@ -11,6 +11,7 @@ import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/
 import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'
 
 import { InputModeContext } from './context'
+import { useTranslation } from 'react-i18next'
 
 interface MessageViewProps {
     uri: DocumentUri;
@@ -79,7 +80,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         message = diag.message
     }
 
-    const { typewriterMode } = React.useContext(InputModeContext)
+    const { typewriterMode, lockEditorMode } = React.useContext(InputModeContext)
 
     return (
     // <details open>
@@ -98,7 +99,7 @@ const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
         //     </span>
         // </summary>
         <div className={severityClass + ' ml1 message'}>
-            {!typewriterMode && <p className="mv2">{title}</p>}
+            {!(typewriterMode && !lockEditorMode) && <p className="mv2">{title}</p>}
             <pre className="font-code pre-wrap">
                 <InteractiveMessage fmt={message} />
             </pre>
@@ -202,6 +203,7 @@ export function AllMessages() {
 
 /** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */
 function AllMessagesBody({uri, curPos, messages}: {uri: DocumentUri, curPos: DocumentPosition | undefined , messages: () => Promise<InteractiveDiagnostic[]>}) {
+    let { t } = useTranslation()
     const [msgs, setMsgs] = React.useState<InteractiveDiagnostic[] | undefined>(undefined)
     React.useEffect(() => { void messages().then(
         msgs => setMsgs(msgs.filter(
@@ -212,7 +214,7 @@ function AllMessagesBody({uri, curPos, messages}: {uri: DocumentUri, curPos: Doc
                 return d.range.start.line == curPos.line
             }))
     ) }, [messages, curPos])
-    if (msgs === undefined) return <div>Loading messages...</div>
+    if (msgs === undefined) return <div>{t("Loading messages…")}</div>
     else return <MessagesList uri={uri} messages={msgs}/>
 }
 

client/src/components/infoview/typewriter.tsx

@@ -20,15 +20,13 @@ import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview
 import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext } from './context'
 import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
 import { GameHint, ProofState } from './rpc_api'
+import { useTranslation } from 'react-i18next'
 
 export interface GameDiagnosticsParams {
   uri: DocumentUri;
   diagnostics: Diagnostic[];
 }
 
-
-
-
 /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
 
 // register Monaco languages
@@ -73,6 +71,7 @@ monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 /** The input field */
 export function Typewriter({disabled}: {disabled?: boolean}) {
+  let { t } = useTranslation()
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
@@ -94,102 +93,6 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
 
   const rpcSess = React.useContext(RpcContext)
 
-  /** Load all goals an messages of the current proof (line-by-line) and save
-   * the retrieved information into context (`ProofContext`)
-   */
-  // const loadAllGoals = React.useCallback(() => {
-
-  //   let goalCalls = []
-  //   let msgCalls = []
-
-  //   // For each line of code ask the server for the goals and the messages on this line
-  //   for (let i = 0; i < model.getLineCount(); i++) {
-  //     goalCalls.push(
-  //       rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
-  //     )
-  //     msgCalls.push(
-  //       getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}).catch((error) => {console.debug("promise broken")})
-  //     )
-  //   }
-
-  //   // Wait for all these requests to be processed before saving the results
-  //   Promise.all(goalCalls).then((steps : InteractiveGoalsWithHints[]) => {
-  //     Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
-  //       let tmpProof : ProofStep[] = []
-
-  //       let goalCount = 0
-
-  //       steps.map((goals, i) => {
-  //         // The first step has an empty command and therefore also no error messages
-  //         // Usually there is a newline at the end of the editors content, so we need to
-  //         // display diagnostics from potentally two lines in the last step.
-  //         let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
-
-  //         // Filter out the 'unsolved goals' message
-  //         messages = messages.filter((msg) => {
-  //           return !("append" in msg.message &&
-  //             "text" in msg.message.append[0] &&
-  //             msg.message.append[0].text === "unsolved goals")
-  //         })
-
-  //         if (typeof goals == 'undefined') {
-  //           tmpProof.push({
-  //             command: i ? model.getLineContent(i) : '',
-  //             goals: [],
-  //             hints: [],
-  //             errors: messages
-  //           } as ProofStep)
-  //           console.debug('goals is undefined')
-  //           return
-  //         }
-
-  //         // If the number of goals reduce, show a message
-  //         if (goals.length && goalCount > goals.length) {
-  //           messages.unshift({
-  //             range: {
-  //               start: {
-  //                 line: i-1,
-  //                 character: 0,
-  //               },
-  //               end: {
-  //                 line: i-1,
-  //                 character: 0,
-  //               }},
-  //             severity: DiagnosticSeverity.Information,
-  //             message: {
-  //             text: 'intermediate goal solved 🎉'
-  //             }
-  //           })
-  //         }
-  //         goalCount = goals.length
-
-  //         // with no goals there will be no hints.
-  //         let hints : GameHint[] = goals.length ? goals[0].hints : []
-
-  //         console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
-  //         console.debug(`Goals: (${i}): `, goalsToString(goals)) //
-  //         console.debug(`Hints: (${i}): `, hints)
-  //         console.debug(`Errors: (${i}): `, messages)
-
-  //         tmpProof.push({
-  //           // the command of the line above. Note that `getLineContent` starts counting
-  //           // at `1` instead of `zero`. The first ProofStep will have an empty command.
-  //           command: i ? model.getLineContent(i) : '',
-  //           // TODO: store correct data
-  //           goals: goals.map(g => g.goal),
-  //           // only need the hints of the active goals in chat
-  //           hints: hints,
-  //           // errors and messages from the server
-  //           errors: messages
-  //         } as ProofStep)
-
-  //       })
-  //       // Save the proof to the context
-  //       setProof(tmpProof)
-  //     }).catch((error) => {console.debug("promise broken")})
-  //   }).catch((error) => {console.debug("promise broken")})
-  // }, [editor, rpcSess, uri, model])
-
   // Run the command
   const runCommand = React.useCallback(() => {
     if (processing) {return}
@@ -355,7 +258,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
           <div ref={inputRef} className="typewriter-input" />
         </div>
         <button type="submit" disabled={processing} className="btn btn-inverted">
-          <FontAwesomeIcon icon={faWandMagicSparkles} /> Execute
+          <FontAwesomeIcon icon={faWandMagicSparkles} />&nbsp;{t("Execute")}
         </button>
       </form>
     </div>

client/src/components/inventory.tsx

@@ -10,6 +10,8 @@ import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadIn
 import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';
 import { useSelector } from 'react-redux';
+import { useTranslation } from 'react-i18next';
+import { t } from 'i18next';
 
 export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
   {
@@ -19,20 +21,21 @@ export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=
     setLemmaTab: any,
     enableAll?: boolean,
   }) {
+  const { t } = useTranslation()
 
   return (
     <div className="inventory">
     {/* TODO: Click on Tactic: show info
       TODO: click on paste icon -> paste into command line */}
-      <h2>Tactics</h2>
+      <h2>{t("Tactics")}</h2>
       {levelInfo?.tactics &&
         <InventoryList items={levelInfo?.tactics} docType="Tactic" openDoc={openDoc} enableAll={enableAll}/>
       }
-      <h2>Definitions</h2>
+      <h2>{t("Definitions")}</h2>
       {levelInfo?.definitions &&
         <InventoryList items={levelInfo?.definitions} docType="Definition" openDoc={openDoc} enableAll={enableAll}/>
       }
-      <h2>Theorems</h2>
+      <h2>{t("Theorems")}</h2>
       {levelInfo?.lemmas &&
         <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
       }
@@ -100,8 +103,8 @@ function InventoryItem({item, name, displayName, locked, disabled, newly, showDo
   const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
   // Note: This is somewhat a hack as the statement of lemmas comes currently in the form
   // `Namespace.statement_name (x y : Nat) : some type`
-  const title = locked ? "Not unlocked yet" :
+  const title = locked ? t("Not unlocked yet") :
-                disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
+                disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
 
   const [copied, setCopied] = useState(false)
 
@@ -137,7 +140,7 @@ export function Documentation({name, type, handleClose}) {
     <h1 className="doc">{doc.data?.displayName}</h1>
     <p><code>{doc.data?.statement}</code></p>
     {/* <code>docstring: {doc.data?.docstring}</code> */}
-    <Markdown>{doc.data?.content}</Markdown>
+    <Markdown>{t(doc.data?.content, {ns: gameId})}</Markdown>
   </div>
 }
 

client/src/components/landing_page.tsx

@@ -1,5 +1,6 @@
 import * as React from 'react';
 import { useNavigate, Link } from "react-router-dom";
+import { Trans, useTranslation } from 'react-i18next';
 
 import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
@@ -14,14 +15,11 @@ import {PrivacyPolicyPopup} from './popup/privacy_policy'
 import { GameTile, useGetGameInfoQuery } from '../state/api'
 import path from 'path';
 
-const flag = {
+import { PreferencesPopup } from './popup/preferences';
-  'Dutch': '🇳🇱',
+import { ImpressumButton, MenuButton, PreferencesButton } from './app_bar';
-  'English': '🇬🇧',
+import ReactCountryFlag from 'react-country-flag';
-  'French': '🇫🇷',
+import lean4gameConfig from '../config.json'
-  'German': '🇩🇪',
+import i18next from 'i18next';
-  'Italian': '🇮🇹',
-  'Spanish': '🇪🇸',
-}
 
 function GithubIcon({url='https://github.com'}) {
 
@@ -35,7 +33,7 @@ function GithubIcon({url='https://github.com'}) {
 }
 
 function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
-
+  let { t } = useTranslation()
   let navigate = useNavigate();
   const routeChange = () =>{
     navigate(gameId);
@@ -47,29 +45,36 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
 
   return <div className="game" onClick={routeChange}>
     <div className="wrapper">
-      <div className="title">{data.title}</div>
+      <div className="title">{t(data.title, { ns: gameId })}</div>
-      <div className="short-description">{data.short}
+      <div className="short-description">{t(data.short, { ns: gameId })}
       </div>
       { data.image ? <img className="image" src={path.join("data", gameId, data.image)} alt="" /> : <div className="image"/> }
-      <div className="long description"><Markdown>{data.long}</Markdown></div>
+      <div className="long description"><Markdown>{t(data.long, { ns: gameId })}</Markdown></div>
     </div>
     <table className="info">
       <tbody>
       <tr>
-        <td title="consider playing these games first.">Prerequisites</td>
+        <td title="consider playing these games first.">{t("Prerequisites")}</td>
-        <td><Markdown>{data.prerequisites.join(', ')}</Markdown></td>
+        <td><Markdown>{t(data.prerequisites.join(', '), { ns: gameId })}</Markdown></td>
       </tr>
       <tr>
-        <td>Worlds</td>
+        <td>{t("Worlds")}</td>
         <td>{data.worlds}</td>
       </tr>
       <tr>
-        <td>Levels</td>
+        <td>{t("Levels")}</td>
         <td>{data.levels}</td>
       </tr>
       <tr>
-        <td>Language</td>
+        <td>{t("Language")}</td>
-        <td title={`in ${data.languages.join(', ')}`}>{data.languages.map((lan) => flag[lan]).join(', ')}</td>
+
+        <td>
+          {data.languages.map((lang) => {
+            let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang)
+            return <ReactCountryFlag key={`flag-${lang}`} title={langOpt?.name} countryCode={langOpt?.flag} className="emojiFlag"/>
+
+          })}
+        </td>
       </tr>
       </tbody>
     </table>
@@ -81,84 +86,78 @@ function LandingPage() {
 
   const navigate = useNavigate();
 
-  const [impressum, setImpressum] = React.useState(false);
+  const [impressumPopup, setImpressumPopup] = React.useState(false);
-  const openImpressum = () => setImpressum(true);
+  const [preferencesPopup, setPreferencesPopup] = React.useState(false);
-  const closeImpressum = () => setImpressum(false);
+  const [navOpen, setNavOpen] = React.useState(false);
+  const openImpressum = () => setImpressumPopup(true);
+  const closeImpressum = () => setImpressumPopup(false);
+  const toggleImpressum = () => setImpressumPopup(!impressumPopup);
+  const closePreferencesPopup = () => setPreferencesPopup(false);
+  const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup);
 
-  // const [allGames, setAllGames] = React.useState([])
+  const [usageCPU, setUsageCPU] = React.useState<number>()
-  // const [allTiles, setAllTiles] = React.useState([])
+  const [usageMem, setUsageMem] = React.useState<number>()
 
-  // const getTiles=()=>{
+  const { t, i18n } = useTranslation()
-  //   fetch('featured_games.json', {
+
-  //     headers : {
+  // Load the namespaces of all games
-  //       'Content-Type': 'application/json',
+  // TODO: should `allGames` contain game-ids starting with `g/`?
-  //       'Accept': 'application/json'
+  i18next.loadNamespaces(lean4gameConfig.allGames.map(id => `g/${id}`))
+
+  let allTiles = lean4gameConfig.allGames.map((gameId) => {
+    let q =  useGetGameInfoQuery({game: `g/${gameId}`})
+
+    // if (q.isError) {
+    //   if (q.error?.originalStatus === 404) {
+    //     // Handle 404 error
+    //     console.log('File not found');
+    //   } else {
+    //     // Suppress additional console.error messages
+    //     console.error(q.error);
     //   }
     // }
-  //   ).then(function(response){
-  //     return response.json()
-  //   }).then(function(data) {
-  //     setAllGames(data.featured_games)
 
-  //   })
+    return q.data?.tile
-  // }
+  })
 
-  // React.useEffect(()=>{
+  /** Parse `games/stats.csv` if present and display server capacity. */
-  //   getTiles()
+  React.useEffect(() => {
-  // },[])
+    const interval = setInterval(() => {
-
+      fetch_stats();
-  // React.useEffect(()=>{
+    }, 2000)
-
+    return () => clearInterval(interval)
-  //   Promise.allSettled(
+  }, [])
-  //     allGames.map((gameId) => (
-  //       fetch(`data/g/${gameId}/game.json`).catch(err => {return undefined})))
-  //   ).then(responses =>
-  //     responses.forEach((result) => console.log(result)))
-  //   //   Promise.all(responses.map(res => {
-  //   //     if (res.status == "fulfilled") {
-  //   //       console.log(res.value.json())
-  //   //       return res.value.json()
-  //   //     } else {
-  //   //       return undefined
-  //   //     }
-  //   //   }))
-  //   // ).then(allData => {
-  //   //   setAllTiles(allData.map(data => data?.tile))
-  //   // })
-  // },[allGames])
-
-  // TODO: I would like to read the supported games list form a JSON,
-  // Then load all these games in
-  //
-  let allGames = [
-    "leanprover-community/nng4",
-    "hhu-adam/robo",
-    "djvelleman/stg4",
-    "miguelmarco/stg4",
-    "trequetrum/lean4game-logic",
-  ]
-  let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
 
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
-      <nav>
+      <nav className="landing-page-nav">
         <GithubIcon url="https://github.com/leanprover-community/lean4game"/>
+        <MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
+        <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
+            <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
+            <PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
+        </div>
       </nav>
       <div id="main-title">
-        <h1>Lean Game Server</h1>
+        <h1>{t("Lean Game Server")}</h1>
         <p>
+          <Trans>
             A repository of learning games for the
             proof assistant <a target="_blank" href="https://leanprover-community.github.io/">Lean</a> <i>(Lean 4)</i> and
             its mathematical library <a target="_blank" href="https://github.com/leanprover-community/mathlib4">mathlib</a>
+          </Trans>
         </p>
       </div>
     </header>
     <div className="game-list">
-      {allTiles.length == 0 ?
+      {allTiles.filter(x => x != null).length == 0 ?
-        <p>No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
+        <p>
+          <Trans>
+            No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
             game directly from a local folder.
+          </Trans>
         </p>
-        : allGames.map((id, i) => (
+        : lean4gameConfig.allGames.map((id, i) => (
           <Tile
             key={id}
             gameId={`g/${id}`}
@@ -167,24 +166,40 @@ function LandingPage() {
         ))
       }
     </div>
+    { // show server capacity from `games/stats.csv` if present
+      (usageMem >= 0 || usageCPU >= 0 ) &&
       <section>
         <div className="wrapper">
-        <h2>Development notes</h2>
+          <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.
-          We hope to address and test this limitation better in the future.
             </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>
             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
             any problems you experience!
           </p>
+        </Trans>
       </div>
     </section>
     <section>
       <div className="wrapper">
-        <h2>Adding new games</h2>
+        <h2>{t("Adding new games")}</h2>
+        <Trans>
           <p>
             If you are considering writing your own game, you should use
             the <a target="_blank" href="https://github.com/hhu-adam/GameSkeleton">GameSkeleton Github Repo</a> as
@@ -199,26 +214,56 @@ function LandingPage() {
           </p>
           <p>
             Featured games on this page are added manually.
-          Please get in contact and we-ll happily add yours.
+            Please get in contact and we'll happily add yours.
           </p>
+        </Trans>
       </div>
     </section>
     <section>
       <div className="wrapper">
-        <h2>Funding</h2>
+        <h2>{t("Funding")}</h2>
         <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
-          Heinrich-Heine-Universität in Düsseldorf.
+            Heinrich Heine University Düsseldorf.
+          </Trans>
         </p>
       </div>
     </section>
     <footer>
+      {/* Do not translate "Impressum", it's needed for German GDPR */}
       <a className="link" onClick={openImpressum}>Impressum</a>
-      {impressum? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
+      {impressumPopup? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
+      {preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
     </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/components/level.tsx

@@ -51,6 +51,10 @@ import { IConnectionProvider } from 'monaco-languageclient'
 import { monacoSetup } from 'lean4web/client/src/monacoSetup'
 import { onigasmH } from 'onigasm/lib/onigasmH'
 import { isLastStepWithErrors, lastStepHasErrors } from './infoview/goals'
+import { InfoPopup } from './popup/game_info'
+import { PreferencesPopup } from './popup/preferences'
+import { useTranslation } from 'react-i18next'
+import i18next from 'i18next'
 
 
 monacoSetup()
@@ -60,21 +64,39 @@ function Level() {
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
 
-  const [impressum, setImpressum] = React.useState(false)
+  const gameId = React.useContext(GameIdContext)
 
-  const closeImpressum = () => {
+  // Load the namespace of the game
-    setImpressum(false)
+  i18next.loadNamespaces(gameId).catch(err => {
-  }
+    console.warn(`translations for ${gameId} do not exist.`)
+  })
+
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+
+  // pop-ups
+  const [impressum, setImpressum] = React.useState(false)
+  const [info, setInfo] = React.useState(false)
+  const [preferencesPopup, setPreferencesPopup] = React.useState(false)
+
+  function closeImpressum()   {setImpressum(false)}
+  function closeInfo()        {setInfo(false)}
+  function closePreferencesPopup() {setPreferencesPopup(false)}
+  function toggleImpressum()  {setImpressum(!impressum)}
+  function toggleInfo()       {setInfo(!info)}
+  function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
 
   return <WorldLevelIdContext.Provider value={{worldId, levelId}}>
     {levelId == 0 ?
-      <Introduction impressum={impressum} setImpressum={setImpressum} /> :
+      <Introduction impressum={impressum} setImpressum={setImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup} /> :
-      <PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} />}
+      <PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>}
     {impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
+    {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
+    {preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
   </WorldLevelIdContext.Provider>
 }
 
 function ChatPanel({lastLevel, visible = true}) {
+  let { t } = useTranslation()
   const chatRef = useRef<HTMLDivElement>(null)
   const {mobile} = useContext(PreferencesContext)
   const gameId = useContext(GameIdContext)
@@ -121,7 +143,7 @@ function ChatPanel({lastLevel, visible = true}) {
   //   // chatRef.current!.scrollTo(0,0)
   // }, [gameId, worldId, levelId])
 
-  let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
+  let introText: Array<string> = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/)
 
   return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
     <div ref={chatRef} className="chat">
@@ -153,11 +175,11 @@ function ChatPanel({lastLevel, visible = true}) {
       {proof?.completed &&
         <>
           <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
-            Level completed! 🎉
+            {t("Level completed! 🎉")}
           </div>
           {level?.data?.conclusion?.trim() &&
             <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
-              <Markdown>{level?.data?.conclusion}</Markdown>
+              <Markdown>{t(level?.data?.conclusion, {ns: gameId})}</Markdown>
             </div>
           }
         </>
@@ -166,10 +188,10 @@ function ChatPanel({lastLevel, visible = true}) {
     <div className="button-row">
       {proof?.completed && (lastLevel ?
         <Button to={`/${gameId}`}>
-          <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
+          <FontAwesomeIcon icon={faHome} />&nbsp;{t("Leave World")}
         </Button> :
         <Button to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
-          Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+          {t("Next")}&nbsp;<FontAwesomeIcon icon={faArrowRight} />
         </Button>)
         }
       <MoreHelpButton />
@@ -190,7 +212,8 @@ function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableR
   </div>
 }
 
-function PlayableLevel({impressum, setImpressum}) {
+function PlayableLevel({impressum, setImpressum, toggleInfo, togglePreferencesPopup}) {
+  let { t } = useTranslation()
   const codeviewRef = useRef<HTMLDivElement>(null)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
@@ -222,7 +245,7 @@ function PlayableLevel({impressum, setImpressum}) {
   const [pageNumber, setPageNumber] = useState(0)
 
   // set to true to prevent switching between typewriter and editor
-  const [lockInputMode, setLockInputMode] = useState(false)
+  const [lockEditorMode, setLockEditorMode] = useState(false)
   const [typewriterInput, setTypewriterInput] = useState("")
   const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
 
@@ -282,10 +305,11 @@ function PlayableLevel({impressum, setImpressum}) {
   // a hint at the beginning of the proof...
   const [selectedStep, setSelectedStep] = useState<number>()
 
+
   useEffect (() => {
     // Lock editor mode
     if (level?.data?.template) {
-      setTypewriterMode(false)
+      setLockEditorMode(true)
 
       if (editor) {
         let code = editor.getModel().getLinesContent()
@@ -312,6 +336,8 @@ function PlayableLevel({impressum, setImpressum}) {
           console.debug(`not inserting template.`)
         }
       }
+    } else {
+      setLockEditorMode(false)
     }
   }, [level, levelId, worldId, gameId, editor])
 
@@ -326,7 +352,7 @@ function PlayableLevel({impressum, setImpressum}) {
   }, [gameId, worldId, levelId])
 
   useEffect(() => {
-    if (!typewriterMode && editor) {
+    if (!(typewriterMode && !lockEditorMode) && editor) {
       // Delete last input attempt from command line
       editor.executeEdits("typewriter", [{
         range: editor.getSelection(),
@@ -335,7 +361,7 @@ function PlayableLevel({impressum, setImpressum}) {
       }]);
       editor.focus()
     }
-  }, [typewriterMode])
+  }, [typewriterMode, lockEditorMode])
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
@@ -355,7 +381,7 @@ function PlayableLevel({impressum, setImpressum}) {
 
   // Effect when command line mode gets enabled
   useEffect(() => {
-    if (onigasmH && editor && typewriterMode) {
+    if (onigasmH && editor && (typewriterMode && !lockEditorMode)) {
       let code = editor.getModel().getLinesContent().filter(line => line.trim())
       editor.executeEdits("typewriter", [{
         range: editor.getModel().getFullModelRange(),
@@ -378,22 +404,25 @@ function PlayableLevel({impressum, setImpressum}) {
       //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
       // }
     }
-  }, [editor, typewriterMode, onigasmH == null])
+  }, [editor, typewriterMode, lockEditorMode, onigasmH == null])
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
       <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
-        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockInputMode, setLockInputMode}}>
+        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode}}>
           <ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>
                 <LevelAppBar
                   pageNumber={pageNumber} setPageNumber={setPageNumber}
                   isLoading={level.isLoading}
-                  levelTitle={`${mobile ? '' : 'Level '}${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
+                  levelTitle={(mobile ? "" : t("Level")) + ` ${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
-                    (level?.data?.title && ` : ${level?.data?.title}`)}
+                    (level?.data?.title && ` : ${t(level?.data?.title, {ns: gameId})}`)}
-                  toggleImpressum={toggleImpressum} />
+                  toggleImpressum={toggleImpressum}
+                  toggleInfo={toggleInfo}
+                  togglePreferencesPopup={togglePreferencesPopup}
+                  />
                 {mobile?
                   // TODO: This is copied from the `Split` component below...
                   <>
@@ -422,11 +451,12 @@ function PlayableLevel({impressum, setImpressum}) {
 }
 
 function IntroductionPanel({gameInfo}) {
+  let { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
   const {mobile} = React.useContext(PreferencesContext)
 
-  let text: Array<string> = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/)
+  let text: Array<string> = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/)
 
   return <div className="chat-panel">
     <div className="chat">
@@ -439,7 +469,7 @@ function IntroductionPanel({gameInfo}) {
       {gameInfo.data?.worldSize[worldId] == 0 ?
         <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
         <Button to={`/${gameId}/world/${worldId}/level/1`}>
-          Start&nbsp;<FontAwesomeIcon icon={faArrowRight} />
+          {t("Start")}&nbsp;<FontAwesomeIcon icon={faArrowRight} />
         </Button>
       }
     </div>
@@ -449,7 +479,9 @@ function IntroductionPanel({gameInfo}) {
 export default Level
 
 /** The site with the introduction text of a world */
-function Introduction({impressum, setImpressum}) {
+function Introduction({impressum, setImpressum, toggleInfo, togglePreferencesPopup}) {
+  let { t } = useTranslation()
+
   const gameId = React.useContext(GameIdContext)
   const {mobile} = useContext(PreferencesContext)
 
@@ -467,7 +499,7 @@ function Introduction({impressum, setImpressum}) {
   }
 
   return <>
-    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" toggleImpressum={toggleImpressum}/>
+    <LevelAppBar isLoading={gameInfo.isLoading} levelTitle={t("Introduction")} toggleImpressum={toggleImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
     {gameInfo.isLoading ?
       <div className="app-content loading"><CircularProgress /></div>
     : mobile ?
@@ -475,10 +507,9 @@ function Introduction({impressum, setImpressum}) {
       :
         <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
           <IntroductionPanel gameInfo={gameInfo} />
-          <div className="world-image-container empty">
+          <div className="world-image-container empty center">
             {image &&
-              // TODO: Temporary for testing
+              <img className="contain" src={path.join("data", gameId, image)} alt="" />
-              <img className={worldId=="Proposition" ? "cover" : "contain"} src={path.join("data", gameId, image)} alt="" />
             }
 
           </div>

client/src/components/popup/erase.tsx

@@ -8,6 +8,7 @@ import { useAppDispatch } from '../../hooks'
 import { deleteProgress, selectProgress } from '../../state/progress'
 import { downloadFile } from '../world_tree'
 import { Button } from '../button'
+import { Trans, useTranslation } from 'react-i18next'
 
 /** download the current progress (i.e. what's saved in the browser store) */
 export function downloadProgress(gameId: string, gameProgress: any, ev: React.MouseEvent) {
@@ -25,6 +26,7 @@ export function downloadProgress(gameId: string, gameProgress: any, ev: React.Mo
  * controlled by the containing element.
  */
 export function ErasePopup ({handleClose}) {
+  let { t } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const gameProgress = useSelector(selectProgress(gameId))
   const dispatch = useAppDispatch()
@@ -43,17 +45,17 @@ export function ErasePopup ({handleClose}) {
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Delete Progress?</h2>
+    <h2>{t("Delete Progress?")}</h2>
-
+    <Trans>
       <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>
-
+    </Trans>
-    <Button onClick={eraseProgress} to="">Delete</Button>
+    <Button onClick={eraseProgress} to="">{t("Delete")}</Button>
-    <Button onClick={downloadAndErase} to="">Download & Delete</Button>
+    <Button onClick={downloadAndErase} to="">{t("Download & Delete")}</Button>
-    <Button onClick={handleClose} to="">Cancel</Button>
+    <Button onClick={handleClose} to="">{t("Cancel")}</Button>
   </div>
 </div>
 }

client/src/components/popup/game_info.tsx

@@ -4,6 +4,8 @@
 import * as React from 'react'
 import { Typography } from '@mui/material'
 import Markdown from '../markdown'
+import { useTranslation } from 'react-i18next'
+import { GameIdContext } from '../../app'
 
 /** Pop-up that is displaying the Game Info.
  *
@@ -11,12 +13,15 @@ import Markdown from '../markdown'
  * controlled by the containing element.
  */
 export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
+  let { t } = useTranslation()
+  const gameId = React.useContext(GameIdContext)
+
   return <div className="modal-wrapper">
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
     <Typography variant="body1" component="div" className="welcome-text">
-      <Markdown>{info}</Markdown>
+      <Markdown>{t(info, {ns: gameId})}</Markdown>
     </Typography>
   </div>
 </div>

client/src/components/popup/preferences.tsx

@@ -1,34 +1,35 @@
 import * as React from 'react'
-import { Input, Typography } from '@mui/material'
+import { Input, MenuItem, Select, SelectChangeEvent, Typography } from '@mui/material'
 import Markdown from '../markdown'
 import { Switch, Button, ButtonGroup } from '@mui/material';
 import Box from '@mui/material/Box';
 import Slider from '@mui/material/Slider';
+import lean4gameConfig from '../../config.json'
 
 import FormControlLabel from '@mui/material/FormControlLabel';
 
-import { IPreferencesContext } from "../infoview/context"
+import { IPreferencesContext, PreferencesContext } from "../infoview/context"
+import ReactCountryFlag from 'react-country-flag';
+import { useTranslation } from 'react-i18next';
 
-interface PreferencesPopupProps extends Omit<IPreferencesContext, 'mobile'> {
+export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
-    handleClose: () => void
+  let { t } = useTranslation()
-}
+  const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
-
-export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) {
 
   const marks = [
     {
       value: 0,
-            label: 'Mobile',
+      label: t('Mobile'),
       key: "mobile"
     },
     {
       value: 1,
-            label: 'Auto',
+      label: t('Auto'),
       key: "auto"
     },
     {
       value: 2,
-            label: 'Desktop',
+      label: t('Desktop'),
       key: "desktop"
     },
   ];
@@ -37,6 +38,10 @@ export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSa
     setLayout(marks[value].key as IPreferencesContext["layout"])
   }
 
+  const handlerChangeLanguage = (ev: SelectChangeEvent<string>) => {
+    setLanguage(ev.target.value as IPreferencesContext["language"])
+  }
+
   return <div className="modal-wrapper">
     <div className="modal-backdrop" onClick={handleClose} />
     <div className="modal">
@@ -44,14 +49,34 @@ export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSa
       <Typography variant="body1" component="div" className="settings">
         <div className='preferences-category'>
           <div className='category-title'>
-                        <h3>Layout</h3>
+            <h3>{t("Language")}</h3>
+          </div>
+          <div className='preferences-item first leave-left-gap'>
+            <FormControlLabel
+              control={
+                <Box sx={{ width: 300 }}>
+                  <Select
+                    value={language}
+                    label={t("Language")}
+                    onChange={handlerChangeLanguage}>
+                      {lean4gameConfig.languages.map(lang => {return <MenuItem key={`menu-item-lang-${lang.iso}`} value={lang.iso}><ReactCountryFlag countryCode={lang.flag}/>&nbsp;{lang.name}</MenuItem>})}
+                  </Select>
+                </Box>
+              }
+              label=""
+            />
+          </div>
+        </div>
+        <div className='preferences-category'>
+          <div className='category-title'>
+            <h3>{t("Layout")}</h3>
           </div>
           <div className='preferences-item first leave-left-gap'>
             <FormControlLabel
               control={
                 <Box sx={{ width: 300 }}>
                   <Slider
-                                        aria-label="Always visible"
+                    aria-label={t("Always visible")}
                     value={marks.find(item => item.key === layout).value}
                     step={1}
                     marks={marks}
@@ -79,7 +104,7 @@ export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSa
                   color="primary"
                 />
               }
-                            label="Save my settings (in the browser store)"
+              label={t("Save my settings (in the browser store)")}
               labelPlacement="end"
             />
           </div>

client/src/components/popup/privacy_policy.tsx

@@ -9,6 +9,8 @@ import * as React from 'react'
  *
  * `handleClose` is the function to close it again because it's open/closed state is
  * controlled by the containing element.
+ *
+ * Note: Do not translate the Impressum!
  */
 export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
   return <div className="privacy-policy modal-wrapper">
@@ -57,19 +59,3 @@ export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
   </div>
 </div>
 }
-
-export const PrivacyPolicy: React.FC = () => {
-  const [open, setOpen] = React.useState(false)
-  const handleOpen = () => setOpen(true)
-  const handleClose = () => setOpen(false)
-  return (
-    <>
-      <div className="privacy" onClick={handleOpen} title="Privacy Policy &amp; Impressum">
-        <FontAwesomeIcon icon={faShield} />
-        <p className="p1">legal</p>
-        <p className="p2">notes</p>
-      </div>
-      {open ? <PrivacyPolicyPopup handleClose={handleClose} /> : null}
-    </>
-  )
-}

client/src/components/popup/rules_help.tsx

@@ -2,6 +2,7 @@
  * @fileOverview
 */
 import * as React from 'react'
+import { Trans, useTranslation } from 'react-i18next'
 
 /** Pop-up that is displayed when opening the help explaining the game rules.
  *
@@ -9,11 +10,14 @@ import * as React from 'react'
  * controlled by the containing element.
  */
 export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) {
+  const { t } = useTranslation()
+
   return <div className="privacy-policy modal-wrapper">
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Game Rules</h2>
+    <h2>{t("Game Rules")}</h2>
+    <Trans>
       <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.
@@ -24,27 +28,28 @@ export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) {
         if you unlock <code>simp</code> in a level, you can use it henceforth in any level.
       </p>
       <p>The options are:</p>
+    </Trans>
     <table>
       <thead>
         <tr>
           <th scope="col"></th>
-          <th scope="col">levels</th>
+          <th scope="col">{t("levels")}</th>
-          <th scope="col">tactics</th>
+          <th scope="col">{t("tactics")}</th>
         </tr>
       </thead>
       <tbody>
         <tr>
-          <th scope="row">regular</th>
+          <th scope="row">{t("regular")}</th>
           <td>🔐</td>
           <td>🔐</td>
         </tr>
         <tr>
-          <th scope="row">relaxed</th>
+          <th scope="row">{t("relaxed")}</th>
           <td>🔓</td>
           <td>🔐</td>
         </tr>
         <tr>
-          <th scope="row">none</th>
+          <th scope="row">{t("none")}</th>
           <td>🔓</td>
           <td>🔓</td>
         </tr>

client/src/components/popup/upload.tsx

@@ -8,6 +8,7 @@ import { useAppDispatch } from '../../hooks'
 import { GameProgressState, loadProgress, selectProgress } from '../../state/progress'
 import { downloadFile } from '../world_tree'
 import { Button } from '../button'
+import { Trans, useTranslation } from 'react-i18next'
 
 /** Pop-up that is displaying the Game Info.
  *
@@ -15,6 +16,8 @@ import { Button } from '../button'
  * controlled by the containing element.
  */
 export function UploadPopup ({handleClose}) {
+  let { t } = useTranslation()
+
   const [file, setFile] = React.useState<File>();
   const gameId = React.useContext(GameIdContext)
   const gameProgress = useSelector(selectProgress(gameId))
@@ -54,17 +57,19 @@ export function UploadPopup ({handleClose}) {
   <div className="modal-backdrop" onClick={handleClose} />
   <div className="modal">
     <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-    <h2>Upload Saved Progress</h2>
+    <h2>{t("Upload Saved Progress")}</h2>
-
+    <Trans>
       <p>Select a JSON file with the saved game progress to load your progress.</p>
 
       <p><b>Warning:</b> This will delete your current game progress!
-      Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p>
+        Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!
+      </p>
+    </Trans>
     <p>
       <input type="file" onChange={handleFileChange}/>
     </p>
 
-    <Button to="" onClick={uploadProgress}>Load selected file</Button>
+    <Button to="" onClick={uploadProgress}>{t("Load selected file")}</Button>
   </div>
 </div>
 }

client/src/components/welcome.tsx

@@ -23,26 +23,31 @@ import { WorldTreePanel } from './world_tree'
 import '../css/welcome.css'
 import { WelcomeAppBar } from './app_bar'
 import { Hint } from './hints'
+import i18next from 'i18next'
+import { useTranslation } from 'react-i18next'
 
 
 /** the panel showing the game's introduction text */
 function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
   const {mobile} = React.useContext(PreferencesContext)
   const gameId = React.useContext(GameIdContext)
+
+  let { t } = useTranslation()
+
   const dispatch = useAppDispatch()
 
   // TODO: I left the setup for splitting up the introduction in place, but if it's not needed
   // then this can be simplified.
 
   // let text: Array<string> = introduction.split(/\n(\s*\n)+/)
-  let text: Array<string> = introduction ? [introduction] : []
+  let text: Array<string> = introduction ? [t(introduction, {ns : gameId})] : []
 
   return <div className="column chat-panel">
     <div className="chat">
       {text?.map(((t, i) =>
         t.trim() ?
           <Hint key={`intro-p-${i}`}
-            hint={{text: t, hidden: false}}
+            hint={{text: t, hidden: false, rawText: t, varNames: []}}
             step={0} selected={null} toggleSelection={undefined} />
         : <></>
       ))}
@@ -64,8 +69,12 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string,
 /** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)
+
+  // Load the namespace of the game
+  i18next.loadNamespaces(gameId)
+
   const {mobile} = React.useContext(PreferencesContext)
-  const {layout, isSavePreferences, setLayout, setIsSavePreferences} = React.useContext(PreferencesContext)
+  const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
 
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
@@ -94,7 +103,6 @@ function Welcome() {
   function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
   function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
 
-
   // set the window title
   useEffect(() => {
     if (gameInfo.data?.title) {
@@ -136,7 +144,7 @@ function Welcome() {
     {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
     {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
     {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
-    {preferencesPopup ? <PreferencesPopup layout={layout} isSavePreferences={isSavePreferences} setLayout={setLayout} setIsSavePreferences={setIsSavePreferences} handleClose={closePreferencesPopup}/> : null}
+    {preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
   </>
 }
 

client/src/components/world_tree.tsx

@@ -17,6 +17,7 @@ import { store } from '../state/store'
 
 import '../css/world_tree.css'
 import { PreferencesContext } from './infoview/context'
+import { useTranslation } from 'react-i18next'
 
 // Settings for the world tree
 cytoscape.use( klay )
@@ -112,6 +113,7 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
     difficulty: number,
     worldSize: number
   }) {
+  const { t } = useTranslation()
 
   // See level icons. Match radius computed there minus `1.2*r`
   const N = Math.max(worldSize, NMIN)
@@ -150,7 +152,7 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
           width={1.42*R} height={1.42*R} transform={"translate("+ -.71*R +","+ -.71*R +")"}>
         <div className={unlocked && !completed ? "playable-world" : ''}>
           <p className="world-title" style={{fontSize: fontSize + "px"}}>
-            {title ? title : world}
+            {title ? t(title, {ns: gameId}) : world}
           </p>
         </div>
       </foreignObject>
@@ -161,7 +163,7 @@ export function WorldIcon({world, title, position, completedLevels, difficulty,
           >
         <div className='world-label' style={{backgroundColor: completed ? darkgreen : unlocked ? darkblue : darkgrey}}>
           <p className='world-title' style={{fontSize: MINFONT + "px"}}>
-            {title ? title : world}
+            {title ? t(title, {ns: gameId}) : world}
           </p>
         </div>
       </foreignObject>}
@@ -195,6 +197,7 @@ export const downloadFile = ({ data, fileName, fileType } :
 
 /** The menu that is shown next to the world selection graph */
 export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
+  const { t, i18n } = useTranslation()
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
@@ -202,20 +205,20 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
 
 
   function label(x : number) {
-    return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular'
+    return x == 0 ? t("none") : x == 1 ? t("relaxed") : t("regular")
   }
 
 
   return <nav className={`world-selection-menu${mobile ? '' : ' desktop'}`}>
     <div className="slider-wrap">
-      <span className="difficulty-label">Rules
+      <span className="difficulty-label">{t("Rules")}
         <FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
       </span>
       <Slider
         orientation="vertical"
-        title="Game Rules"
+        title={t("Game Rules")}
         min={0} max={2}
-        aria-label="Game Rules"
+        aria-label={t("Game Rules")}
         value={difficulty}
         marks={[
           {value: 0, label: label(0)},

client/src/config.json

@@ -0,0 +1,37 @@
+{
+  "allGames": [
+    "leanprover-community/nng4",
+    "hhu-adam/robo",
+    "djvelleman/stg4",
+    "trequetrum/lean4game-logic",
+    "jadabouhawili/knightsandknaves-lean4game"
+  ],
+
+  "languages": [
+    {
+      "iso": "en",
+      "flag": "GB",
+      "name": "English"
+    },
+    {
+      "iso": "de",
+      "flag": "DE",
+      "name": "Deutsch"
+    },
+    {
+      "iso": "zh",
+      "flag": "CN",
+      "name": "中文"
+    },
+    {
+      "iso": "es",
+      "flag": "ES",
+      "name": "Español"
+    },
+    {
+      "iso": "ko",
+      "flag": "KR",
+      "name": "한국어"
+    }
+  ]
+}

client/src/css/landing_page.css

@@ -19,7 +19,7 @@ a {
 
 @viewport {
   width: device-width ;
-  zoom: 1.0 ;
+  initial-scale: 1.0 ;
 }
 
 .landing-page {
@@ -36,6 +36,13 @@ a {
   padding-bottom: 80px;
 }
 
+.landing-page-nav {
+  position: relative;
+}
+
+#menu-btn {
+  background-color: unset;
+}
 
 @media screen and (max-width: 440px) {
   .game-list {
@@ -182,6 +189,8 @@ footer .link {
 
 .github-link {
   height: 24px; /* TODO: why do I need that? s*/
+  margin-top: auto;
+  margin-bottom: auto;
 }
 
 .landing-page > section {

client/src/css/level.css

@@ -348,13 +348,19 @@ td code  {
 .world-image-container {
   display: flex;
   flex-direction: column;
-  justify-content: center;
+  min-height: 0px; /* somehow this has a desired affect, but why? */
+  overflow: hidden;
 }
 
 .world-image-container img.contain {
   object-fit: contain;
 }
 
+.world-image-container.center {
+  justify-content: center;
+}
+
+
 .world-image-container img.cover {
   height: 100%;
   object-fit: cover;
@@ -369,7 +375,21 @@ td code  {
   text-align: center;
 }
 
+/* Fixes https://github.com/leanprover-community/lean4game/issues/202 */
+.katex-mathml {
+  display: none;
+}
+
 /* DEBUG */
 /* .proof .step {
   border: 2px solid rgb(0, 123, 255);
 } */
+
+.nav-btns {
+  height: 2rem;
+}
+
+.nav-btns .language-btn {
+  background: #DDF6FF;
+  text-align: center;
+}

client/src/i18n.ts

@@ -0,0 +1,35 @@
+import i18n from "i18next";
+import Backend from "i18next-http-backend"
+import { initReactI18next } from "react-i18next";
+
+i18n
+.use(initReactI18next)
+.use(Backend)
+.init({
+    ns: ['translation'],
+    backend: {
+      // > see https://github.com/i18next/i18next-http-backend
+      loadPath: function(lngs, namespaces: Array<string>) {
+        if (namespaces[0].startsWith("g/")) {
+          return '/i18n/{{ns}}/{{lng}}/Game.json';
+        } else {
+          return '/locales/{{lng}}/{{ns}}.json';
+        }
+      }
+    },
+    // > language to use, more information here:
+    // > https://www.i18next.com/overview/configuration-options#languages-namespaces-resources
+    lng: "en",
+    // we use natural language keys, so we don't need a fallback language.
+    fallbackLng: false,
+    // > you can use the i18n.changeLanguage function to change the language manually:
+    // > https://www.i18next.com/overview/api#changelanguage
+    // > if you're using a language detector, do not define the lng option
+    returnEmptyString: false,
+    interpolation: {
+      // > react already safes from xss
+      escapeValue: false
+    }
+  });
+
+  export default i18n;

client/src/index.tsx

@@ -9,6 +9,7 @@ import ErrorPage from './components/error_page'
 import Welcome from './components/welcome'
 import LandingPage from './components/landing_page'
 import Level from './components/level'
+import './i18n';
 
 
 
@@ -19,21 +20,28 @@ let root_object: RouteObject = single_game ? {
   path: "/",
   loader: () => redirect("/g/local/game")
 } : {
+  path: "/",
+  element: <App />,
+  errorElement: <ErrorPage />,
+  children: [
+    {
       path: "/",
       element: <LandingPage />,
     }
+  ]
+}
 
 const router = createHashRouter([
   root_object,
   {
     // 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/hooks/use_preferences.ts

@@ -4,6 +4,7 @@ import {
     PreferencesState,
     setLayout as setPreferencesLayout,
     setIsSavePreferences as setPreferencesIsSavePreferences,
+    setLanguage as setLanguagePreferences,
     getWindowDimensions,
     AUTO_SWITCH_THRESHOLD
 } from "../preferences";
@@ -19,6 +20,9 @@ const UsePreferences = () => {
     const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences);
     const setIsSavePreferences = (isSave: boolean) => dispatch(setPreferencesIsSavePreferences(isSave))
 
+    const language = useAppSelector((state) => state.preferences.language);
+    const setLanguage = (lang: string) => dispatch(setLanguagePreferences(lang))
+
     const automaticallyAdjustLayout = () => {
         const {width} = getWindowDimensions()
         setMobile(width < AUTO_SWITCH_THRESHOLD)
@@ -35,7 +39,7 @@ const UsePreferences = () => {
         }
     }, [layout])
 
-    return {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}
+    return {mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage}
 }
 
 export default UsePreferences;

client/src/state/preferences.ts

@@ -5,6 +5,7 @@ import { loadPreferences, removePreferences, savePreferences } from "./local_sto
 export interface PreferencesState {
   layout: "mobile" | "auto" | "desktop";
   isSavePreferences: boolean;
+  language: string;
 }
 
 export function getWindowDimensions() {
@@ -16,8 +17,9 @@ export const AUTO_SWITCH_THRESHOLD = 800
 
 const initialState: PreferencesState = loadPreferences() ??{
     layout: "auto",
-    isSavePreferences: false
+    isSavePreferences: false,
-}
+    language: import.meta.env.VITE_CLIENT_DEFAULT_LANGUAGE || "en",
+};
 
 export const preferencesSlice = createSlice({
   name: "preferences",
@@ -29,7 +31,10 @@ export const preferencesSlice = createSlice({
     setIsSavePreferences: (state, action) => {
       state.isSavePreferences = action.payload;
     },
+    setLanguage: (state, action) => {
+      state.language = action.payload;
+    },
   },
 });
 
-export const { setLayout, setIsSavePreferences } = preferencesSlice.actions;
+export const { setLayout, setIsSavePreferences, setLanguage } = preferencesSlice.actions;

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$. -/
@@ -202,36 +202,7 @@ Statement ...
   sorry
 ```
 
-#### Local `let` definitions
+For more details and features, read [Writing Exercises](writing_exercises.md)
-
-If you want to make a local definition/notation which only holds for this exercise (e.g.
-a function `f : ℤ → ℤ := fun x ↦ 2 * x`) the recommended way is to use a `let`-statement:
-
-```lean
-Statement (a : ℤ) (h : 0 < a) :
-    let f : ℤ → ℤ := fun x ↦ 2 * x
-    0 < f a := by
-  sorry
-```
-
-The game automatically `intros` such `let`-statements, such that you and the player will see
-the following initial proof state:
-
-```
-a: ℤ
-h: 0 < a
-f: ℤ → ℤ := fun x => 2 * x
-⊢ 0 < f a
-```
-
-#### Attributes
-
-You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:
-
-```lean
-@[simp]
-Statement my_simp_lemma ...
-```
 
 ### 6. c) Proof
 
@@ -271,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)
 
@@ -290,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,
+
+### LaTeX support
+
+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.

doc/writing_exercises.md

@@ -0,0 +1,56 @@
+# Writing exercises
+
+This page deals in more details with the `Statement` command and all the options you have
+to write better exercises/levels.
+
+
+## Local `let` definitions
+
+If you want to make a local definition/notation which only holds for this exercise (e.g.
+a function `f : ℤ → ℤ := fun x ↦ 2 * x`) the recommended way is to use a `let`-statement:
+
+```lean
+Statement (a : ℤ) (h : 0 < a) :
+    let f : ℤ → ℤ := fun x ↦ 2 * x
+    0 < f a := by
+  sorry
+```
+
+The game automatically `intros` such `let`-statements, such that you and the player will see
+the following initial proof state:
+
+```
+a: ℤ
+h: 0 < a
+f: ℤ → ℤ := fun x => 2 * x
+⊢ 0 < f a
+```
+
+## "Preamble" & non-`Prop`-valued exercises
+
+You can use the following syntax with `(preamble := tac)` where `tac` is a tactic sequence.
+
+```
+Statement my_statement (preamble := dsimp) (a : ℤ) (h : 0 < a) :
+    0 < f a := by
+  sorry
+```
+
+This tactic sequence will be executed before the exercise is handed to the player.
+
+For example, if your exercise is to construct a structure, you could use `preamble` to fill
+all data fields correctly, leaving all `Prop`-valued fields of the structure as separate goals
+for the player to proof.
+
+Note: `(preamble := tac)` always has to be written between the optional name and the first
+hypothesis. Nevertheless, you can use all hypotheses in the tactic sequence, because it is
+only evaluated at the beginning of the proof.
+
+## Attributes
+
+You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:
+
+```lean
+@[simp]
+Statement my_simp_lemma ...
+```

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>

package.json

@@ -27,12 +27,17 @@
     "cytoscape-klay": "^3.1.4",
     "debounce": "^1.2.1",
     "express": "^4.18.2",
+    "i18next": "^23.10.1",
+    "i18next-http-backend": "^2.5.0",
+    "i18next-scanner-typescript": "^1.2.0",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
     "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
     "octokit": "^3.1.2",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",
+    "react-country-flag": "^3.1.0",
     "react-dom": "^18.2.0",
+    "react-i18next": "^14.1.0",
     "react-markdown": "^8.0.4",
     "react-native": "^0.72.3",
     "react-redux": "^8.0.5",
@@ -58,6 +63,7 @@
     "concurrently": "^7.6.0",
     "css-loader": "^6.7.3",
     "file-loader": "^6.2.0",
+    "i18next-scanner": "^4.4.0",
     "nodemon": "^3.0.1",
     "react-refresh": "^0.14.0",
     "style-loader": "^3.3.1",
@@ -73,7 +79,8 @@
     "preview": "vite preview",
     "build_server": "cd server && lake build",
     "build_client": "cross-env NODE_ENV=production vite build",
-    "production": "cross-env NODE_ENV=production node relay/index.mjs"
+    "production": "cross-env NODE_ENV=production node relay/index.mjs",
+    "translate": "npx i18next-scanner --config client/i18next-scanner.config.cjs"
   },
   "eslintConfig": {
     "extends": [

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);
@@ -37,6 +39,30 @@ router.get('/import/trigger/:owner/:repo', importTrigger)
 
 const server = app
   .use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game
+  .use('/i18n/g/:owner/:repo/:lang/*', (req, res, next) => {
+    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);
+  })
   .use('/data/g/:owner/:repo/*', (req, res, next) => {
     const owner = req.params.owner;
     const repo = req.params.repo
@@ -44,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}`));
 
@@ -170,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

@@ -4,10 +4,13 @@ import GameServer.Options
 import GameServer.SaveData
 import GameServer.Hints
 import GameServer.Tactic.LetIntros
+import GameServer.RpcHandlers -- only needed to collect the translations of "level completed" msgs
 import I18n
 
 open Lean Meta Elab Command
 
+open GameServer
+
 set_option autoImplicit false
 
 /-! # Game metadata -/
@@ -40,7 +43,7 @@ elab "Title" t:str : command => do
   | .Level => modifyCurLevel fun level => pure {level with title := title}
   | .World => modifyCurWorld  fun world => pure {world with title := title}
   | .Game => modifyCurGame  fun game => pure {game with
-      title := t.getString
+      title := title
       tile := {game.tile with title := title}}
 
 /-- Define the introduction of the current game/world/level. -/
@@ -108,14 +111,15 @@ elab "CaptionLong" t:str : command => do
   modifyCurGame fun game => pure {game with
     tile := {game.tile with long := caption}}
 
-/-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
+/-- A list of Languages the game is translated to. For example `Languages "de" "en"`.
-NOTE: For the time being, only a single language is supported.
+
+The keys are ISO language codes.
  -/
 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
@@ -341,11 +345,36 @@ elab "LemmaTab"  category:str : command => do
 
 /-! # Exercise Statement -/
 
+/-- You can write `Statement add_comm (preamble := simp) .... := by` which
+will automatically execute the given tactic sequence before the exercise
+is handed to the player.
+
+A common example is to use
+
+```
+refine { carrier := M, ?.. }
+```
+
+in exercises, where the statement is a structure, to fill in all the data fields.
+
+For example in "Show that all matrices with first column zero form a submodule",
+you could provide the set of all these matrices as `carrier` and the player will receive
+all the `Prop`-valued fields as goals.
+-/
+syntax preambleArg := atomic(" (preamble := " withoutPosition(tacticSeq) ")")
+
 /-- Define the statement of the current level. -/
 elab doc:docComment ? attrs:Parser.Term.attributes ?
-    "Statement" statementName:ident ? sig:declSig val:declVal : command => do
+    "Statement" statementName:ident ? preamble:preambleArg ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
+  -- add an optional tactic sequence that the engine executes before the game starts
+  let preambleSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← match preamble with
+  | none => `(Parser.Tactic.tacticSeq|skip)
+  | some x => match x with
+    | `(preambleArg| (preamble := $tac)) => pure tac
+    | _ => `(Parser.Tactic.tacticSeq|skip)
+
   let docContent ← parseDocComment doc
   let docContent ← match docContent with
   | none => pure none
@@ -378,22 +407,24 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     let env ← getEnv
     let fullName := (← getCurrNamespace) ++ name.getId
     if env.contains fullName then
-      let origType := (env.constants.map₁.find! fullName).type
+      let some orig := env.constants.map₁.find? fullName
+        | throwError s!"error in \"Statement\": `{fullName}` not found."
+      let origType := orig.type
       -- TODO: Check if `origType` agrees with `sig` and output `logInfo` instead of `logWarning`
       -- in that case.
       logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
       m!"statement will be available in later levels:\n\n{origType}")
-      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨tacticStx⟩)})
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)})
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
     else
-      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨tacticStx⟩)})
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)})
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
   | none =>
-    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨tacticStx⟩)})
+    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)})
     elabCommand thmStatement
 
   let msgs := (← get).messages
@@ -468,6 +499,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
   modifyCurLevel fun level => pure { level with
     module := env.header.mainModule
     goal := sig,
+    preamble := preambleSeq
     scope := scope,
     descrText := docContent
     statementName := match statementName with
@@ -477,7 +509,8 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     hints := hints
     tactics := {level.tactics with used := usedInventory.tactics.toArray}
     definitions := {level.definitions with used := usedInventory.definitions.toArray}
-    lemmas := {level.lemmas with used := usedInventory.lemmas.toArray} }
+    lemmas := {level.lemmas with used := usedInventory.lemmas.toArray}
+    }
 
 /-! # Hints -/
 
@@ -544,7 +577,8 @@ elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
   -- Show an info whether the branch proofs all remaining goals.
   let gs ← Tactic.getUnsolvedGoals
   if gs.isEmpty then
-    trace[debug] "This branch finishes the proof."
+    -- trace[debug] "This branch finishes the proof."
+    pure ()
   else
     trace[debug] "This branch leaves open goals."
 
@@ -576,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 _ :: [] =>
         []
@@ -708,7 +742,8 @@ elab "MakeGame" : command => do
           | 0 => pure ()
           | 1 => pure () -- level ids start with 1, so we need to skip 1, too
           | i₀ + 1 =>
-            match (world.levels.find! (i₀)).statementName with
+            let some idx := world.levels.find? (i₀) | throwError s!"Level {i₀ + 1} not found for world {worldId}!"
+            match (idx).statementName with
             | .anonymous => pure ()
             | .num _ _ => panic "Did not expect to get a numerical statement name!"
             | .str pre s =>
@@ -719,7 +754,9 @@ elab "MakeGame" : command => do
 
       -- if the last level was named, we need to add it as a new lemma
       let i₀ := world.levels.size
-        match (world.levels.find! (i₀)).statementName with
+
+        let some idx := world.levels.find? (i₀) | throwError s!"Level {i₀} not found for world {worldId}!"
+        match (idx).statementName with
         | .anonymous => pure ()
         | .num _ _ => panic "Did not expect to get a numerical statement name!"
         | .str pre s =>
@@ -841,7 +878,8 @@ elab "MakeGame" : command => do
           | 1 => pure () -- level ids start with 1, so we need to skip 1, too.
           | i₀ + 1 =>
             -- add named statement from previous level to the available lemmas.
-            match (world.levels.find! (i₀)).statementName with
+            let some idx := world.levels.find? (i₀) | throwError s!"Level {i₀ + 1} not found for world {worldId}!"
+            match (idx).statementName with
             | .anonymous => pure ()
             | .num _ _ => panic "Did not expect to get a numerical statement name!"
             | .str pre s =>
@@ -855,7 +893,8 @@ elab "MakeGame" : command => do
         match i₀ with
         | 0 => logWarning m!"World `{worldId}` contains no levels."
         | i₀ =>
-          match (world.levels.find! (i₀)).statementName with
+          let some idx := world.levels.find? (i₀) | throwError s!"Level {i₀} not found for world {worldId}!"
+          match (idx).statementName with
           | .anonymous => pure ()
           | .num _ _ => panic "Did not expect to get a numerical statement name!"
           | .str pre s =>

server/GameServer/EnvExtensions.lean

@@ -30,7 +30,7 @@ The inventory contains documentation that the user can access.
 There are three inventory types: Lemma, Tactic, Definition. They vary about in the information
 they carry.
 
-The commands `LemmaDoc`, `TacticDoc`, and `DefinitionDoc` add keys and templates to an
+The commands `TheoremDoc`, `TacticDoc`, and `DefinitionDoc` add keys and templates to an
 env. extension called `InventoryTemplateExt`. Commands like `NewLemma`, etc. as well as
 `Statement` check if there is a key registered in this extension and might add a default or
 print a warning if not.
@@ -265,6 +265,8 @@ structure GameLevel where
   template: Option String := none
   /-- The image for this level. -/
   image : String := default
+  /-- A sequence of tactics the game automatically executes before the first step. -/
+  preamble : TSyntax `Lean.Parser.Tactic.tacticSeq := default
 deriving Inhabited, Repr
 
 /-- Json-encodable version of `GameLevel`

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
@@ -263,7 +263,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           -- This makes the experience for the user much nicer and allows for local
           -- definitions in the exercise.
           let cmdStx ← `(command|
-            theorem the_theorem $(level.goal) := by {let_intros; $(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preamble⟩); $(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
       cmdCtx cmdStateRef
   let postNew := (← tacticCacheNew.get).post
@@ -331,6 +331,9 @@ structure GameParams where
   diagnostics : GameDiagnostics
 deriving ToJson, FromJson
 
+-- `snap` and `initParams` are unused
+set_option linter.unusedVariables false in
+
 /-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/
 def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) :
     IO Unit := do
@@ -380,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/Helpers.lean

@@ -1,4 +1,5 @@
 import Lean
+import GameServer.Helpers.PrettyPrinter
 
 /-! This document contains various things which cluttered `Commands.lean`. -/
 
@@ -6,6 +7,8 @@ open Lean Meta Elab Command
 
 /-! ## Doc Comment Parsing -/
 
+namespace GameServer
+
 /-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
 def parseDocComment! (doc: Option (TSyntax `Lean.Parser.Command.docComment)) :
     CommandElabM String := do
@@ -59,26 +62,6 @@ def parseDocCommentLegacy (doc: Option (TSyntax `Lean.Parser.Command.docComment)
         and remove the string following it!"
         pure <| ← parseDocComment! doc
 
-/-! ## Statement string -/
-
-def getStatement (name : Name) : CommandElabM MessageData := do
-  return ← addMessageContextPartial (.ofPPFormat { pp := fun
-    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
-    | none     => return "that's a bug." })
-
--- Note: We use `String` because we can't send `MessageData` as json, but
--- `MessageData` might be better for interactive highlighting.
-/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
-
-Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
-`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
-def getStatementString (name : Name) : CommandElabM String := do
-  try
-    return ← (← getStatement name).toString
-  catch
-  | _ => throwError m!"Could not find {name} in context."
-  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.
-
 /-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
 syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 -- TODO

server/GameServer/Helpers/PrettyPrinter.lean

@@ -0,0 +1,93 @@
+--import Lean
+import Lean.PrettyPrinter.Delaborator.Builtins
+import Lean.PrettyPrinter
+import Lean
+
+import Std.Tactic.OpenPrivate
+
+namespace GameServer
+
+namespace PrettyPrinter
+
+open Lean Meta
+open Lean.Parser Term
+open PrettyPrinter Delaborator SubExpr
+open TSyntax.Compat
+
+open private shouldGroupWithNext evalSyntaxConstant from Lean.PrettyPrinter.Delaborator.Builtins
+
+-- def typeSpec := leading_parser " :\\n: " >> termParser
+
+-- def declSig := leading_parser
+--   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> typeSpec
+
+
+@[inherit_doc Lean.PrettyPrinter.Delaborator.delabConstWithSignature]
+partial def delabConstWithSignature : Delab := do
+  let e ← getExpr
+  -- use virtual expression node of arity 2 to separate name and type info
+  let idStx ← descend e 0 <|
+    withOptions (pp.universes.set · true |> (pp.fullNames.set · true)) <|
+      delabConst
+  descend (← inferType e) 1 <|
+    delabParams idStx #[] #[]
+where
+  -- follows `delabBinders`, but does not uniquify binder names and accumulates all binder groups
+  delabParams (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
+    if let .forallE n d _ i ← getExpr then
+      let stxN ← annotateCurPos (mkIdent n)
+      let curIds := curIds.push ⟨stxN⟩
+      if ← shouldGroupWithNext then
+        withBindingBody n <| delabParams idStx groups curIds
+      else
+        let delabTy := withOptions (pp.piBinderTypes.set · false) delab
+        let group ← withBindingDomain do
+          match i with
+          | .implicit       => `(bracketedBinderF|{$curIds*})
+          | .strictImplicit => `(bracketedBinderF|⦃$curIds*⦄)
+          | .instImplicit   => `(bracketedBinderF|[$(← delabTy)])
+          | _ =>
+            if d.isOptParam then
+              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
+            else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
+              let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
+              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
+            else
+              `(bracketedBinderF|($curIds* : $(← delabTy)))
+        withBindingBody n <| delabParams idStx (groups.push group) #[]
+    else
+      let type ← delab
+
+      -- pure type
+      `(Command.declSig| $groups* : $type)
+
+@[inherit_doc Lean.PrettyPrinter.ppSignature]
+def ppSignature (c : Name) : MetaM FormatWithInfos := do
+  let decl ← getConstInfo c
+  let e := .const c (decl.levelParams.map mkLevelParam)
+  let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
+  return ⟨← ppTerm ⟨stx⟩, infos⟩  -- HACK: not a term
+
+end PrettyPrinter
+
+open Lean Meta Elab Command
+
+/-! ## Statement string -/
+
+def getStatement (name : Name) : CommandElabM MessageData := do
+  return ← addMessageContextPartial (.ofPPFormat { pp := fun
+    | some ctx => ctx.runMetaM <| GameServer.PrettyPrinter.ppSignature name
+    | none     => return "that's a bug." })
+
+-- Note: We use `String` because we can't send `MessageData` as json, but
+-- `MessageData` might be better for interactive highlighting.
+/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`.
+
+Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into
+`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/
+def getStatementString (name : Name) : CommandElabM String := do
+  --try
+    return ← (← getStatement name).toString
+  --catch
+  --| _ => throwError m!"Could not find {name} in context."
+  -- TODO: I think it would be nicer to unresolve Namespaces as much as possible.

server/GameServer/RpcHandlers.lean

@@ -1,7 +1,7 @@
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
-import Std.Data.Array.Init.Basic
 import GameServer.Hints
+import I18n
 
 open Lean
 open Server
@@ -171,7 +171,11 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
   if goalCount == 0 then
     if completed then
       out := out.push {
-        message := .text "level completed! 🎉"
+        -- TODO: marking these with `t!` has the implication that every game
+        -- needs to translate these messages again,
+        -- but cannot think of another option
+        -- that would not involve manually adding them somewhere in the translation files.
+        message := .text t!"level completed! 🎉"
         range := {
           start := pos
           «end» := pos
@@ -179,7 +183,7 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
         severity? := Lsp.DiagnosticSeverity.information }
     else if completedWithWarnings then
       out := out.push {
-        message := .text "level completed with warnings… 🎭"
+        message := .text t!"level completed with warnings… 🎭"
         range := {
           start := pos
           «end» := pos
@@ -192,7 +196,7 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
     -- so showing the message "intermediate goal solved" would be confusing.
     if (¬ (filterUnsolvedGoal startDiags).any (·.severity? == some .error)) then
       out := out.push {
-        message := .text "intermediate goal solved! 🎉"
+        message := .text t!"intermediate goal solved! 🎉"
         range := {
           start := pos
           «end» := pos
@@ -227,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/SaveData.lean

@@ -59,8 +59,8 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
 
   IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
 
-  -- write PO file for translation
+  -- write file for translation
-  I18n.createPOTemplate
+  I18n.createTemplate
 
 open GameData
 

server/GameServer/Tactic/LetIntros.lean

@@ -7,6 +7,10 @@ import Lean.Meta.Tactic.Intro
 
 `let_intros` is a weaker form of `intros` aimed to only introduce `let` statements,
 but not for example `∀`-binders.
+
+Note: Mathlib has a tactic `extract_lets` which does essentially exactly this.
+  The only difference is that `let_intros` is unhygenic, in the sense that it will name
+  the introduced variables `f` instead of leaving them inaccessible `f✝`.
 -/
 
 namespace GameServer
@@ -40,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.
@@ -48,8 +52,6 @@ If names are provided, it will introduce as many `let` statements as there are n
 syntax (name := letIntros) "let_intros" : tactic
 -- (ppSpace colGt (ident <|> hole))*
 
-#check letIntros
-
 @[tactic letIntros] def evalLetIntros : Tactic := fun stx => do
   match stx with
   | `(tactic| let_intros) => liftMetaTactic fun mvarId => do

server/lake-manifest.json

@@ -4,19 +4,37 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "v4.7.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/mhuisi/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/hhu-adam/lean-i18n.git",
    "type": "git",
    "subDir": null,
-   "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5",
+   "rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39",
    "name": "i18n",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "v4.7.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "rev": "ac07367cbdd57440e6fe78e5be13b41f9cb0f896",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.7.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lakefile.lean

@@ -4,12 +4,14 @@ open Lake DSL
 package GameServer
 
 -- Using this assumes that each dependency has a tag of the form `v4.X.0`.
--- def leanVersion : String := s!"v{Lean.versionString}"
+def leanVersion : String := s!"v{Lean.versionString}"
-def leanVersion := "v4.6.0" -- TODO
 
 require std from git "https://github.com/leanprover/std4.git" @ leanVersion
 require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion
 
+require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
+
+
 lean_lib GameServer
 
 @[default_target]

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0

server/test/test_statement.lean

@@ -73,10 +73,13 @@ theorem xy (n : Nat) : n + 0 = n := by
 
 /-- Doc comment -/
 @[simp]
-Statement My.add_comm (n m : Nat) : n + m = m + n := by
+Statement My.add_assoc (n m x : Nat) : (m + n) + x = m + (n + x) := by
-  rw [Nat.add_comm]
+  rw [Nat.add_assoc]
 
-example (n m : Nat) : n + m = m + n := by
+example (n m : Nat) : (m + n) + x = m + (n + x) := by
   simp
 
-#check My.add_comm
+#check My.add_assoc
+
+Statement My.add_comm (preamble := simp [add_comm m n]) (n m : Nat) : n + (m + 0) = m + n := by
+  rw [Nat.add_comm]

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,21 +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:${backendPort}`,
       },
     }
   },