npm audit

Update level.css - hide .katex-mathml, to fix scrolling issue

.github/workflows/build.yml

@@ -1,6 +1,8 @@
 name: Build
 run-name: Build the project
-on: [push]
+on:
+  workflow_dispatch:
+  push:
 jobs:
   build:
     runs-on: ubuntu-latest

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,94 @@
+{
+  "Tactics": "Taktiken",
+  "Lean Game Server": "Lean-Spielserver",
+  "<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Die Spielregeln bestimmen ob es erlaubt ist, Levels zu überspringen und ob das Spiel überprüft welche Taktiken und Theoreme freigeschaltet sind und nur diese im Beweis akzeptiert.</p><1>Bemerkung: \"Freigeschaltete\" Taktiken (und Theoreme) werden durch zwei Faktoren bestimmt: The Menge der Taktiken die minimal notwending sind um den Level zu lösen und dazu die Menge aller Taktiken, die in einem anderen Level freigeschaltet wurden. Das bedeutet wenn <1>simp</1> in einem Level freigeschaltet wird, kann diese Taktik danach in jeglichen Levels verwendet werden.",
+  "Game Rules": "Spielregeln",
+  "levels": "Levels",
+  "tactics": "Taktiken",
+  "regular": "regulär",
+  "relaxed": "relaxed",
+  "none": "keine",
+  "Rules": "Regeln",
+  "Intro": "Inführung",
+  "Game Introduction": "Spieleinführung",
+  "World selection": "Weltenauswahl",
+  "Start": "Start",
+  "Inventory": "Inventar",
+  "next level": "nächstes Level",
+  "Next": "Weiter",
+  "back to world selection": "Zurück zur Weltenauswahl",
+  "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 von JSON laden",
+  "Upload": "Laden",
+  "Home": "Home",
+  "back to games selection": "Zurück zur Spielauswahl",
+  "close inventory": "Inventar schliessen",
+  "show inventory": "Inventar öffnen",
+  "World": "Welt",
+  "Show more help!": "Mehr Hilfe",
+  "Goal": "Goal",
+  "Current Goal": "Aktuelles Goal",
+  "Objects": "Objekte",
+  "Assumptions": "Annahmen",
+  "Further Goals": "Weitere Goals",
+  "No Goals": "Keine Goals",
+  "Loading goal…": "Goal wird geladen…",
+  "Click somewhere in the Lean file to enable the infoview.": "Ein Klick in den Lean-Code aktiviert den Infoview.",
+  "Waiting for Lean server to start…": "Warte auf das Starten des Lean-Servers…",
+  "Level completed! 🎉": "Level gelöst! 🎉",
+  "Level completed with warnings 🎭": "Level mit Warnungen abgeschlossen 🎭",
+  "Active Goal": "Aktuelles Goal",
+  "Crashed! Go to editor mode and fix your proof! Last server response:": "",
+  "Line": "Zeile",
+  "Character": "Charakter",
+  "Loading messages…": "",
+  "Execute": "Ausführen",
+  "Definitions": "Definitionen",
+  "Theorems": "Theoreme",
+  "Not unlocked yet": "Noch nicht verfügbar",
+  "Not available in this level": "In diesem Level nicht verfügbar",
+  "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean</1> <i>(Lean 4)</i> und dessen mathematische Bibliothek <5>mathlib</5>",
+  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen. öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt von einem lokalen Ordner zu laden.",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
+  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
+  "Prerequisites": "Voraussetzungen",
+  "Worlds": "Welten",
+  "Levels": "Levels",
+  "Language": "Sprachen",
+  "Development notes": "Entwicklungshinweis",
+  "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 dem Spielstand um diesen zu laden.</p><1><0>Achtung:</0> Diese Aktion überschreibt den aktuellen Spielstand! Es wird empfohlen zuerst den <2>aktuellen Spielstand herunterzuladen</2>!</1>",
+  "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>": "",
+  "Level": "",
+  "Introduction": "",
+  "Retry proof from here": "",
+  "Retry": "",
+  "Failed command": ""
+}

client/public/locales/en/translation.json

@@ -0,0 +1,94 @@
+{
+  "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.",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>",
+  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.",
+  "Prerequisites": "Prerequisites",
+  "Worlds": "Worlds",
+  "Levels": "Levels",
+  "Language": "Language",
+  "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"
+}

client/public/locales/zh/translation.json

@@ -0,0 +1,94 @@
+{
+  "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>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在另一个关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<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": "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>": "",
+  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "没有加载游戏。使用<1>http://localhost:3000/#/g/local/FOLDER</1>直接从本地文件夹打开游戏。",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
+  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
+  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
+  "Prerequisites": "前置条件",
+  "Worlds": "世界(Worlds)",
+  "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": ""
+}

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}}>
-            <Outlet />
+          <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">
-      <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
+    <Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
+      <FontAwesomeIcon icon={faHome} />&nbsp;{t("Leave World")}
     </Button>
   )
 }
@@ -83,66 +86,117 @@ 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"}>
-    <FontAwesomeIcon icon={typewriterMode ? faCode : faTerminal} />
-    {isDropdown && (typewriterMode ? <>&nbsp;Editor mode</> : <>&nbsp;Typewriter mode</>)}
+      title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")}>
+    <FontAwesomeIcon icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal} />
+    {isDropdown && ((typewriterMode && !lockEditorMode) ? <>&nbsp;{t("Editor mode")}</> : <>&nbsp;{t("Typewriter mode")}</>)}
   </Button>
 }
 
-/** button to toggle iimpressum popup */
-function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
-  return <Button className="btn btn-inverted toggle-width"
-    title="information, Impressum, privacy policy" inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
+/** button to toggle iimpressum popup
+ *
+ * Note: Do not translate the word "Impressum"! German GDPR needs this.
+*/
+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>
+}
+
 /** button in mobile level to toggle inventory.
  * 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="/">
-        <FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
-      </Button>
+      <LandingPageButton />
       <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)}}>
-        <FontAwesomeIcon icon={faCircleInfo} />&nbsp;Game Info
-      </Button>
-      <Button title="Clear Progress" inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
-        <FontAwesomeIcon icon={faEraser} />&nbsp;Erase
-      </Button>
-      <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>
+      <GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
+      <EraseButton setNavOpen={setNavOpen} toggleEraseMenu={toggleEraseMenu}/>
+      <DownloadButton setNavOpen={setNavOpen} gameId={gameId} gameProgress={gameProgress}/>
+      <UploadButton setNavOpen={setNavOpen} toggleUploadMenu={toggleUploadMenu}/>
+      <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
+      <PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
     </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,16 +4,38 @@ 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 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 t(hint.text, {ns: gameId})
+  }
+}
 
 export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
-    <Markdown>{hint.text}</Markdown>
+    <Markdown>{getHintText(hint)}</Markdown>
   </div>
 }
 
 export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
-    <Markdown>{hint.text}</Markdown>
+    <Markdown>{getHintText(hint)}</Markdown>
   </div>
 }
 
@@ -31,7 +53,7 @@ export function Hints({hints, showHidden, step, selected, toggleSelection, lastL
 
 export function DeletedHint({hint} : {hint: GameHint}) {
   return <div className="message information deleted-hint">
-    <Markdown>{hint.text}</Markdown>
+    <Markdown>{getHintText(hint)}</Markdown>
   </div>
 }
 
@@ -70,15 +92,19 @@ 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)
 
-  let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected
+  let k = proof?.steps.length ?
+    ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
+    : 0
 
   const activateHiddenHints = (ev) => {
     // If the last step (`k`) has errors, we want the hidden hints from the
     // second-to-last step to be affected
-    if (!(proof.steps.length)) {return}
+    if (!(proof?.steps.length)) {return}
 
     // state must not be mutated, therefore we need to clone the set
     let tmp = new Set(showHelp)
@@ -91,9 +117,9 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
     console.debug(`help: ${Array.from(tmp.values())}`)
   }
 
-  if (hasHiddenHints(proof.steps[k]) && !showHelp.has(k)) {
+  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

@@ -4,6 +4,7 @@
 import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { InteractiveDiagnostic } from '@leanprover/infoview-api';
+import { Diagnostic } from 'vscode-languageserver-types'
 import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { PreferencesState } from '../../state/preferences';
 
@@ -33,9 +34,19 @@ export const ProofContext = React.createContext<{
    */
   proof: ProofState,
   setProof: React.Dispatch<React.SetStateAction<ProofState>>
+  /** TODO: Workaround to capture a crash of the gameserver. */
+  interimDiags: Diagnostic[],
+  setInterimDiags: React.Dispatch<React.SetStateAction<Array<Diagnostic>>>
+  /** TODO: Workaround to capture a crash of the gameserver. */
+  crashed: Boolean,
+  setCrashed: React.Dispatch<React.SetStateAction<Boolean>>
 }>({
-  proof: {steps: [], diagnostics: [], completed: false},
-  setProof: () => {}
+  proof: {steps: [], diagnostics: [], completed: false, completedWithWarnings: false},
+  setProof: () => {},
+  interimDiags: [],
+  setInterimDiags: () => {},
+  crashed: false,
+  setCrashed: () => {}
 })
 
 
@@ -68,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<{
@@ -114,13 +128,13 @@ export const InputModeContext = React.createContext<{
   setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
   typewriterInput: string,
   setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
-  lockInputMode: boolean,
-  setLockInputMode: React.Dispatch<React.SetStateAction<boolean>>,
+  lockEditorMode: boolean,
+  setLockEditorMode: React.Dispatch<React.SetStateAction<boolean>>,
 }>({
   typewriterMode: true,
   setTypewriterMode: () => {},
   typewriterInput: "",
   setTypewriterInput: () => {},
-  lockInputMode: false,
-  setLockInputMode: () => {},
+  lockEditorMode: false,
+  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
@@ -268,7 +246,7 @@ interface GoalsProps {
 
 export function Goals({ goals, filter }: GoalsProps) {
     if (goals.goals.length === 0) {
-        return <>No goals</>
+        return <></>
     } else {
         return <>
           {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
@@ -345,96 +323,29 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
 })
 
 export function loadGoals(
-    rpcSess: RpcSessionAtPos,
-    uri: string,
-    setProof: React.Dispatch<React.SetStateAction<ProofState>>) {
-  console.info('sending rpc request to load the proof state')
+  rpcSess: RpcSessionAtPos,
+  uri: string,
+  setProof: React.Dispatch<React.SetStateAction<ProofState>>,
+  setCrashed: React.Dispatch<React.SetStateAction<Boolean>>) {
+console.info('sending rpc request to load the proof state')
 
-  rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then(
-    (proof : ProofState) => {
+rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then(
+  (proof : ProofState) => {
+    if (typeof proof !== 'undefined') {
       console.info(`received a proof state!`)
       console.log(proof)
       setProof(proof)
-
-
-
-
-      // 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)
-
-
-
+      setCrashed(false)
+    } else {
+      console.warn('received undefined proof state!')
+      setCrashed(true)
+      // setProof(undefined)
     }
-  )
+  }
+).catch((error) => {
+  setCrashed(true)
+  console.warn(error)
+})
 }
 
 

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">
@@ -293,7 +295,9 @@ function InfoAux(props: InfoProps) {
     type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'>
     const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((resolve, reject) => {
 
-        const proofReq = rpcSess.call('Game.getProofState', DocumentPosition.toTdpp(pos))
+        const proofReq = rpcSess.call('Game.getProofState', DocumentPosition.toTdpp(pos)).catch((error) => {
+            console.warn(error)
+          })
         const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos))
         const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos))
         const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound)

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';
 
@@ -36,15 +36,19 @@ import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
 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>
@@ -60,14 +64,14 @@ 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)
 
   const dispatch = useAppDispatch()
 
   React.useEffect(() => {
-    if (proof.completed) {
+    if (proof?.completed) {
       dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
 
       // On completion, add the names of all new items to the local storage
@@ -110,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} />
@@ -132,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 &&
@@ -150,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)
@@ -227,17 +235,21 @@ 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.completed && <div className="level-completed">Level completed! 🎉</div>}
+      {proof?.completedWithWarnings &&
+        <div className="level-completed">
+          {proof?.completed ? t("Level completed! 🎉") : t("Level completed with warnings 🎭")}
+        </div>
+      }
       <Infos />
-      <Hints hints={proof.steps[curPos?.line]?.goals[0]?.hints}
+      <Hints hints={proof?.steps[curPos?.line]?.goals[0]?.hints}
         showHidden={showHelp.has(curPos?.line)} step={curPos?.line}
         selected={selectedStep} toggleSelection={toggleSelection(curPos?.line)}
-        lastLevel={curPos?.line == proof.steps.length - 1}/>
+        lastLevel={curPos?.line == proof?.steps.length - 1}/>
       <MoreHelpButton selected={curPos?.line}/>
     </div>
   }
@@ -255,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 <></> }
 
@@ -262,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}>
-        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
+      <div className="command-text">{proof?.steps[i].command}</div>
+      <Button to="" className="undo-button btn btn-inverted" title={t("Retry proof from here")} onClick={deleteProof}>
+        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;{t("Retry")}
       </Button>
     </div>
   }
@@ -327,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) {
@@ -339,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>
@@ -384,17 +398,23 @@ 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)
   const {mobile} = React.useContext(PreferencesContext)
-  const { proof, setProof } = React.useContext(ProofContext)
+  const { proof, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext)
   const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
@@ -410,7 +430,7 @@ export function TypewriterInterface({props}) {
   function deleteProof(line: number) {
     return (ev) => {
       let deletedChat: Array<GameHint> = []
-      proof.steps.slice(line).map((step, i) => {
+      proof?.steps.slice(line).map((step, i) => {
         let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
 
         // Only add these hidden hints to the deletion stack which were visible
@@ -418,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 },
@@ -427,9 +450,9 @@ export function TypewriterInterface({props}) {
         forceMoveMarkers: false
       }])
       setSelectedStep(undefined)
-      setTypewriterInput(proof.steps[line].command)
+      setTypewriterInput(proof?.steps[line].command)
       // Reload proof on deleting
-      loadGoals(rpcSess, uri, setProof)
+      loadGoals(rpcSess, uri, setProof, setCrashed)
       ev.stopPropagation()
     }
   }
@@ -449,7 +472,7 @@ export function TypewriterInterface({props}) {
 
    // Scroll to the end of the proof if it is updated.
    React.useEffect(() => {
-    if (proof.steps.length > 1) {
+    if (proof?.steps.length > 1) {
       proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
     } else {
       proofPanelRef.current?.scrollTo(0,0)
@@ -471,7 +494,7 @@ export function TypewriterInterface({props}) {
   }, [selectedStep])
 
   // TODO: superfluous, can be replaced with `withErr` from above
-  let lastStepErrors = proof.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof.steps.length)) : false
+  let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false
 
 
   useServerNotificationEffect("$/game/loading", (params : any) => {
@@ -487,16 +510,45 @@ 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} />
-        {proof.steps.length ?
+        {crashed ? <div>
+          <p className="crashed_message">{t("Crashed! Go to editor mode and fix your proof! Last server response:")}</p>
+          {interimDiags.map(diag => {
+            const severityClass = diag.severity ? {
+              [DiagnosticSeverity.Error]: 'error',
+              [DiagnosticSeverity.Warning]: 'warning',
+              [DiagnosticSeverity.Information]: 'information',
+              [DiagnosticSeverity.Hint]: 'hint',
+            }[diag.severity] : '';
+
+            return <div>
+              <div className={`${severityClass} ml1 message`}>
+                <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>
+                </div>
+            </div>
+          })}
+
+        </div> : proof?.steps.length ?
           <>
-            {proof.steps.map((step, i) => {
+            {proof?.steps.map((step, i) => {
               let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
 
-              // if (i == proof.steps.length - 1 && hasInteractiveErrors(step.diags)) {
+              // if (i == proof?.steps.length - 1 && hasInteractiveErrors(step.diags)) {
               //   // if the last command contains an error, we only display the errors but not the
               //   // entered command as it is still present in the command line.
               //   // TODO: Should not use index as key.
@@ -517,18 +569,18 @@ export function TypewriterInterface({props}) {
                       hints={filteredHints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
                   }
-                  {/* <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
+                  {/* <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
                   {!(isLastStepWithErrors(proof, i)) &&
-                    <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+                    <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
                   }
-                  {mobile && i == proof.steps.length - 1 &&
+                  {mobile && i == proof?.steps.length - 1 &&
                     <MoreHelpButton />
                   }
 
                   {/* Show a message that there are no goals left */}
                   {/* {!step.goals.length && (
                     <div className="message information">
-                      {proof.completed ?
+                      {proof?.completed ?
                         <p>Level completed! 🎉</p> :
                         <p>
                           <b>no goals left</b><br />
@@ -541,16 +593,16 @@ export function TypewriterInterface({props}) {
               }
             //}
             )}
-            {proof.diagnostics.length > 0 &&
+            {proof?.diagnostics.length > 0 &&
               <div key={`proof-step-remaining`} className="step step-remaining">
-                <Errors errors={proof.diagnostics} typewriterMode={true} />
+                <Errors errors={proof?.diagnostics} typewriterMode={true} />
               </div>
             }
-            {mobile && proof.completed &&
+            {mobile && proof?.completed &&
               <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}`}>
@@ -559,11 +611,14 @@ export function TypewriterInterface({props}) {
                 }
               </div>
             }
-          </> : <CircularProgress variant="determinate" value={loadingProgress} />
+          </> : <CircularProgress variant="determinate" value={100*(1 - 1.024 ** (- loadingProgress))} />
+        // note: since we don't know the total number of files,
+        // we use a function which strictly monotonely increases towards `100` as `x → ∞`
+        // The base is chosen at random s.t. we get roughly 91% for `x = 100`.
         }
       </div>
     </div>
-    <Typewriter disabled={disableInput || !proof.steps.length}/>
+    <Typewriter disabled={disableInput || !proof?.steps.length}/>
     </RpcContext.Provider>
   </div>
 }

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/rpc_api.ts

@@ -49,6 +49,8 @@ export interface InteractiveTermGoal extends InteractiveGoalCore {
 export interface GameHint {
   text: string;
   hidden: boolean;
+  rawText: string;
+  varNames: string[][]; // in Lean: `Array (Name × Name)`
 }
 
 export interface InteractiveGoalWithHints {

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)
@@ -87,109 +86,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
   const inputRef = useRef()
 
   // The context storing all information about the current proof
-  const {proof, setProof} = React.useContext(ProofContext)
+  const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
 
   // state to store the last batch of deleted messages
   const {setDeletedChat} = React.useContext(DeletedChatContext)
 
   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}
@@ -210,7 +113,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
       }])
       setTypewriterInput('')
       // Load proof after executing edits
-      loadGoals(rpcSess, uri, setProof)
+      loadGoals(rpcSess, uri, setProof, setCrashed)
     }
 
     editor.setPosition(pos)
@@ -224,13 +127,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
 
   /* Load proof on start/switching to typewriter */
   useEffect(() => {
-    loadGoals(rpcSess, uri, setProof)
+    loadGoals(rpcSess, uri, setProof, setCrashed)
   }, [])
 
   /** If the last step has an error, add the command to the typewriter. */
   useEffect(() => {
     if (lastStepHasErrors(proof)) {
-      setTypewriterInput(proof.steps[proof.steps.length - 1].command)
+      setTypewriterInput(proof?.steps[proof?.steps.length - 1].command)
     }
   }, [proof])
 
@@ -238,6 +141,11 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == uri) {
       setProcessing(false)
+
+      console.log('Received lean diagnostics')
+      console.log(params.diagnostics)
+      setInterimDiags(params.diagnostics)
+
       //loadGoals(rpcSess, uri, setProof)
 
       // TODO: loadAllGoals()
@@ -254,13 +162,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
     // loadAllGoals()
   }, [uri]);
 
-  // React when answer from the server comes back
-  useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => {
-    console.log('Received game diagnostics')
-    console.log(`diag. uri : ${params.uri}`)
-    console.log(params.diagnostics)
+  // // React when answer from the server comes back
+  // useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => {
+  //   console.log('Received game diagnostics')
+  //   console.log(`diag. uri : ${params.uri}`)
+  //   console.log(params.diagnostics)
 
-  }, [uri]);
+  // }, [uri]);
 
 
   useEffect(() => {
@@ -344,13 +252,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
   }
 
   // do not display if the proof is completed (with potential warnings still present)
-  return <div className={`typewriter${proof.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
+  return <div className={`typewriter${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
       <form onSubmit={handleSubmit}>
         <div className="typewriter-input-wrapper">
           <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>
@@ -376,10 +284,10 @@ export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
 export function getInteractiveDiagsAt (proof: ProofState, k : number) {
   if (k == 0) {
     return []
-  } else if (k >= proof.steps.length-1) {
+  } else if (k >= proof?.steps.length-1) {
     // TODO: Do we need that?
-    return proof.diagnostics.filter(msg => msg.range.start.line >= proof.steps.length-1)
+    return proof?.diagnostics.filter(msg => msg.range.start.line >= proof?.steps.length-1)
   } else {
-    return proof.diagnostics.filter(msg => msg.range.start.line == k-1)
+    return proof?.diagnostics.filter(msg => msg.range.start.line == k-1)
   }
 }

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" :
-                disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
+  const title = locked ? t("Not unlocked yet") :
+                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 = {
-  'Dutch': '🇳🇱',
-  'English': '🇬🇧',
-  'French': '🇫🇷',
-  'German': '🇩🇪',
-  'Italian': '🇮🇹',
-  'Spanish': '🇪🇸',
-}
+import { PreferencesPopup } from './popup/preferences';
+import { ImpressumButton, MenuButton, PreferencesButton } from './app_bar';
+import ReactCountryFlag from 'react-country-flag';
+import lean4gameConfig from '../config.json'
+import i18next from 'i18next';
 
 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="short-description">{data.short}
+      <div className="title">{t(data.title, { ns: gameId })}</div>
+      <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><Markdown>{data.prerequisites.join(', ')}</Markdown></td>
+        <td title="consider playing these games first.">{t("Prerequisites")}</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 title={`in ${data.languages.join(', ')}`}>{data.languages.map((lan) => flag[lan]).join(', ')}</td>
+        <td>{t("Language")}</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,67 @@ function LandingPage() {
 
   const navigate = useNavigate();
 
-  const [impressum, setImpressum] = React.useState(false);
-  const openImpressum = () => setImpressum(true);
-  const closeImpressum = () => setImpressum(false);
+  const [impressumPopup, setImpressumPopup] = React.useState(false);
+  const [preferencesPopup, setPreferencesPopup] = React.useState(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 [allTiles, setAllTiles] = React.useState([])
+  const { t, i18n } = useTranslation()
 
-  // const getTiles=()=>{
-  //   fetch('featured_games.json', {
-  //     headers : {
-  //       'Content-Type': 'application/json',
-  //       'Accept': 'application/json'
-  //     }
-  //   }
-  //   ).then(function(response){
-  //     return response.json()
-  //   }).then(function(data) {
-  //     setAllGames(data.featured_games)
+  // Load the namespaces of all games
+  // TODO: should `allGames` contain game-ids starting with `g/`?
+  i18next.loadNamespaces(lean4gameConfig.allGames.map(id => `g/${id}`))
 
-  //   })
-  // }
+  let allTiles = lean4gameConfig.allGames.map((gameId) => {
+    let q =  useGetGameInfoQuery({game: `g/${gameId}`})
 
-  // React.useEffect(()=>{
-  //   getTiles()
-  // },[])
+    // 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);
+    //   }
+    // }
 
-  // React.useEffect(()=>{
-
-  //   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 q.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>
-          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>
+            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 ?
-        <p>No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
-          game directly from a local folder.
+      {allTiles.filter(x => x != null).length == 0 ?
+        <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}`}
@@ -169,53 +157,61 @@ function LandingPage() {
     </div>
     <section>
       <div className="wrapper">
-        <h2>Development notes</h2>
-        <p>
-          As this server runs lean on our university machines, it has a limited capacity.
-          Our current estimate is about 70 simultaneous games.
-          We hope to address and test this limitation better in the future.
-        </p>
-        <p>
-          Most aspects of the games and the infrastructure are still in development. Feel free to
-          file a <a target="_blank" href="https://github.com/leanprover-community/lean4game/issues">GitHub Issue</a> about
-          any problems you experience!
-        </p>
+        <h2>{t("Development notes")}</h2>
+        <Trans>
+          <p>
+            As this server runs lean on our university machines, it has a limited capacity.
+            Our current estimate is about 70 simultaneous games.
+            We hope to address and test this limitation better in the future.
+          </p>
+          <p>
+            Most aspects of the games and the infrastructure are still in development. Feel free to
+            file a <a target="_blank" href="https://github.com/leanprover-community/lean4game/issues">GitHub Issue</a> about
+            any problems you experience!
+          </p>
+        </Trans>
       </div>
     </section>
     <section>
       <div className="wrapper">
-        <h2>Adding new games</h2>
-        <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
-          a template and read <a target="_blank" href="https://github.com/leanprover-community/lean4game/">How to Create a Game</a>.
-        </p>
-        <p>
-          You can directly load your games into the server and play it using
-          the correct URL. The <a target="_blank" href="https://github.com/leanprover-community/lean4game/">instructions above</a> also
-          explain the details for how to load your game to the server.
+        <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
+            a template and read <a target="_blank" href="https://github.com/leanprover-community/lean4game/">How to Create a Game</a>.
+          </p>
+          <p>
+            You can directly load your games into the server and play it using
+            the correct URL. The <a target="_blank" href="https://github.com/leanprover-community/lean4game/">instructions above</a> 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.
-        </p>
-        <p>
-          Featured games on this page are added manually.
-          Please get in contact and we-ll happily add yours.
-        </p>
+            We'd like to encourage you to contact us if you have any questions.
+          </p>
+          <p>
+            Featured games on this page are added manually.
+            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>
-          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.
+          <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.
+          </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>
 

client/src/components/level.tsx

@@ -16,6 +16,7 @@ import { InfoviewApi } from '@leanprover/infoview'
 import { EditorContext } from '../../../node_modules/lean4-infoview/src/infoview/contexts'
 import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection'
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'
+import { Diagnostic } from 'vscode-languageserver-types'
 
 import { GameIdContext } from '../app'
 import { useAppDispatch, useAppSelector } from '../hooks'
@@ -50,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()
@@ -59,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 = () => {
-    setImpressum(false)
-  }
+  // Load the namespace of the game
+  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} /> :
-      <PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} />}
+      <Introduction impressum={impressum} setImpressum={setImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup} /> :
+      <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)
@@ -84,7 +107,7 @@ function ChatPanel({lastLevel, visible = true}) {
   const {selectedStep, setSelectedStep} = useContext(SelectionContext)
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
-  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)
+  let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
 
   function toggleSelection(line: number) {
     return (ev) => {
@@ -120,55 +143,55 @@ 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">
       {introText?.filter(t => t.trim()).map(((t, i) =>
         // Show the level's intro text as hints, too
         <Hint key={`intro-p-${i}`}
-          hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
+          hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
       ))}
-      {proof.steps.map((step, i) => {
+      {proof?.steps.map((step, i) => {
         let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
         if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
           return <Hints key={`hints-${i}`}
           hints={filteredHints} showHidden={showHelp.has(i)} step={i}
-          selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
+          selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
         }
       })}
 
       {/* {modifiedHints.map((step, i) => {
         // It the last step has errors, it will have the same hints
         // as the second-to-last step. Therefore we should not display them.
-        if (!(i == proof.steps.length - 1 && withErr)) {
+        if (!(i == proof?.steps.length - 1 && withErr)) {
           // TODO: Should not use index as key.
           return <Hints key={`hints-${i}`}
             hints={step} showHidden={showHelp.has(i)} step={i}
-            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
+            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
         }
       })} */}
       <DeletedHints hints={deletedChat}/>
-      {proof.completed &&
+      {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>
           }
         </>
       }
     </div>
     <div className="button-row">
-      {proof.completed && (lastLevel ?
+      {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 />
@@ -189,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)
@@ -208,6 +232,10 @@ function PlayableLevel({impressum, setImpressum}) {
 
   // The state variables for the `ProofContext`
   const [proof, setProof] = useState<ProofState>({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
+  const [interimDiags, setInterimDiags] = useState<Array<Diagnostic>>([])
+  const [isCrashed, setIsCrashed] = useState<Boolean>(false)
+
+
   // When deleting the proof, we want to keep to old messages around until
   // a new proof has been entered. e.g. to consult messages coming from dead ends
   const [deletedChat, setDeletedChat] = useState<Array<GameHint>>([])
@@ -217,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]
 
@@ -277,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()
@@ -307,6 +336,8 @@ function PlayableLevel({impressum, setImpressum}) {
           console.debug(`not inserting template.`)
         }
       }
+    } else {
+      setLockEditorMode(false)
     }
   }, [level, levelId, worldId, gameId, editor])
 
@@ -321,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(),
@@ -330,19 +361,19 @@ function PlayableLevel({impressum, setImpressum}) {
       }]);
       editor.focus()
     }
-  }, [typewriterMode])
+  }, [typewriterMode, lockEditorMode])
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
-    if (proof.steps.length) {
+    if (proof?.steps.length) {
       console.debug(Array.from(showHelp))
-      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.steps.length))))
+      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof?.steps.length))))
     }
   }, [proof])
 
   // save showed help in store
   useEffect(() => {
-    if (proof.steps.length) {
+    if (proof?.steps.length) {
       console.debug(`showHelp:\n ${showHelp}`)
       dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)}))
     }
@@ -350,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(),
@@ -373,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}}>
-          <ProofContext.Provider value={{proof, setProof}}>
+        <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]}` +
-                    (level?.data?.title && ` : ${level?.data?.title}`)}
-                  toggleImpressum={toggleImpressum} />
+                  levelTitle={(mobile ? "" : t("Level")) + ` ${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
+                    (level?.data?.title && ` : ${t(level?.data?.title, {ns: gameId})}`)}
+                  toggleImpressum={toggleImpressum}
+                  toggleInfo={toggleInfo}
+                  togglePreferencesPopup={togglePreferencesPopup}
+                  />
                 {mobile?
                   // TODO: This is copied from the `Split` component below...
                   <>
@@ -417,24 +451,25 @@ 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">
       {text?.filter(t => t.trim()).map(((t, i) =>
         <Hint key={`intro-p-${i}`}
-          hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
+          hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
       ))}
     </div>
     <div className={`button-row${mobile ? ' mobile' : ''}`}>
       {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>
@@ -444,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)
 
@@ -462,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 ?
@@ -470,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={worldId=="Proposition" ? "cover" : "contain"} src={path.join("data", gameId, image)} alt="" />
+              <img className="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>
-
-    <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>
-
-    <Button onClick={eraseProgress} to="">Delete</Button>
-    <Button onClick={downloadAndErase} to="">Download & Delete</Button>
-    <Button onClick={handleClose} to="">Cancel</Button>
+    <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="">{t("Delete")}</Button>
+    <Button onClick={downloadAndErase} to="">{t("Download & Delete")}</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,90 +1,115 @@
 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'> {
-    handleClose: () => void
-}
+export function PreferencesPopup({ handleClose }: { 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: t('Mobile'),
+      key: "mobile"
+    },
+    {
+      value: 1,
+      label: t('Auto'),
+      key: "auto"
+    },
+    {
+      value: 2,
+      label: t('Desktop'),
+      key: "desktop"
+    },
+  ];
 
-    const marks = [
-        {
-            value: 0,
-            label: 'Mobile',
-            key: "mobile"
-        },
-        {
-            value: 1,
-            label: 'Auto',
-            key: "auto"
-        },
-        {
-            value: 2,
-            label: 'Desktop',
-            key: "desktop"
-        },
-    ];
+  const handlerChangeLayout = (_: Event, value: number) => {
+    setLayout(marks[value].key as IPreferencesContext["layout"])
+  }
 
-    const handlerChangeLayout = (_: Event, value: number) => {
-        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">
-            <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-            <Typography variant="body1" component="div" className="settings">
-                <div className='preferences-category'>
-                    <div className='category-title'>
-                        <h3>Layout</h3>
-                    </div>
-                    <div className='preferences-item first leave-left-gap'>
-                        <FormControlLabel
-                            control={
-                                <Box sx={{ width: 300 }}>
-                                    <Slider
-                                        aria-label="Always visible"
-                                        value={marks.find(item => item.key === layout).value}
-                                        step={1}
-                                        marks={marks}
-                                        max={2}
-                                        sx={{
-                                            '& .MuiSlider-track': { display: 'none', },
-                                        }}
-                                        onChange={handlerChangeLayout}
-                                    />
-                                </Box>
-                            }
-                            label=""
-                        />
-                    </div>
-                </div>
-
-                <div className='preferences-category tail-category'>
-                    <div className='preferences-item'>
-                        <FormControlLabel
-                            control={
-                                <Switch
-                                    checked={isSavePreferences}
-                                    onChange={() => setIsSavePreferences(!isSavePreferences)}
-                                    name="checked"
-                                    color="primary"
-                                />
-                            }
-                            label="Save my settings (in the browser store)"
-                            labelPlacement="end"
-                        />
-                    </div>
-                </div>
-            </Typography>
+  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="settings">
+        <div className='preferences-category'>
+          <div className='category-title'>
+            <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={t("Always visible")}
+                    value={marks.find(item => item.key === layout).value}
+                    step={1}
+                    marks={marks}
+                    max={2}
+                    sx={{
+                      '& .MuiSlider-track': { display: 'none', },
+                    }}
+                    onChange={handlerChangeLayout}
+                  />
+                </Box>
+              }
+              label=""
+            />
+          </div>
+        </div>
+
+        <div className='preferences-category tail-category'>
+          <div className='preferences-item'>
+            <FormControlLabel
+              control={
+                <Switch
+                  checked={isSavePreferences}
+                  onChange={() => setIsSavePreferences(!isSavePreferences)}
+                  name="checked"
+                  color="primary"
+                />
+              }
+              label={t("Save my settings (in the browser store)")}
+              labelPlacement="end"
+            />
+          </div>
+        </div>
+      </Typography>
     </div>
+  </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,42 +10,46 @@ 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>
-    <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>
-    <p>
-      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 <code>simp</code> in a level, you can use it henceforth in any level.
-    </p>
-    <p>The options are:</p>
+    <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.
+      </p>
+      <p>
+        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 <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">tactics</th>
+          <th scope="col">{t("levels")}</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>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>
+      <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>
+    </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,26 @@
+{
+  "allGames": [
+    "leanprover-community/nng4",
+    "hhu-adam/robo",
+    "djvelleman/stg4",
+    "trequetrum/lean4game-logic"
+  ],
+
+  "languages": [
+    {
+      "iso": "en",
+      "flag": "GB",
+      "name": "English"
+    },
+    {
+      "iso": "de",
+      "flag": "DE",
+      "name": "Deutsch"
+    },
+    {
+      "iso": "zh",
+      "flag": "CN",
+      "name": "中文"
+    }
+  ]
+}

client/src/css/infoview.css

@@ -41,6 +41,13 @@
 .level-completed {
   font-size: 1.8rem;
   font-weight: 500;
+  padding-left: .5em;
+  padding-right: .5em;
+  padding-top: .2em;
+  padding-bottom: .2em;
+  border-radius: .5em;
+  background-color: #eee;
+
 }
 
 .typewriter {
@@ -211,3 +218,10 @@
 .undo-button {
   color: #888;
 }
+
+.crashed_message {
+  color: #D8000C;
+  font-weight: bold;
+  padding-left: .5em;
+  padding-right: .5em;
+}

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;
 }
 
-/* DEBUG */
-.proof .step {
-  border: 2px solid rgb(0, 123, 255);
+/* 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';
 
 
 
@@ -20,7 +21,14 @@ let root_object: RouteObject = single_game ? {
   loader: () => redirect("/g/local/game")
 } : {
   path: "/",
-  element: <LandingPage />,
+  element: <App />,
+  errorElement: <ErrorPage />,
+  children: [
+    {
+      path: "/",
+      element: <LandingPage />,
+    }
+  ]
 }
 
 const router = createHashRouter([

client/src/state/hooks/use_preferences.ts

@@ -1,9 +1,10 @@
 import React, { useState } from "react";
 import { useAppDispatch, useAppSelector } from "../../hooks";
-import { 
-    PreferencesState, 
-    setLayout as setPreferencesLayout, 
+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)
@@ -28,14 +32,14 @@ const UsePreferences = () => {
         if (layout === "auto"){
           void automaticallyAdjustLayout()
           window.addEventListener('resize', automaticallyAdjustLayout)
-    
+
           return () => window.removeEventListener('resize', automaticallyAdjustLayout)
         } else {
           setMobile(layout === "mobile")
         }
     }, [layout])
 
-    return {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}
-} 
+    return {mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage}
+}
 
-export default UsePreferences;
+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,7 +17,8 @@ export const AUTO_SWITCH_THRESHOLD = 800
 
 const initialState: PreferencesState = loadPreferences() ??{
     layout: "auto",
-    isSavePreferences: false
+    isSavePreferences: false,
+    language: "en",
 }
 
 export const preferencesSlice = createSlice({
@@ -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

@@ -189,8 +189,7 @@ The statement is the exercise of the level. The basics work the same as they wou
 
 #### Name
 
-You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
-
+You can give your exercise a name: `Statement my_first_exercise (n : Nat) …`. If you do so, it will be added to the inventory and be available in future levels.
 You can but a `Statement` inside namespaces like you would with `theorem`.
 
 #### Doc String / Exercise statement
@@ -203,14 +202,7 @@ Statement ...
   sorry
 ```
 
-#### 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 ...
-```
+For more details and features, read [Writing Exercises](writing_exercises.md)
 
 ### 6. c) Proof
 

doc/hints.md

@@ -86,4 +86,36 @@ create new assumptions.
 
 You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
 
+**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!
+
 TODO: Write a doc about latex/markdown options available.
+
+### 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}
+$$
+```
+
+See https://www.jmilne.org/not/Mamscd.pdf

doc/troubleshoot.md

@@ -2,6 +2,15 @@
 
 Here are some issues experienced by users.
 
+- You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
+  ```
+  cd [THE PROJECT]
+  rm -rf .lake/
+  lake update -R
+  lake build
+  ```
+  If you experience problems related to Lean or lake, you should first try to reset it this way.
+
 # VSCode Dev-Container
 * If you don't get the pop-up, you might have disabled them, and you can reenable it by
   running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.

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 ...
+```

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

@@ -37,6 +37,14 @@ 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 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

server/GameServer/Commands.lean

@@ -2,9 +2,15 @@ import GameServer.Helpers
 import GameServer.Inventory
 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 -/
@@ -32,16 +38,17 @@ elab "Level" level:num : command => do
 
 /-- Define the title of the current game/world/level. -/
 elab "Title" t:str : command => do
+  let title ← t.getString.translate
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
-  | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
+  | .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
-      tile := {game.tile with title := t.getString}}
+      title := title
+      tile := {game.tile with title := title}}
 
 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
-  let intro := t.getString
+  let intro ← t.getString.translate
   match ← getCurLayer with
   | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
   | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
@@ -49,7 +56,7 @@ elab "Introduction" t:str : command => do
 
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
-  let info:= t.getString
+  let info ← t.getString.translate
   match ← getCurLayer with
   | .Level =>
     logError "Can't use `Info` in a level!"
@@ -81,7 +88,7 @@ elab "Image" t:str : command => do
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
-  let conclusion := t.getString
+  let conclusion ← t.getString.translate
   match ← getCurLayer with
   | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
   | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
@@ -94,18 +101,19 @@ elab "Prerequisites" t:str* : command => do
 
 /-- Short caption for the game (1 sentence) -/
 elab "CaptionShort" t:str : command => do
-  let caption := t.getString
+  let caption ← t.getString.translate
   modifyCurGame fun game => pure {game with
     tile := {game.tile with short := caption}}
 
 /-- More detailed description what the game is about (2-4 sentences). -/
 elab "CaptionLong" t:str : command => do
-  let caption := t.getString
+  let caption ← t.getString.translate
   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"`.
-NOTE: For the time being, only a single language is supported.
+/-- A list of Languages the game is translated to. For example `Languages "de" "en"`.
+
+The keys are ISO language codes.
  -/
 elab "Languages" t:str* : command => do
   modifyCurGame fun game => pure {game with
@@ -141,6 +149,7 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
  -/
 elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
   let doc ← parseDocCommentLegacy doc content
+  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Tactic
     name := name.getId
@@ -165,6 +174,7 @@ The theorem/definition to have the same fully qualified name as in mathlib.
 elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
     command => do
   let doc ← parseDocCommentLegacy doc content
+  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Lemma
     name := name.getId
@@ -194,6 +204,7 @@ The theorem/definition to have the same fully qualified name as in mathlib.
  -/
 elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
   let doc ← parseDocCommentLegacy doc template
+  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Definition
     name := name.getId,
@@ -334,12 +345,40 @@ 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
+  | some d => d.translate
 
   -- Save the messages before evaluation of the proof.
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
@@ -355,36 +394,40 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     collectUsedInventory proof
   | _ => throwError "expected `:=`"
 
+  -- extract the `tacticSeq` from `val` in order to add `let_intros` in front.
+  -- TODO: don't understand meta-programming enough to avoid having `let_intros`
+  -- duplicated three times below…
+  let tacticStx : TSyntax `Lean.Parser.Tactic.tacticSeq := match val with
+  | `(Parser.Command.declVal| := by $proof) => proof
+  | _ => panic "expected `:= by`"
+
   -- Add theorem to context.
   match statementName with
   | some name =>
     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 $val)
+      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 $val)
+      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 $val)
+    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)})
     elabCommand thmStatement
 
   let msgs := (← get).messages
-
   let mut hints := #[]
   let mut nonHintMsgs := #[]
   for msg in msgs.msgs do
@@ -396,12 +439,41 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
         .nest hidden $
         .compose (.ofGoal text) (.ofGoal goal) := msg.data then
       let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
+
+        let goalDecl ← goal.getDecl
+        let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (·.fvarId)
+
+        -- NOTE: This code about `hintFVarsNames` is duplicated from `RpcHandlers`
+        -- where the variable bijection is constructed, and they
+        -- need to be matching.
+        -- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
+        -- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
+        -- and we wrap them in `«{}»` here since I don't know how to do it later.
+        let mut hintFVarsNames : Array Expr := #[]
+        for fvar in fvars do
+          let name₁ ← fvar.getUserName
+          hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
+
+        let text ← instantiateMVars (mkMVar text)
+
+        -- Evaluate the text in the `Hint`'s context to get the old variable names.
+        let rawText := (← GameServer.evalHintMessage text) hintFVarsNames
+        let ctx₂ := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+        let rawText : String ← (MessageData.withContext ctx₂ rawText).toString
+
         return {
           goal := ← abstractCtx goal
-          text := ← instantiateMVars (mkMVar text)
+          text := text
+          rawText := rawText
           strict := strict == 1
           hidden := hidden == 1
         }
+
+      -- Note: The current setup for hints is a bit convoluted, but for now we need to
+      -- send the text once through i18n to register it in the env extension.
+      -- This could probably be rewritten once i18n works fully.
+      let _ ← hint.rawText.translate
+
       hints := hints.push hint
     else
       nonHintMsgs := nonHintMsgs.push msg
@@ -427,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
@@ -436,10 +509,13 @@ 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 -/
 
+open GameServer in
+
 /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
 see hints. The tactic does not affect the goal state.
 -/
@@ -501,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."
 
@@ -665,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 =>
@@ -676,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 =>
@@ -798,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 =>
@@ -812,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

@@ -1,7 +1,13 @@
 import GameServer.AbstractCtx
 import GameServer.Graph
+import GameServer.Hints
 
+open GameServer
 
+-- TODO: Is there a better place?
+/-- Keywords that the server should not consider as tactics. -/
+def GameServer.ALLOWED_KEYWORDS : List String :=
+  ["with", "fun", "at", "only", "by", "generalizing"]
 
 /-- The default game name if `Game "MyGame"` is not used. -/
 def defaultGameName: String := "MyGame"
@@ -18,29 +24,13 @@ defined in this file.
 
 open Lean
 
-/-! ## Hints -/
-
-/-- A hint to help the user with a specific goal state -/
-structure GoalHintEntry where
-  goal : AbstractCtxResult
-  /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
-  text : Expr
-  /-- If true, then hint should be hidden and only be shown on player's request -/
-  hidden : Bool := false
-  /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
-  strict : Bool := false
-
-instance : Repr GoalHintEntry := {
-  reprPrec := fun a n => reprPrec a.text n
-}
-
 /-! ## Inventory (documentation)
 
 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.
@@ -275,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

@@ -4,6 +4,7 @@ import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
 import GameServer.EnvExtensions
+import GameServer.Tactic.LetIntros
 
 namespace MyModule
 
@@ -122,7 +123,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
     -- Atoms might be tactic names or other keywords.
     -- Note: We whitelisted known keywords because we cannot
     -- distinguish keywords from tactic names.
-    let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"]
+    let allowed := GameServer.ALLOWED_KEYWORDS
     -- Ignore syntax elements that do not start with a letter or are listed above.
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       -- Treat `simp?` and `simp!` like `simp`
@@ -169,15 +170,20 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
       match theoremsAndDefs.find? (·.name == n) with
       | none =>
         -- Theorem will never be introduced in this game
-        addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+        addMessageByDifficulty info s!"The theorem/definition '{n}' is not available in this game!"
       | some thm =>
         -- Theorem is introduced at some point in the game.
         if thm.disabled then
           -- Theorem is disabled in this level.
           addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
         else if thm.locked then
-          -- Theorem is still locked.
-          addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+          match workerState.inventory.find? (· == n.toString) with
+          | none =>
+            -- Theorem is still locked.
+            addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+          | some _ =>
+            -- Theorem is in the inventory, allow it.
+            pure ()
 
 where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
   -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
@@ -253,8 +259,11 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
 
+          -- Always call `let_intros` to get rid `let` statements in the goal.
+          -- 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 {$(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preamble⟩); $(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
       cmdCtx cmdStateRef
   let postNew := (← tacticCacheNew.get).post
@@ -299,7 +308,7 @@ where
   private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
       (snaps : Array Snapshot) : IO Unit := do
     let trees := snaps.map fun snap => snap.infoTree
-    let references := findModuleRefs m.text trees (localVars := true)
+    let references ← findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
     let param := { version := m.version, references : LeanIleanInfoParams }
     hOut.writeLspNotification { method, param }
 
@@ -322,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
@@ -386,60 +398,60 @@ def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.Ini
 
   hOut.writeLspNotification { method := "$/game/publishProofState", param }
 
-  /-- Checks whether game level has been completed and sends a notification to the client -/
-  def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
-    -- check if there is any error or warning
-    for snap in snaps do
-      if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
-      then return
-    let param := { uri := m.uri : GameCompletedParams}
-    hOut.writeLspNotification { method := "$/game/completed", param }
+/-- Checks whether game level has been completed and sends a notification to the client -/
+def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
+  -- check if there is any error or warning
+  for snap in snaps do
+    if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
+    then return
+  let param := { uri := m.uri : GameCompletedParams}
+  hOut.writeLspNotification { method := "$/game/completed", param }
 
-  /-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/
-  -- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private
-  private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) :
-      AsyncElabM (Option Snapshot) := do
-    cancelTk.check
-    let s ← get
-    let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
-    if lastSnap.isAtEnd then
-      publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
-      publishProgressDone m ctx.hOut
-      publishIleanInfoFinal m ctx.hOut s.snaps
-      return none
-    publishProgressAtPos m lastSnap.endPos ctx.hOut
+/-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/
+-- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private
+private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
+    (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) :
+    AsyncElabM (Option Snapshot) := do
+  cancelTk.check
+  let s ← get
+  let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
+  if lastSnap.isAtEnd then
+    publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
+    publishProgressDone m ctx.hOut
+    publishIleanInfoFinal m ctx.hOut s.snaps
+    return none
+  publishProgressAtPos m lastSnap.endPos ctx.hOut
 
-    -- (modified part)
-    -- Make sure that there is at least one snap after the head snap, so that
-    -- we can see the current goal even on an empty document
-    let couldBeEndSnap := s.snaps.size > 1
-    let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
-      gameWorkerState initParams
+  -- (modified part)
+  -- Make sure that there is at least one snap after the head snap, so that
+  -- we can see the current goal even on an empty document
+  let couldBeEndSnap := s.snaps.size > 1
+  let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
+    gameWorkerState initParams
 
-    set { s with snaps := s.snaps.push snap }
-    cancelTk.check
-    publishProofState m snap initParams ctx.hOut
-    publishDiagnostics m snap.diagnostics.toArray ctx.hOut
-    publishIleanInfoUpdate m ctx.hOut #[snap]
-    return some snap
+  set { s with snaps := s.snaps.push snap }
+  cancelTk.check
+  -- publishProofState m snap initParams ctx.hOut
+  publishDiagnostics m snap.diagnostics.toArray ctx.hOut
+  publishIleanInfoUpdate m ctx.hOut #[snap]
+  return some snap
 
-  -- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`.
-  @[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps]
-  def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
-      (startAfterMs : UInt32) (gameWorkerState : WorkerState)
-      : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
-    let ctx ← read
-    let some headerSnap := snaps[0]? | panic! "empty snapshots"
-    if headerSnap.msgLog.hasErrors then
-      publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
-      publishIleanInfoFinal m ctx.hOut #[headerSnap]
-      return AsyncList.ofList [headerSnap]
-    else
-      publishIleanInfoUpdate m ctx.hOut snaps
-      return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
-        IO.sleep startAfterMs
-        AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
+-- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`.
+@[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps]
+def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
+    (startAfterMs : UInt32) (gameWorkerState : WorkerState)
+    : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
+  let ctx ← read
+  let some headerSnap := snaps[0]? | panic! "empty snapshots"
+  if headerSnap.msgLog.hasErrors then
+    publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
+    publishIleanInfoFinal m ctx.hOut #[headerSnap]
+    return AsyncList.ofList [headerSnap]
+  else
+    publishIleanInfoUpdate m ctx.hOut snaps
+    return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
+      IO.sleep startAfterMs
+      AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 
@@ -503,6 +515,12 @@ def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
   fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
   fileMap  := default
 
+/-- `gameDir` and `module` were added.
+
+TODO: In general this resembles little similarity with the
+original code, and I don't know why...
+-/
+-- @[inherit_doc Lean.Server.FileWorker.compileHeader]
 def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
     (gameDir : String) (module : Name):
     IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
@@ -538,7 +556,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     let cmdState := Elab.Command.mkState headerEnv {} opts
     let cmdState := { cmdState with infoState := {
       enabled := true
-      trees := #[Elab.InfoTree.context ({
+      trees := #[Elab.InfoTree.context (.commandCtx {
         env     := headerEnv
         fileMap := m.text
         ngen    := { namePrefix := `_worker }
@@ -555,7 +573,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     let headerSnap := {
       beginPos := 0
       stx := headerStx
-      mpState := {}
+      mpState := {} -- was `headerParserState`
       cmdState := cmdState
       interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
       tacticCache := (← IO.mkRef {})

server/GameServer/Helpers.lean

@@ -1,13 +1,14 @@
 import Lean
+import GameServer.Helpers.PrettyPrinter
 
 /-! This document contains various things which cluttered `Commands.lean`. -/
 
 open Lean Meta Elab Command
 
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
-
 /-! ## 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
@@ -61,47 +62,10 @@ 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
 
-
-/-- Remove any spaces at the beginning of a new line -/
-partial def removeIndentation (s : String) : String :=
-  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
-    let c := s.get i
-    let i := s.next i
-    if s.atEnd i then
-      acc.push c
-    else if removeSpaces && c == ' ' then
-      loop i acc (removeSpaces := true)
-    else if c == '\n' then
-      loop i (acc.push c) (removeSpaces := true)
-    else
-      loop i (acc.push c)
-  loop ⟨0⟩ ""
-
-
 /-! ## Loops in Graph-like construct
 
 TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?

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/Hints.lean

@@ -0,0 +1,54 @@
+import GameServer.AbstractCtx
+
+/-!
+This file contains anything related to the `Hint` tactic used to add hints to a game level.
+-/
+
+open Lean Meta Elab
+
+namespace GameServer
+
+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
+
+/-- A hint to help the user with a specific goal state -/
+structure GoalHintEntry where
+  goal : AbstractCtxResult
+  /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
+  text : Expr
+  rawText : String
+  /-- If true, then hint should be hidden and only be shown on player's request -/
+  hidden : Bool := false
+  /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
+  strict : Bool := false
+
+instance : Repr GoalHintEntry := {
+  reprPrec := fun a n => reprPrec a.text n
+}
+
+/-- For a hint `(hint : GoalHintEntry)` one uses `(← evalHintMessage hint.text) x`
+ where `(x : Array Expr)` contains the names of all the variables that should be inserted
+ in the text.
+
+ TODO: explain better. -/
+unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
+  evalExpr (Array Expr → MessageData)
+    (.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
+      (mkConst ``MessageData) .default)
+
+@[implemented_by evalHintMessageUnsafe]
+def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
+
+/-- Remove any spaces at the beginning of a new line -/
+partial def removeIndentation (s : String) : String :=
+  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
+    let c := s.get i
+    let i := s.next i
+    if s.atEnd i then
+      acc.push c
+    else if removeSpaces && c == ' ' then
+      loop i acc (removeSpaces := true)
+    else if c == '\n' then
+      loop i (acc.push c) (removeSpaces := true)
+    else
+      loop i (acc.push c)
+  loop ⟨0⟩ ""

server/GameServer/InteractiveGoal.lean

@@ -146,7 +146,7 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
     return {
       hyps
       type := goalFmt
-      ctx := ⟨← Elab.ContextInfo.save⟩
+      ctx := ⟨{← Elab.CommandContextInfo.save with }⟩
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId

server/GameServer/Inventory.lean

@@ -121,7 +121,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
   | .atom _info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore some standard keywords
-    let allowed := ["with", "fun", "at", "only", "by"]
+    let allowed := GameServer.ALLOWED_KEYWORDS
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
       return {acc with tactics := acc.tactics.insert val}

server/GameServer/RpcHandlers.lean

@@ -1,6 +1,7 @@
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
-import Std.Data.Array.Init.Basic
+import GameServer.Hints
+import I18n
 
 open Lean
 open Server
@@ -103,14 +104,6 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in
   then return some bij
   else return none
 
-unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
-  evalExpr (Array Expr → MessageData)
-    (.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
-      (mkConst ``MessageData) .default)
-
-@[implemented_by evalHintMessageUnsafe]
-def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
-
 open Meta in
 /-- Find all hints whose trigger matches the current goal -/
 def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
@@ -121,19 +114,53 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
       openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
         if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
         then
-          let lctx := (← goal.getDecl).lctx
-          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+
+          -- NOTE: This code for `hintFVarsNames` is also duplicated in the
+          -- "Statement" command, where `hint.rawText` is created. They need to be matching.
+          -- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
+          -- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
+          -- and we wrap them in `«{}»` here since I don't know how to do it later.
+          let mut hintFVarsNames : Array Expr := #[]
+          for fvar in hintFVars do
+            let name₁ ← fvar.fvarId!.getUserName
+            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
+
+          let lctx := (← goal.getDecl).lctx -- the player's local context
+          if let some bij ← matchDecls hintFVars lctx.getFVars
+            (strict := hint.strict) (initBij := fvarBij)
           then
             let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
+            -- Evaluate the text in the player's context to get the new variable names.
             let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
             let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
             let text ← (MessageData.withContext ctx text).toString
-            return some { text := text, hidden := hint.hidden }
+
+            -- Here we map the goal's variable names to the player's variable names.
+            let mut varNames : Array <| Name × Name := #[]
+            for (fvar₁, fvar₂) in bij.forward.toArray do
+              -- get the `userName` of the fvar in the opened local context of the hint.
+              let name₁ ← fvar₁.getUserName
+              -- get the `userName` in the player's local context.
+              let name₂ := (lctx.get! fvar₂).userName
+              varNames := varNames.push (name₁, name₂)
+
+            return some {
+              text := text,
+              hidden := hint.hidden,
+              rawText := hint.rawText,
+              varNames := varNames }
+
           else return none
         else
           return none
     return hints
 
+def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
+    Array InteractiveDiagnostic :=
+  a.filter (fun d => match d.message with
+  | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
+  | _ => true)
+
 -- TODO: no need to have `RequestM`, just anything where `mut` works
 /-- Add custom diagnostics about whether the level is completed. -/
 def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : Bool)
@@ -144,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
@@ -152,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
@@ -161,21 +192,20 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
     else
       pure ()
   else if goalCount < prevGoalCount then
-    out := out.push {
-      message := .text "intermediate goal solved! 🎉"
-      range := {
-        start := pos
-        «end» := pos
-        }
-      severity? := Lsp.DiagnosticSeverity.information
-    }
+    -- If there is any errors, goals might vanish without being 'solved'
+    -- so showing the message "intermediate goal solved" would be confusing.
+    if (¬ (filterUnsolvedGoal startDiags).any (·.severity? == some .error)) then
+      out := out.push {
+        message := .text t!"intermediate goal solved! 🎉"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information
+      }
+
   return out
 
-def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
-    Array InteractiveDiagnostic :=
-  a.filter (fun d => match d.message with
-  | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
-  | _ => true)
 
 /-- Request that returns the goals at the end of each line of the tactic proof
 plus the diagnostics (i.e. warnings/errors) for the proof.
@@ -185,9 +215,6 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo
   let rc ← readThe RequestContext
   let text := doc.meta.text
 
-  -- BUG: trimming here is a problem, since the snap might already be evaluated before
-  -- the trimming and then the positions don't match anymore :((
-
   withWaitFindSnap
     doc
     -- TODO (Alex): I couldn't find a good condition to find the correct snap. So we are looking

server/GameServer/SaveData.lean

@@ -1,8 +1,8 @@
 import GameServer.EnvExtensions
+import I18n
 
 open Lean Meta Elab Command
 
-
 /-! ## Copy images -/
 
 open IO.FS System FilePath in
@@ -59,6 +59,9 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
 
   IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
 
+  -- write file for translation
+  I18n.createTemplate
+
 open GameData
 
 def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do

server/GameServer/Structures.lean

@@ -54,8 +54,17 @@ deriving RpcEncodable
 
 /-- A hint in the game at the corresponding goal. -/
 structure GameHint where
+  /-- The text with the variable names already inserted.
+
+  Note: This is in theory superfluous and will be completely replaced by `rawText`. We just left
+  it in for debugging for now. -/
   text : String
+  /-- Flag whether the hint should be hidden initially. -/
   hidden : Bool
+  /-- The text with the variables not inserted yet. -/
+  rawText : String
+  /-- The assignment of variable names in the `rawText` to the ones the player used. -/
+  varNames : Array <| Name × Name
 deriving FromJson, ToJson
 
 /-- Bundled `InteractiveGoal` together with an array of hints that apply at this stage. -/

server/GameServer/Tactic/LetIntros.lean

@@ -0,0 +1,67 @@
+import Lean.Elab.Binders
+import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Intro
+
+/-!
+# `let_intros` Tactic
+
+`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
+
+open Lean Meta Elab Parser Tactic
+
+/--
+Copied from `Lean.Meta.getIntrosSize`.
+-/
+private partial def getLetIntrosSize : Expr → Nat
+  -- | .forallE _ _ b _ => getLetIntrosSize b + 1
+  | .letE _ _ _ b _  => getLetIntrosSize b + 1
+  | .mdata _ b       => getLetIntrosSize b
+  | e                =>
+    if let some (_, _, _, b) := e.letFun? then
+      getLetIntrosSize b + 1
+    else
+      0
+
+/--
+Copied and from `Lean.MVarId.intros`.
+-/
+def _root_.Lean.MVarId.letIntros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
+  let type ← mvarId.getType
+  let type ← instantiateMVars type
+  let n := getLetIntrosSize type
+  if n == 0 then
+    return (#[], mvarId)
+  else
+    -- `introNP` preserves the binder names
+    mvarId.introNP n
+
+/--
+`let_intros` introduces all `let` statements that are preceeding 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.
+-/
+syntax (name := letIntros) "let_intros" : tactic
+-- (ppSpace colGt (ident <|> hole))*
+
+@[tactic letIntros] def evalLetIntros : Tactic := fun stx => do
+  match stx with
+  | `(tactic| let_intros) => liftMetaTactic fun mvarId => do
+    let (_, mvarId) ← mvarId.letIntros
+    return [mvarId]
+  -- | `(tactic| let_intros $ids*) => do
+  --   let fvars ← liftMetaTacticAux fun mvarId => do
+  --     let (fvars, mvarId) ← mvarId.introN ids.size (ids.map getNameOfIdent').toList
+  --     return (fvars, [mvarId])
+  --   withMainContext do
+  --     for stx in ids, fvar in fvars do
+  --       Term.addLocalVarInfo stx (mkFVar fvar)
+  | _ => throwUnsupportedSyntax

server/lake-manifest.json

@@ -4,10 +4,37 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.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": "7550f08140c59c9a604bbcc23ab7830c103a3e39",
+   "name": "i18n",
+   "manifestFile": "lake-manifest.json",
+   "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

@@ -7,8 +7,10 @@ package GameServer
 def leanVersion : String := s!"v{Lean.versionString}"
 
 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
 
--- require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
 
 lean_lib GameServer
 

server/lean-toolchain

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

server/test/let_intros.lean

@@ -0,0 +1,17 @@
+import GameServer.Tactic.LetIntros
+
+set_option linter.unusedVariables false in
+
+example (f : Nat) :
+    let f := fun x ↦ x + 1
+    let g : Nat → Nat := fun y ↦ y
+    ∀ x : Nat, x ≤ f x := by
+  let_intros
+  /-
+  f✝ : Nat
+  f : Nat → Nat := fun x => x + 1
+  g : Nat → Nat := fun y => y
+  ⊢ ∀ (x : Nat), x ≤ f x
+  -/
+  intro x
+  exact Nat.le_succ x

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
-  rw [Nat.add_comm]
+Statement My.add_assoc (n m x : Nat) : (m + n) + x = m + (n + x) := by
+  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]

tsconfig.json

@@ -11,6 +11,10 @@
     "downlevelIteration": true,
     "experimentalDecorators": true,
     "allowSyntheticDefaultImports": true,
+    "lib": [
+      "ES2021.String",
+      "DOM"
+    ]
   },
   "exclude": ["server", "relay"]
 }

vite.config.ts

@@ -44,6 +44,9 @@ export default defineConfig({
       '/data': {
         target: 'http://localhost:8080',
       },
+      '/i18n': {
+        target: 'http://localhost:8080',
+      },
     }
   },
   resolve: {