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}}>
+          <PreferencesContext.Provider value={{mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage}}>
-            <Outlet />
+            <React.Suspense>
+              <Outlet />
+            </React.Suspense>
           </PreferencesContext.Provider>
       </GameIdContext.Provider>
     </div>

client/src/components/app_bar.tsx

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

client/src/components/hints.tsx

@@ -1,22 +1,46 @@
-import { GameHint } from "./infoview/rpc_api";
+import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
 import * as React from 'react';
 import Markdown from './markdown';
-import { ProofStep } from "./infoview/context";
+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>
 }
 
 export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
-
+  if (!hints) {return <></>}
   const openHints = hints.filter(hint => !hint.hidden)
   const hiddenHints = hints.filter(hint => hint.hidden)
 
@@ -29,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>
 }
 
@@ -46,22 +70,56 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
 }
 
 /** Filter hints to not show consequtive identical hints twice.
- *
+ * Hidden hints are not filtered.
- * This function takes a `ProofStep[]` and extracts the hints in form of an
- * element of type `GameHint[][]` where it removes hints that are identical to hints
- * appearing in the previous step. Hidden hints are not filtered.
- *
- * This effectively means we prevent consequtive identical hints from being shown.
  */
-export function filterHints(proof: ProofStep[]): GameHint[][] {
+export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
-  return proof.map((step, i) => {
+  if (!hints) {
-    if (i == 0){
+    return []}
-      return step.hints
+  else if (!prevHints) {
-    } else {
+    return hints }
-      // TODO: Writing all fields explicitely is somewhat fragile to changes, is there a
+  else {
-      // good way to shallow-compare objects?
+    return hints.filter((hint) => hint.hidden ||
-      return step.hints.filter((hint) => hint.hidden ||
+    (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
-        (proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined))
+    )
-    }
+  }
-  })
+}
+
+
+function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
+  return step?.goals[0]?.hints.some((hint) => hint.hidden)
+}
+
+
+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 = 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}
+
+    // state must not be mutated, therefore we need to clone the set
+    let tmp = new Set(showHelp)
+    if (tmp.has(k)) {
+      tmp.delete(k)
+    } else {
+      tmp.add(k)
+    }
+    setShowHelp(tmp)
+    console.debug(`help: ${Array.from(tmp.values())}`)
+  }
+
+  if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
+    return <Button to="" onClick={activateHiddenHints}>
+      {t("Show more help!")}
+    </Button>
+  }
 }

client/src/components/infoview/context.ts

@@ -3,8 +3,9 @@
  */
 import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api';
+import { InteractiveDiagnostic } from '@leanprover/infoview-api';
-import { GameHint, InteractiveGoal, InteractiveGoals } from './rpc_api';
+import { Diagnostic } from 'vscode-languageserver-types'
+import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { PreferencesState } from '../../state/preferences';
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
@@ -12,37 +13,49 @@ export const MonacoEditorContext = React.createContext<monaco.editor.IStandalone
 
 export type InfoStatus = 'updating' | 'error' | 'ready';
 
-/** One step of the proof */
+// /** One step of the proof */
-export type ProofStep = {
+// export type ProofStep = {
-  /** The command in this step */
+//   /** The command in this step */
-  command : string
+//   command : string
-  /** List of goals *after* this command */
+//   /** List of goals *after* this command */
-  goals: InteractiveGoal[]     // TODO: Add correct type
+//   goals: InteractiveGoal[]     // TODO: Add correct type
-  /** Story relevant messages */
+//   /** Story relevant messages */
-  hints: GameHint[]        // TODO: Add correct type
+//   hints: GameHint[]        // TODO: Add correct type
-  /** Errors and warnings */
+//   /** Errors and warnings */
-  errors: InteractiveDiagnostic[]       // TODO: Add correct type
+//   errors: InteractiveDiagnostic[]       // TODO: Add correct type
-}
+// }
 
 /** The context storing the proof step-by-step for the command line mode */
 export const ProofContext = React.createContext<{
   /** The proof consists of multiple steps that are processed one after the other.
    * In particular multi-line terms like `match`-statements will not be supported.
    *
-   * Note that the first step will always have `null` as command
+   * Note that the first step will always have "" as command
    */
-  proof: ProofStep[],
+  proof: ProofState,
-  setProof: React.Dispatch<React.SetStateAction<Array<ProofStep>>>
+  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: [],
+  proof: {steps: [], diagnostics: [], completed: false, completedWithWarnings: false},
-  setProof: () => {} // TODO: implement me
+  setProof: () => {},
+  interimDiags: [],
+  setInterimDiags: () => {},
+  crashed: false,
+  setCrashed: () => {}
 })
 
+
+// TODO: Do we still need that?
 export interface ProofStateProps {
   // pos: DocumentPosition;
   status: InfoStatus;
   messages: InteractiveDiagnostic[];
-  goals?: InteractiveGoals;
+  goals?: InteractiveGoalsWithHints;
   termGoal?: InteractiveTermGoal;
   error?: string;
   // userWidgets: UserWidgetInstance[];
@@ -50,31 +63,34 @@ export interface ProofStateProps {
   // triggerUpdate: () => Promise<void>;
 }
 
-export const ProofStateContext = React.createContext<{
+// export const ProofStateContext = React.createContext<{
-  proofState : ProofStateProps,
+//   proofState : ProofStateProps,
-  setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
+//   setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
-}>({
+// }>({
-  proofState : {
+//   proofState : {
-    status: 'updating',
+//     status: 'updating',
-    messages: [],
+//     messages: [],
-    goals: undefined,
+//     goals: undefined,
-    termGoal: undefined,
+//     termGoal: undefined,
-    error: undefined},
+//     error: undefined},
-  setProofState: () => {},
+//   setProofState: () => {},
-})
+// })
 
 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<{
@@ -112,13 +128,13 @@ export const InputModeContext = React.createContext<{
   setTypewriterMode: React.Dispatch<React.SetStateAction<boolean>>,
   typewriterInput: string,
   setTypewriterInput: React.Dispatch<React.SetStateAction<string>>,
-  lockInputMode: boolean,
+  lockEditorMode: boolean,
-  setLockInputMode: React.Dispatch<React.SetStateAction<boolean>>,
+  setLockEditorMode: React.Dispatch<React.SetStateAction<boolean>>,
 }>({
   typewriterMode: true,
   setTypewriterMode: () => {},
   typewriterInput: "",
   setTypewriterInput: () => {},
-  lockInputMode: false,
+  lockEditorMode: false,
-  setLockInputMode: () => {},
+  setLockEditorMode: () => {},
 });

client/src/components/infoview/goals.tsx

@@ -10,7 +10,11 @@ import { Locations, LocationsContext, SelectableLocation } from '../../../../nod
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
 import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
 import { InputModeContext } from './context';
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api';
+import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api';
+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 {
@@ -39,7 +43,11 @@ function goalToString(g: InteractiveGoal): string {
 }
 
 export function goalsToString(goals: InteractiveGoals): string {
-    return goals.goals.map(goalToString).join('\n\n')
+    return goals.goals.map(g => goalToString(g)).join('\n\n')
+}
+
+export function goalsWithHintsToString(goals: InteractiveGoalsWithHints): string {
+    return goals.goals.map(g => goalToString(g.goal)).join('\n\n')
 }
 
 interface GoalFilterState {
@@ -127,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 <></>}
@@ -150,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>
@@ -163,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]
@@ -195,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>
@@ -205,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>
@@ -235,36 +239,17 @@ 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: InteractiveGoals
+    goals: InteractiveGoalsWithHints
     filter: GoalFilterState
 }
 
 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} filter={filter} />)}
+          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
         </>
     }
 }
@@ -276,7 +261,7 @@ interface FilteredGoalsProps {
      * When this is `undefined`, the component will not appear at all but will remember its state
      * by virtue of still being mounted in the React tree. When it does appear again, the filter
      * settings and collapsed state will be as before. */
-    goals?: InteractiveGoals
+    goals?: InteractiveGoalsWithHints
 }
 
 /**
@@ -291,7 +276,7 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
             data-id="copy-goal-to-comment"
             onClick={e => {
                 e.preventDefault();
-                if (goals) void ec.copyToComment(goalsToString(goals))
+                if (goals) void ec.copyToComment(goalsWithHintsToString(goals))
             }}
             title="copy state to comment" />
 
@@ -336,3 +321,45 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
         </details>
     </div>
 })
+
+export function loadGoals(
+  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) => {
+    if (typeof proof !== 'undefined') {
+      console.info(`received a proof state!`)
+      console.log(proof)
+      setProof(proof)
+      setCrashed(false)
+    } else {
+      console.warn('received undefined proof state!')
+      setCrashed(true)
+      // setProof(undefined)
+    }
+  }
+).catch((error) => {
+  setCrashed(true)
+  console.warn(error)
+})
+}
+
+
+export function lastStepHasErrors (proof : ProofState): boolean {
+  if (!proof?.steps.length) {return false}
+
+  let diags = [...proof.steps[proof.steps.length - 1].diags, ...proof.diagnostics]
+
+  return diags.some(
+    (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
+  )
+}
+
+export function isLastStepWithErrors (proof : ProofState, i: number): boolean {
+  if (!proof?.steps.length) {return false}
+  return (i == proof.steps.length - 1) && lastStepHasErrors(proof)
+}

client/src/components/infoview/info.tsx

@@ -4,7 +4,7 @@ import * as React from 'react'
 import { CircularProgress } from '@mui/material'
 import type { Location, Diagnostic } from 'vscode-languageserver-protocol'
 import { getInteractiveTermGoal, InteractiveDiagnostic, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
-  RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api'
+  RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api'
 import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
   mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util'
 import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'
@@ -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 { InteractiveGoals } from './rpc_api'
+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'
@@ -83,11 +84,12 @@ interface InfoDisplayContentProps extends PausableProps {
   error?: string
   userWidgets: UserWidgetInstance[]
   triggerUpdate: () => Promise<void>
-  proof? : string
+  proofString? : string
 }
 
 const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
-    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proof} = props
+    let { t } = useTranslation()
+    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props
 
     const hasWidget = userWidgets.length > 0
     const hasError = !!error
@@ -114,7 +116,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
 
     const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
-    return <>
+
+   return <>
         {hasError &&
             <div className='error' key='errors'>
                 Error updating:{' '}{error}.
@@ -130,14 +133,14 @@ 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>
         {userWidgets.map(widget =>
           <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
             <summary className='mv2 pointer'>{widget.name}</summary>
-            <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals.map (goal => goal) : []}
+            <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []}
               termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
           </details>
         )}
@@ -149,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">
@@ -166,6 +169,7 @@ interface InfoDisplayProps {
   pos: DocumentPosition,
   status: InfoStatus,
   messages: InteractiveDiagnostic[],
+  proof?: ProofState,
   goals?: InteractiveGoals,
   termGoal?: InteractiveTermGoal,
   error?: string,
@@ -175,7 +179,7 @@ interface InfoDisplayProps {
 }
 
 /** Displays goal state and messages. Can be paused. */
-function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable) {
+function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
     // Used to update the paused state *just once* if it is paused,
     // but a display update is triggered
     const [shouldRefresh, setShouldRefresh] = React.useState<boolean>(false)
@@ -214,7 +218,7 @@ function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable)
     {/* <details open> */}
         {/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
         <div className="vscode-light">
-            <InfoDisplayContent {...props} proof={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
+            <InfoDisplayContent {...props} proofString={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
         </div>
     {/* </details> */}
     </RpcContext.Provider>
@@ -252,7 +256,7 @@ function useIsProcessingAt(p: DocumentPosition): boolean {
 
 function InfoAux(props: InfoProps) {
 
-    const proofContext = React.useContext(ProofContext)
+    const { setProof } = React.useContext(ProofContext)
 
     const config = React.useContext(ConfigContext)
 
@@ -290,6 +294,10 @@ function InfoAux(props: InfoProps) {
     // with e.g. a new `pos`.
     type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'>
     const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((resolve, reject) => {
+
+        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)
@@ -308,6 +316,7 @@ function InfoAux(props: InfoProps) {
                 pos,
                 status: 'updating',
                 messages: lspDiagsHere.map(lspDiagToInteractive),
+                proof: undefined,
                 goals: undefined,
                 termGoal: undefined,
                 error: undefined,
@@ -318,11 +327,12 @@ function InfoAux(props: InfoProps) {
 
         // NB: it is important to await await reqs at once, otherwise
         // if both throw then one exception becomes unhandled.
-        Promise.all([goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
+        Promise.all([proofReq, goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
-            ([goals, termGoal, userWidgets, messages]) => resolve({
+            ([proof, goals, termGoal, userWidgets, messages]) => resolve({
                 pos,
                 status: 'ready',
                 messages,
+                proof : proof as any,
                 goals: goals as any,
                 termGoal,
                 error: undefined,
@@ -353,6 +363,7 @@ function InfoAux(props: InfoProps) {
                     pos,
                     status: 'error',
                     messages: lspDiagsHere.map(lspDiagToInteractive),
+                    proof: undefined,
                     goals: undefined,
                     termGoal: undefined,
                     error: `Error fetching goals: ${errorString}`,
@@ -389,6 +400,7 @@ function InfoAux(props: InfoProps) {
         pos,
         status: 'updating',
         messages: [],
+        proof: undefined,
         goals: undefined,
         termGoal: undefined,
         error: undefined,
@@ -412,6 +424,11 @@ function InfoAux(props: InfoProps) {
           //   hintContext.setHints(state.value.goals.goals[0].hints)
           // }
           setDisplayProps({ ...state.value, triggerUpdate })
+
+          // Update the game's proof state
+          console.info('updating proof from editor mode.')
+          setProof(state.value.proof)
+
         } else if (state.state === 'rejected' && state.error !== 'retry') {
             // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception.
             console.warn('Unreachable code reached with error: ', state.error)

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,30 +20,35 @@ 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';
 
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
-import { Goal } from './goals';
+import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals';
-import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
-import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
+import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
-import { GameHint } from './rpc_api';
+import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { store } from '../../state/store';
-import { Hints, filterHints } from '../hints';
+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>
@@ -59,38 +64,37 @@ 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)
 
-  // Mark level as completed when server gives notification
   const dispatch = useAppDispatch()
-  useServerNotificationEffect(
-    '$/game/completed',
-    (params: any) => {
-      if (ec.events.changedCursorLocation.current &&
-          ec.events.changedCursorLocation.current.uri === params.uri) {
-        dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
 
-        // On completion, add the names of all new items to the local storage
+  React.useEffect(() => {
-        let newTiles = [
+    if (proof?.completed) {
-          ...level?.tactics,
+      dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
-          ...level?.lemmas,
-          ...level?.definitions
-        ].filter((tile) => tile.new).map((tile) => tile.name)
 
-        // Add the proven statement to the local storage as well.
+      // On completion, add the names of all new items to the local storage
-        if (level?.statementName != null) {
+      let newTiles = [
-          newTiles.push(level?.statementName)
+        ...level?.tactics,
-        }
+        ...level?.lemmas,
+        ...level?.definitions
+      ].filter((tile) => tile.new).map((tile) => tile.name)
 
-        let inv: string[] = selectInventory(gameId)(store.getState())
+      // Add the proven statement to the local storage as well.
-
+      if (level?.statementName != null) {
-        // add new items and remove duplicates
+        newTiles.push(level?.statementName)
-        let newInv = [...inv, ...newTiles].filter((item, i, array) => array.indexOf(item) == i)
-
-        dispatch(changedInventory({ game: gameId, inventory: newInv }))
       }
-    }, [level]
+
-  )
+      let inv: string[] = selectInventory(gameId)(store.getState())
+
+      // add new items and remove duplicates
+      let newInv = [...inv, ...newTiles].filter((item, i, array) => array.indexOf(item) == i)
+
+      dispatch(changedInventory({ game: gameId, inventory: newInv }))
+
+    }
+  }, [proof, level])
 
   /* Set up updates to the global infoview state on editor events. */
   const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
@@ -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,12 +157,26 @@ 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)
 
-  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
+  const { proof, setProof } = React.useContext(ProofContext)
+  const {selectedStep, setSelectedStep} = React.useContext(SelectionContext)
+  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
 
+
+  function toggleSelection(line: number) {
+    return (ev) => {
+      console.debug('toggled selection')
+      if (selectedStep == line) {
+        setSelectedStep(undefined)
+      } else {
+        setSelectedStep(line)
+      }
+    }
+  }
   console.debug(`template: ${props.data?.template}`)
 
   // React.useEffect (() => {
@@ -182,6 +203,19 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
 
   const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
 
+  const curPos: DocumentPosition | undefined =
+    useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined)
+
+  // Effect when the cursor changes in the editor
+  React.useEffect(() => {
+    // TODO: this is a bit of a hack and will yield unexpected behaviour if lines
+    // are indented.
+    let newPos = curPos?.line + (curPos?.character == 0 ? 0 : 1)
+
+    // scroll the chat along
+    setSelectedStep(newPos)
+  }, [curPos])
+
   useClientNotificationEffect(
     'textDocument/didClose',
     (params: DidCloseTextDocumentParams) => {
@@ -201,13 +235,22 @@ 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">
-      {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}
+        showHidden={showHelp.has(curPos?.line)} step={curPos?.line}
+        selected={selectedStep} toggleSelection={toggleSelection(curPos?.line)}
+        lastLevel={curPos?.line == proof?.steps.length - 1}/>
+      <MoreHelpButton selected={curPos?.line}/>
     </div>
   }
 
@@ -223,15 +266,26 @@ const goalFilter = {
 }
 
 /** The display of a single entered lean command */
-function Command({ command, deleteProof }: { command: string, deleteProof: any }) {
+function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) {
+  let {t} = useTranslation()
+
   // The first step will always have an empty command
-  if (!command) { return <></> }
+  if (!proof?.steps[i]?.command) { return <></> }
-  return <div className="command">
+
-    <div className="command-text">{command}</div>
+  if (isLastStepWithErrors(proof, i)) {
-    <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
+    // If the last step has errors, we display the command in a different style
-      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
+    // indicating that it will be removed on the next try.
-    </Button>
+    return <div className="failed-command">
-  </div>
+      <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={t("Retry proof from here")} onClick={deleteProof}>
+        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;{t("Retry")}
+      </Button>
+    </div>
+  }
 }
 
 // const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
@@ -286,21 +340,25 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 // }, fastIsEqual)
 
 /** The tabs of goals that lean ahs after the command of this step has been processed */
-function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: ProofStep, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
+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) {
+    return <></>
+  }
+
   return <div className="goal-tabs" onClick={onClick}>
     <div className={`tab-bar ${last ? 'current' : ''}`}>
       {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>
     <div className="goal-tab vscode-light">
-      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
+      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]?.goal} />
     </div>
   </div>
 }
@@ -340,22 +398,27 @@ 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 } = React.useContext(ProofContext)
+  const { proof, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext)
   const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
-  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
   // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
   // const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
 
@@ -367,12 +430,17 @@ export function TypewriterInterface({props}) {
   function deleteProof(line: number) {
     return (ev) => {
       let deletedChat: Array<GameHint> = []
-      filterHints(proof).slice(line).map((hintsAtStep, 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
-        deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+        deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
       })
       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 },
@@ -382,7 +450,9 @@ export function TypewriterInterface({props}) {
         forceMoveMarkers: false
       }])
       setSelectedStep(undefined)
-      setTypewriterInput(proof[line].command)
+      setTypewriterInput(proof?.steps[line].command)
+      // Reload proof on deleting
+      loadGoals(rpcSess, uri, setProof, setCrashed)
       ev.stopPropagation()
     }
   }
@@ -402,7 +472,7 @@ export function TypewriterInterface({props}) {
 
    // Scroll to the end of the proof if it is updated.
    React.useEffect(() => {
-    if (proof?.length > 1) {
+    if (proof?.steps.length > 1) {
       proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
     } else {
       proofPanelRef.current?.scrollTo(0,0)
@@ -423,38 +493,8 @@ export function TypewriterInterface({props}) {
     }
   }, [selectedStep])
 
-  // TODO: This about hidden hints is all copied from `level.tsx`. Can we move that into `hints.tsx`?
+  // TODO: superfluous, can be replaced with `withErr` from above
-
+  let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false
-  // If the last step has errors, we want to treat it as if it is part of the second-to-last step
-  let k = proof.length - 1
-  let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 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.length)) {return}
-
-    // state must not be mutated, therefore we need to clone the set
-    let tmp = new Set(showHelp)
-    if (tmp.has(k - withErr)) {
-      tmp.delete(k - withErr)
-    } else {
-      tmp.add(k - withErr)
-    }
-    setShowHelp(tmp)
-    console.debug(`help: ${Array.from(tmp.values())}`)
-  }
-
-  function hasHiddenHints(i : number): boolean {
-    let step = proof[i]
-
-    // For example if the proof isn't loaded yet
-    if(!step) {return false}
-
-    return step.hints.some((hint) => hint.hidden)
-  }
-
-  let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
 
 
   useServerNotificationEffect("$/game/loading", (params : any) => {
@@ -470,24 +510,55 @@ 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.length ?
+        {crashed ? <div>
-          <>
+          <p className="crashed_message">{t("Crashed! Go to editor mode and fix your proof! Last server response:")}</p>
-            {proof.map((step, i) => {
+          {interimDiags.map(diag => {
-              if (i == proof.length - 1 && lastStepErrors) {
+            const severityClass = diag.severity ? {
-                // if the last command contains an error, we only display the errors but not the
+              [DiagnosticSeverity.Error]: 'error',
-                // entered command as it is still present in the command line.
+              [DiagnosticSeverity.Warning]: 'warning',
-                // TODO: Should not use index as key.
+              [DiagnosticSeverity.Information]: 'information',
-                return <div key={`proof-step-${i}`}>
+              [DiagnosticSeverity.Hint]: 'hint',
-                  <Errors errors={step.errors} typewriterMode={true} />
+            }[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>
-              } else {
+            </div>
+          })}
+
+        </div> : proof?.steps.length ?
+          <>
+            {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 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.
+              //   return <div key={`proof-step-${i}`} className={`step step-${i}`}>
+              //     <Errors errors={step.diags} typewriterMode={true} />
+              //   </div>
+              // } else {
                 return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
-                  <Command command={step.command} deleteProof={deleteProof(i)} />
+                  <Command proof={proof} i={i} deleteProof={deleteProof(i)} />
-                  <Errors errors={step.errors} typewriterMode={true} />
+                  <Errors errors={step.diags} typewriterMode={true} />
                   {mobile && i == 0 && props.data?.introduction &&
                     <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
                       <Markdown>{props.data?.introduction}</Markdown>
@@ -495,22 +566,21 @@ export function TypewriterInterface({props}) {
                   }
                   {mobile &&
                     <Hints key={`hints-${i}`}
-                      hints={step.hints} showHidden={showHelp.has(i)} step={i}
+                      hints={filteredHints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
                   }
-                  <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.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)) &&
-                  {mobile && i == proof.length - 1 &&
+                    <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) => {}}/>
-                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+                  }
-                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
+                  {mobile && i == proof?.steps.length - 1 &&
-                      Show more help!
+                    <MoreHelpButton />
-                    </Button>
                   }
 
                   {/* Show a message that there are no goals left */}
-                  {!step.goals.length && (
+                  {/* {!step.goals.length && (
                     <div className="message information">
-                      {completed ?
+                      {proof?.completed ?
                         <p>Level completed! 🎉</p> :
                         <p>
                           <b>no goals left</b><br />
@@ -518,15 +588,21 @@ export function TypewriterInterface({props}) {
                         </p>
                       }
                     </div>
-                  )}
+                  )} */}
                 </div>
               }
-            })}
+            //}
-            {mobile && completed &&
+            )}
+            {proof?.diagnostics.length > 0 &&
+              <div key={`proof-step-remaining`} className="step step-remaining">
+                <Errors errors={proof?.diagnostics} typewriterMode={true} />
+              </div>
+            }
+            {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}`}>
@@ -535,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 hidden={!withErr && proof[proof.length - 1]?.goals.length == 0} disabled={disableInput || !proof.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>
@@ -194,17 +195,26 @@ export function AllMessages() {
                 </a>
             </span>
         </summary> */}
-        <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} />
+        <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} curPos={curPos} />
     {/* </Details> */}
     </RpcContext.Provider>
     )
 }
 
 /** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */
-function AllMessagesBody({uri, messages}: {uri: DocumentUri, messages: () => Promise<InteractiveDiagnostic[]>}) {
+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(setMsgs) }, [messages])
+    React.useEffect(() => { void messages().then(
-    if (msgs === undefined) return <div>Loading messages...</div>
+        msgs => setMsgs(msgs.filter(
+            (d)=>{
+                //console.log(`message start: ${d.range.start.line}. CurPos: ${curPos.line}`)
+
+                // Only show the messages from the line where the cursor is.
+                return d.range.start.line == curPos.line
+            }))
+    ) }, [messages, curPos])
+    if (msgs === undefined) return <div>{t("Loading messages…")}</div>
     else return <MessagesList uri={uri} messages={msgs}/>
 }
 

client/src/components/infoview/rpc_api.ts

@@ -3,46 +3,82 @@
  *
  * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts`
  */
-import { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
+import type { Range } from 'vscode-languageserver-protocol';
-
+import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
-export interface GameHint {
+import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*';
-  text: string;
+import type { Diagnostic } from 'vscode-languageserver-protocol';
-  hidden: boolean;
-}
 
 export interface InteractiveHypothesisBundle {
   /** The pretty names of the variables in the bundle. Anonymous names are rendered
    * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
    * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
   names: string[];
-  /** Present since server version 1.1.2. */
   fvarIds?: FVarId[];
   type: CodeWithInfos;
   val?: CodeWithInfos;
   isInstance?: boolean;
   isType?: boolean;
-  isAssumption?: boolean;
   isInserted?: boolean;
   isRemoved?: boolean;
+  isAssumption?: boolean;
 }
 
 export interface InteractiveGoalCore {
   hyps: InteractiveHypothesisBundle[];
   type: CodeWithInfos;
-  /** Present since server version 1.1.2. */
   ctx?: ContextInfo;
 }
 
 export interface InteractiveGoal extends InteractiveGoalCore {
   userName?: string;
   goalPrefix?: string;
-  /** Present since server version 1.1.2. */
   mvarId?: MVarId;
   isInserted?: boolean;
   isRemoved?: boolean;
+}
+
+export interface InteractiveGoals extends InteractiveGoalCore {
+  goals: InteractiveGoals[];
+}
+
+export interface InteractiveTermGoal extends InteractiveGoalCore {
+  range?: Range;
+  term?: TermInfo;
+}
+
+export interface GameHint {
+  text: string;
+  hidden: boolean;
+  rawText: string;
+  varNames: string[][]; // in Lean: `Array (Name × Name)`
+}
+
+export interface InteractiveGoalWithHints {
+  goal: InteractiveGoal;
   hints: GameHint[];
 }
 
-export interface InteractiveGoals {
+export interface InteractiveGoalsWithHints {
-  goals: InteractiveGoal[];
+  goals: InteractiveGoalWithHints[];
+  command: string;
+  diags: InteractiveDiagnostic[];
+}
+
+/**
+ * The proof state as it is received from the server.
+ * Per proof step of the tactic proof, there is one `InteractiveGoalWithHints[]`.
+ */
+export interface ProofState {
+  /** The proof steps. step 0 is the state at the beginning of the proof. step one
+   * contains the goal after the first line has been evaluated.
+   *
+   * In particular `step[i]` is the proof step at the beginning of line `i` in vscode.
+   */
+  steps: InteractiveGoalsWithHints[];
+  /** The remaining diagnostics that are not in the steps. Usually this should only
+   * be the "unsolved goals" message, I believe.
+   */
+  diagnostics : InteractiveDiagnostic[];
+  completed : Boolean;
+  completedWithWarnings : Boolean;
 }

client/src/components/infoview/typewriter.tsx

@@ -5,7 +5,7 @@ import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { Registry } from 'monaco-textmate' // peer dependency
 import { wireTmGrammars } from 'monaco-editor-textmate'
-import { DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol';
+import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol';
 import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
@@ -13,13 +13,19 @@ import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json'
 import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json'
 import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json'
 import languageConfig from 'lean4/language-configuration.json';
-import { InteractiveDiagnostic, getInteractiveDiagnostics } from '@leanprover/infoview-api';
+import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } from '@leanprover/infoview-api';
 import { Diagnostic } from 'vscode-languageserver-types';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context'
+import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext } from './context'
-import { goalsToString } from './goals'
+import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
-import { GameHint, InteractiveGoals } from './rpc_api'
+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. */
 
@@ -64,7 +70,8 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 /** The input field */
-export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boolean}) {
+export function Typewriter({disabled}: {disabled?: boolean}) {
+  let { t } = useTranslation()
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
@@ -79,109 +86,13 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   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 : InteractiveGoals[]) => {
-      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.goals.length && goalCount > goals.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.goals.length
-
-          // with no goals there will be no hints.
-          let hints : GameHint[] = goals.goals.length ? goals.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.goals,
-            // 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}
@@ -201,6 +112,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
         forceMoveMarkers: false
       }])
       setTypewriterInput('')
+      // Load proof after executing edits
+      loadGoals(rpcSess, uri, setProof, setCrashed)
     }
 
     editor.setPosition(pos)
@@ -212,9 +125,15 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     }
   }, [typewriterInput])
 
+  /* Load proof on start/switching to typewriter */
   useEffect(() => {
-    if (proof.length && hasInteractiveErrors(proof[proof.length - 1].errors)) {
+    loadGoals(rpcSess, uri, setProof, setCrashed)
-      setTypewriterInput(proof[proof.length - 1].command)
+  }, [])
+
+  /** 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)
     }
   }, [proof])
 
@@ -222,7 +141,14 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == uri) {
       setProcessing(false)
-      loadAllGoals()
+
+      console.log('Received lean diagnostics')
+      console.log(params.diagnostics)
+      setInterimDiags(params.diagnostics)
+
+      //loadGoals(rpcSess, uri, setProof)
+
+      // TODO: loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
         //setTypewriterInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
@@ -236,6 +162,15 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     // 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)
+
+  // }, [uri]);
+
+
   useEffect(() => {
     const myEditor = monaco.editor.create(inputRef.current!, {
       value: typewriterInput,
@@ -306,7 +241,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   useEffect(() => {
     console.debug(`time to update: ${uri} \n ${rpcSess}`)
     console.debug(rpcSess)
-    loadAllGoals()
+    // console.debug('LOAD ALL GOALS')
+    // TODO: loadAllGoals()
   }, [rpcSess])
 
   /** Process the entered command */
@@ -315,13 +251,14 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     runCommand()
   }
 
-  return <div className={`typewriter${hidden ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
+  // do not display if the proof is completed (with potential warnings still present)
+  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>
@@ -343,3 +280,14 @@ export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
     (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
   )
 }
+
+export function getInteractiveDiagsAt (proof: ProofState, k : number) {
+  if (k == 0) {
+    return []
+  } 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)
+  } else {
+    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" :
+  const title = locked ? t("Not unlocked yet") :
-                disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
+                disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
 
   const [copied, setCopied] = useState(false)
 
@@ -137,7 +140,7 @@ export function Documentation({name, type, handleClose}) {
     <h1 className="doc">{doc.data?.displayName}</h1>
     <p><code>{doc.data?.statement}</code></p>
     {/* <code>docstring: {doc.data?.docstring}</code> */}
-    <Markdown>{doc.data?.content}</Markdown>
+    <Markdown>{t(doc.data?.content, {ns: gameId})}</Markdown>
   </div>
 }
 

client/src/components/landing_page.tsx

@@ -1,5 +1,6 @@
 import * as React from 'react';
 import { useNavigate, Link } from "react-router-dom";
+import { Trans, useTranslation } from 'react-i18next';
 
 import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
@@ -14,14 +15,11 @@ import {PrivacyPolicyPopup} from './popup/privacy_policy'
 import { GameTile, useGetGameInfoQuery } from '../state/api'
 import path from 'path';
 
-const flag = {
+import { PreferencesPopup } from './popup/preferences';
-  'Dutch': '🇳🇱',
+import { ImpressumButton, MenuButton, PreferencesButton } from './app_bar';
-  'English': '🇬🇧',
+import ReactCountryFlag from 'react-country-flag';
-  'French': '🇫🇷',
+import lean4gameConfig from '../config.json'
-  'German': '🇩🇪',
+import i18next from 'i18next';
-  'Italian': '🇮🇹',
-  'Spanish': '🇪🇸',
-}
 
 function GithubIcon({url='https://github.com'}) {
 
@@ -35,7 +33,7 @@ function GithubIcon({url='https://github.com'}) {
 }
 
 function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
-
+  let { t } = useTranslation()
   let navigate = useNavigate();
   const routeChange = () =>{
     navigate(gameId);
@@ -47,29 +45,36 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
 
   return <div className="game" onClick={routeChange}>
     <div className="wrapper">
-      <div className="title">{data.title}</div>
+      <div className="title">{t(data.title, { ns: gameId })}</div>
-      <div className="short-description">{data.short}
+      <div className="short-description">{t(data.short, { ns: gameId })}
       </div>
       { data.image ? <img className="image" src={path.join("data", gameId, data.image)} alt="" /> : <div className="image"/> }
-      <div className="long description"><Markdown>{data.long}</Markdown></div>
+      <div className="long description"><Markdown>{t(data.long, { ns: gameId })}</Markdown></div>
     </div>
     <table className="info">
       <tbody>
       <tr>
-        <td title="consider playing these games first.">Prerequisites</td>
+        <td title="consider playing these games first.">{t("Prerequisites")}</td>
-        <td><Markdown>{data.prerequisites.join(', ')}</Markdown></td>
+        <td><Markdown>{t(data.prerequisites.join(', '), { ns: gameId })}</Markdown></td>
       </tr>
       <tr>
-        <td>Worlds</td>
+        <td>{t("Worlds")}</td>
         <td>{data.worlds}</td>
       </tr>
       <tr>
-        <td>Levels</td>
+        <td>{t("Levels")}</td>
         <td>{data.levels}</td>
       </tr>
       <tr>
-        <td>Language</td>
+        <td>{t("Language")}</td>
-        <td title={`in ${data.languages.join(', ')}`}>{data.languages.map((lan) => flag[lan]).join(', ')}</td>
+
+        <td>
+          {data.languages.map((lang) => {
+            let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang)
+            return <ReactCountryFlag key={`flag-${lang}`} title={langOpt?.name} countryCode={langOpt?.flag} className="emojiFlag"/>
+
+          })}
+        </td>
       </tr>
       </tbody>
     </table>
@@ -81,84 +86,67 @@ function LandingPage() {
 
   const navigate = useNavigate();
 
-  const [impressum, setImpressum] = React.useState(false);
+  const [impressumPopup, setImpressumPopup] = React.useState(false);
-  const openImpressum = () => setImpressum(true);
+  const [preferencesPopup, setPreferencesPopup] = React.useState(false);
-  const closeImpressum = () => setImpressum(false);
+  const [navOpen, setNavOpen] = React.useState(false);
+  const openImpressum = () => setImpressumPopup(true);
+  const closeImpressum = () => setImpressumPopup(false);
+  const toggleImpressum = () => setImpressumPopup(!impressumPopup);
+  const closePreferencesPopup = () => setPreferencesPopup(false);
+  const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup);
 
-  // const [allGames, setAllGames] = React.useState([])
+  const { t, i18n } = useTranslation()
-  // const [allTiles, setAllTiles] = React.useState([])
 
-  // const getTiles=()=>{
+  // Load the namespaces of all games
-  //   fetch('featured_games.json', {
+  // TODO: should `allGames` contain game-ids starting with `g/`?
-  //     headers : {
+  i18next.loadNamespaces(lean4gameConfig.allGames.map(id => `g/${id}`))
-  //       'Content-Type': 'application/json',
-  //       'Accept': 'application/json'
-  //     }
-  //   }
-  //   ).then(function(response){
-  //     return response.json()
-  //   }).then(function(data) {
-  //     setAllGames(data.featured_games)
 
-  //   })
+  let allTiles = lean4gameConfig.allGames.map((gameId) => {
-  // }
+    let q =  useGetGameInfoQuery({game: `g/${gameId}`})
 
-  // React.useEffect(()=>{
+    // if (q.isError) {
-  //   getTiles()
+    //   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(()=>{
+    return q.data?.tile
-
+  })
-  //   Promise.allSettled(
-  //     allGames.map((gameId) => (
-  //       fetch(`data/g/${gameId}/game.json`).catch(err => {return undefined})))
-  //   ).then(responses =>
-  //     responses.forEach((result) => console.log(result)))
-  //   //   Promise.all(responses.map(res => {
-  //   //     if (res.status == "fulfilled") {
-  //   //       console.log(res.value.json())
-  //   //       return res.value.json()
-  //   //     } else {
-  //   //       return undefined
-  //   //     }
-  //   //   }))
-  //   // ).then(allData => {
-  //   //   setAllTiles(allData.map(data => data?.tile))
-  //   // })
-  // },[allGames])
-
-  // TODO: I would like to read the supported games list form a JSON,
-  // Then load all these games in
-  //
-  let allGames = [
-    "leanprover-community/nng4",
-    "hhu-adam/robo",
-    "djvelleman/stg4",
-    "miguelmarco/stg4",
-    "trequetrum/lean4game-logic",
-  ]
-  let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
 
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
-      <nav>
+      <nav className="landing-page-nav">
         <GithubIcon url="https://github.com/leanprover-community/lean4game"/>
+        <MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
+        <div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
+            <ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
+            <PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
+        </div>
       </nav>
       <div id="main-title">
-        <h1>Lean Game Server</h1>
+        <h1>{t("Lean Game Server")}</h1>
         <p>
-          A repository of learning games for the
+          <Trans>
-          proof assistant <a target="_blank" href="https://leanprover-community.github.io/">Lean</a> <i>(Lean 4)</i> and
+            A repository of learning games for the
-          its mathematical library <a target="_blank" href="https://github.com/leanprover-community/mathlib4">mathlib</a>
+            proof assistant <a target="_blank" href="https://leanprover-community.github.io/">Lean</a> <i>(Lean 4)</i> and
+            its mathematical library <a target="_blank" href="https://github.com/leanprover-community/mathlib4">mathlib</a>
+          </Trans>
         </p>
       </div>
     </header>
     <div className="game-list">
-      {allTiles.length == 0 ?
+      {allTiles.filter(x => x != null).length == 0 ?
-        <p>No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
+        <p>
-          game directly from a local folder.
+          <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>
+        <h2>{t("Development notes")}</h2>
-        <p>
+        <Trans>
-          As this server runs lean on our university machines, it has a limited capacity.
+          <p>
-          Our current estimate is about 70 simultaneous games.
+            As this server runs lean on our university machines, it has a limited capacity.
-          We hope to address and test this limitation better in the future.
+            Our current estimate is about 70 simultaneous games.
-        </p>
+            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
+          <p>
-          file a <a target="_blank" href="https://github.com/leanprover-community/lean4game/issues">GitHub Issue</a> about
+            Most aspects of the games and the infrastructure are still in development. Feel free to
-          any problems you experience!
+            file a <a target="_blank" href="https://github.com/leanprover-community/lean4game/issues">GitHub Issue</a> about
-        </p>
+            any problems you experience!
+          </p>
+        </Trans>
       </div>
     </section>
     <section>
       <div className="wrapper">
-        <h2>Adding new games</h2>
+        <h2>{t("Adding new games")}</h2>
-        <p>
+        <Trans>
-          If you are considering writing your own game, you should use
+          <p>
-          the <a target="_blank" href="https://github.com/hhu-adam/GameSkeleton">GameSkeleton Github Repo</a> as
+            If you are considering writing your own game, you should use
-          a template and read <a target="_blank" href="https://github.com/leanprover-community/lean4game/">How to Create a Game</a>.
+            the <a target="_blank" href="https://github.com/hhu-adam/GameSkeleton">GameSkeleton Github Repo</a> as
-        </p>
+            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
+          <p>
-          the correct URL. The <a target="_blank" href="https://github.com/leanprover-community/lean4game/">instructions above</a> also
+            You can directly load your games into the server and play it using
-          explain the details for how to load your game to the server.
+            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.
+            We'd like to encourage you to contact us if you have any questions.
-        </p>
+          </p>
-        <p>
+          <p>
-          Featured games on this page are added manually.
+            Featured games on this page are added manually.
-          Please get in contact and we-ll happily add yours.
+            Please get in contact and we'll happily add yours.
-        </p>
+          </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
+          <Trans>
-          project <a target="_blank" href="https://hhu-adam.github.io">ADAM : Anticipating the Digital Age of Mathematics</a> at
+            This server has been developed as part of the
-          Heinrich-Heine-Universität in Düsseldorf.
+            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'
@@ -28,10 +29,10 @@ import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
-  ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
+  ProofContext, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
-import { GameHint } from './infoview/rpc_api'
+import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints, filterHints } from './hints'
+import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import path from 'path';
 
@@ -49,6 +50,11 @@ import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc'
 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()
@@ -58,21 +64,39 @@ function Level() {
   const levelId = parseInt(params.levelId)
   const worldId = params.worldId
 
-  const [impressum, setImpressum] = React.useState(false)
+  const gameId = React.useContext(GameIdContext)
 
-  const closeImpressum = () => {
+  // Load the namespace of the game
-    setImpressum(false)
+  i18next.loadNamespaces(gameId).catch(err => {
-  }
+    console.warn(`translations for ${gameId} do not exist.`)
+  })
+
+  const gameInfo = useGetGameInfoQuery({game: gameId})
+
+  // pop-ups
+  const [impressum, setImpressum] = React.useState(false)
+  const [info, setInfo] = React.useState(false)
+  const [preferencesPopup, setPreferencesPopup] = React.useState(false)
+
+  function closeImpressum()   {setImpressum(false)}
+  function closeInfo()        {setInfo(false)}
+  function closePreferencesPopup() {setPreferencesPopup(false)}
+  function toggleImpressum()  {setImpressum(!impressum)}
+  function toggleInfo()       {setInfo(!info)}
+  function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
 
   return <WorldLevelIdContext.Provider value={{worldId, levelId}}>
     {levelId == 0 ?
-      <Introduction impressum={impressum} setImpressum={setImpressum} /> :
+      <Introduction impressum={impressum} setImpressum={setImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup} /> :
-      <PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} />}
+      <PlayableLevel key={`${worldId}/${levelId}`} impressum={impressum} setImpressum={setImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>}
     {impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
+    {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
+    {preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
   </WorldLevelIdContext.Provider>
 }
 
-function ChatPanel({lastLevel}) {
+function ChatPanel({lastLevel, visible = true}) {
+  let { t } = useTranslation()
   const chatRef = useRef<HTMLDivElement>(null)
   const {mobile} = useContext(PreferencesContext)
   const gameId = useContext(GameIdContext)
@@ -83,9 +107,7 @@ function ChatPanel({lastLevel}) {
   const {selectedStep, setSelectedStep} = useContext(SelectionContext)
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
-  // If the last step has errors, we want to treat it as if it is part of the second-to-last step
+  let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
-  let k = proof.length - 1
-  let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 0
 
   function toggleSelection(line: number) {
     return (ev) => {
@@ -98,29 +120,6 @@ function ChatPanel({lastLevel}) {
     }
   }
 
-  function hasHiddenHints(i : number): boolean {
-    let step = proof[i]
-    // For example if the proof isn't loaded yet
-    if(!step) {return false}
-    return step.hints.some((hint) => hint.hidden)
-  }
-
-  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.length)) {return}
-
-    // state must not be mutated, therefore we need to clone the set
-    let tmp = new Set(showHelp)
-    if (tmp.has(k - withErr)) {
-      tmp.delete(k - withErr)
-    } else {
-      tmp.add(k - withErr)
-    }
-    setShowHelp(tmp)
-    console.debug(`help: ${Array.from(tmp.values())}`)
-  }
-
   useEffect(() => {
     // TODO: For some reason this is always called twice
     console.debug('scroll chat')
@@ -144,62 +143,64 @@ function ChatPanel({lastLevel}) {
   //   // 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)+/)
 
-  // experimental: Remove all hints that appeared identically in the previous step
+  return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
-  // This effectively prevent consequtive hints being shown.
-  let modifiedHints : GameHint[][] = filterHints(proof)
-
-  return <div className="chat-panel">
     <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)} />
       ))}
-      {modifiedHints.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}/>
+        }
+      })}
+
+      {/* {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.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.length - 1}/>
+            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
         }
-      })}
+      })} */}
       <DeletedHints hints={deletedChat}/>
-      {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">
-      {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>)
         }
-      {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+      <MoreHelpButton />
-        <Button to="" onClick={activateHiddenHints}>
-          Show more help!
-        </Button>
-      }
     </div>
   </div>
 }
 
-function ExercisePanel({codeviewRef, visible=true}) {
+
+function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject<HTMLDivElement>, visible?: boolean}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -211,7 +212,8 @@ function ExercisePanel({codeviewRef, visible=true}) {
   </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)
@@ -229,7 +231,11 @@ function PlayableLevel({impressum, setImpressum}) {
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
   // The state variables for the `ProofContext`
-  const [proof, setProof] = useState<Array<ProofStep>>([])
+  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>>([])
@@ -239,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]
 
@@ -299,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()
@@ -329,6 +336,8 @@ function PlayableLevel({impressum, setImpressum}) {
           console.debug(`not inserting template.`)
         }
       }
+    } else {
+      setLockEditorMode(false)
     }
   }, [level, levelId, worldId, gameId, editor])
 
@@ -343,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(),
@@ -352,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.length) {
+    if (proof?.steps.length) {
       console.debug(Array.from(showHelp))
-      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.length))))
+      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof?.steps.length))))
     }
   }, [proof])
 
   // save showed help in store
   useEffect(() => {
-    if (proof.length) {
+    if (proof?.steps.length) {
       console.debug(`showHelp:\n ${showHelp}`)
       dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)}))
     }
@@ -372,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(),
@@ -395,22 +404,25 @@ function PlayableLevel({impressum, setImpressum}) {
       //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
       // }
     }
-  }, [editor, typewriterMode, onigasmH == null])
+  }, [editor, typewriterMode, lockEditorMode, onigasmH == null])
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
       <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
-        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockInputMode, setLockInputMode}}>
+        <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockEditorMode, setLockEditorMode}}>
-          <ProofContext.Provider value={{proof, setProof}}>
+          <ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>
                 <LevelAppBar
                   pageNumber={pageNumber} setPageNumber={setPageNumber}
                   isLoading={level.isLoading}
-                  levelTitle={`${mobile ? '' : 'Level '}${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
+                  levelTitle={(mobile ? "" : t("Level")) + ` ${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
-                    (level?.data?.title && ` : ${level?.data?.title}`)}
+                    (level?.data?.title && ` : ${t(level?.data?.title, {ns: gameId})}`)}
-                  toggleImpressum={toggleImpressum} />
+                  toggleImpressum={toggleImpressum}
+                  toggleInfo={toggleInfo}
+                  togglePreferencesPopup={togglePreferencesPopup}
+                  />
                 {mobile?
                   // TODO: This is copied from the `Split` component below...
                   <>
@@ -439,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>
@@ -466,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)
 
@@ -484,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 ?
@@ -492,10 +507,9 @@ function Introduction({impressum, setImpressum}) {
       :
         <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
           <IntroductionPanel gameInfo={gameInfo} />
-          <div className="world-image-container empty">
+          <div className="world-image-container empty center">
             {image &&
-              // TODO: Temporary for testing
+              <img className="contain" src={path.join("data", gameId, image)} alt="" />
-              <img className={worldId=="Proposition" ? "cover" : "contain"} src={path.join("data", gameId, image)} alt="" />
             }
 
           </div>
@@ -622,7 +636,9 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
     }
     // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
     setInfoProvider(infoProvider)
-    client.restart()
+
+    // TODO: it looks like we get errors "File Changed" here.
+    client.restart("Lean4Game")
 
     const editorApi = infoProvider.getApi()
 

client/src/components/popup/erase.tsx

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

client/src/components/popup/game_info.tsx

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

client/src/components/popup/preferences.tsx

@@ -1,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'> {
+export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
-    handleClose: () => void
+  let { t } = useTranslation()
-}
+  const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
 
-export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) {
+  const marks = [
+    {
+      value: 0,
+      label: t('Mobile'),
+      key: "mobile"
+    },
+    {
+      value: 1,
+      label: t('Auto'),
+      key: "auto"
+    },
+    {
+      value: 2,
+      label: t('Desktop'),
+      key: "desktop"
+    },
+  ];
 
-    const marks = [
+  const handlerChangeLayout = (_: Event, value: number) => {
-        {
+    setLayout(marks[value].key as IPreferencesContext["layout"])
-            value: 0,
+  }
-            label: 'Mobile',
-            key: "mobile"
-        },
-        {
-            value: 1,
-            label: 'Auto',
-            key: "auto"
-        },
-        {
-            value: 2,
-            label: 'Desktop',
-            key: "desktop"
-        },
-    ];
 
-    const handlerChangeLayout = (_: Event, value: number) => {
+  const handlerChangeLanguage = (ev: SelectChangeEvent<string>) => {
-        setLayout(marks[value].key as IPreferencesContext["layout"])
+    setLanguage(ev.target.value as IPreferencesContext["language"])
-    }
+  }
 
-    return <div className="modal-wrapper">
+  return <div className="modal-wrapper">
-        <div className="modal-backdrop" onClick={handleClose} />
+    <div className="modal-backdrop" onClick={handleClose} />
-        <div className="modal">
+    <div className="modal">
-            <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+      <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
-            <Typography variant="body1" component="div" className="settings">
+      <Typography variant="body1" component="div" className="settings">
-                <div className='preferences-category'>
+        <div className='preferences-category'>
-                    <div className='category-title'>
+          <div className='category-title'>
-                        <h3>Layout</h3>
+            <h3>{t("Language")}</h3>
-                    </div>
+          </div>
-                    <div className='preferences-item first leave-left-gap'>
+          <div className='preferences-item first leave-left-gap'>
-                        <FormControlLabel
+            <FormControlLabel
-                            control={
+              control={
-                                <Box sx={{ width: 300 }}>
+                <Box sx={{ width: 300 }}>
-                                    <Slider
+                  <Select
-                                        aria-label="Always visible"
+                    value={language}
-                                        value={marks.find(item => item.key === layout).value}
+                    label={t("Language")}
-                                        step={1}
+                    onChange={handlerChangeLanguage}>
-                                        marks={marks}
+                      {lean4gameConfig.languages.map(lang => {return <MenuItem key={`menu-item-lang-${lang.iso}`} value={lang.iso}><ReactCountryFlag countryCode={lang.flag}/>&nbsp;{lang.name}</MenuItem>})}
-                                        max={2}
+                  </Select>
-                                        sx={{
+                </Box>
-                                            '& .MuiSlider-track': { display: 'none', },
+              }
-                                        }}
+              label=""
-                                        onChange={handlerChangeLayout}
+            />
-                                    />
+          </div>
-                                </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>
         </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>
+    <h2>{t("Game Rules")}</h2>
-    <p>
+    <Trans>
-      Game rules determine if it is allowed to skip levels and if the games runs checks to only
+      <p>
-      allow unlocked tactics and theorems in proofs.
+        Game rules determine if it is allowed to skip levels and if the games runs checks to only
-    </p>
+        allow unlocked tactics and theorems in proofs.
-    <p>
+      </p>
-      Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal
+      <p>
-      tactics needed to solve a level, plus any tactics you unlocked in another level. That means
+        Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal
-      if you unlock <code>simp</code> in a level, you can use it henceforth in any level.
+        tactics needed to solve a level, plus any tactics you unlocked in another level. That means
-    </p>
+        if you unlock <code>simp</code> in a level, you can use it henceforth in any level.
-    <p>The options are:</p>
+      </p>
+      <p>The options are:</p>
+    </Trans>
     <table>
       <thead>
         <tr>
           <th scope="col"></th>
-          <th scope="col">levels</th>
+          <th scope="col">{t("levels")}</th>
-          <th scope="col">tactics</th>
+          <th scope="col">{t("tactics")}</th>
         </tr>
       </thead>
       <tbody>
         <tr>
-          <th scope="row">regular</th>
+          <th scope="row">{t("regular")}</th>
           <td>🔐</td>
           <td>🔐</td>
         </tr>
         <tr>
-          <th scope="row">relaxed</th>
+          <th scope="row">{t("relaxed")}</th>
           <td>🔓</td>
           <td>🔐</td>
         </tr>
         <tr>
-          <th scope="row">none</th>
+          <th scope="row">{t("none")}</th>
           <td>🔓</td>
           <td>🔓</td>
         </tr>

client/src/components/popup/upload.tsx

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

client/src/components/welcome.tsx

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

client/src/components/world_tree.tsx

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

client/src/config.json

@@ -0,0 +1,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 {
@@ -188,6 +195,18 @@
   flex-direction: row;
 }
 
+.exercise .failed-command {
+  background-color: #eee;
+  padding: .5em;
+  border-radius: .2em;
+  /* TODO: It seems my browsers merge the margings of the proof steps,
+  so that it only shows once 0.5rem instead of twice. Thus have 1.5 here now.
+  */
+  margin-bottom: 1.5rem;
+  display: flex;
+  flex-direction: row;
+}
+
 .exercise .command-text {
   flex: 1;
   background-color: #fff;
@@ -199,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;
@@ -368,3 +374,22 @@ td code  {
   min-width: 40px;
   text-align: center;
 }
+
+/* Fixes https://github.com/leanprover-community/lean4game/issues/202 */
+.katex-mathml {
+  display: none;
+}
+
+/* DEBUG */
+/* .proof .step {
+  border: 2px solid rgb(0, 123, 255);
+} */
+
+.nav-btns {
+  height: 2rem;
+}
+
+.nav-btns .language-btn {
+  background: #DDF6FF;
+  text-align: center;
+}

client/src/i18n.ts

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

client/src/index.tsx

@@ -9,6 +9,7 @@ import ErrorPage from './components/error_page'
 import Welcome from './components/welcome'
 import LandingPage from './components/landing_page'
 import Level from './components/level'
+import './i18n';
 
 
 
@@ -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 { 
+import {
-    PreferencesState, 
+    PreferencesState,
-    setLayout as setPreferencesLayout, 
+    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
+For more details and features, read [Writing Exercises](writing_exercises.md)
-
-You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:
-
-```lean
-@[simp]
-Statement my_simp_lemma ...
-```
 
 ### 6. c) Proof
 

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/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}
+  | .Level => modifyCurLevel fun level => pure {level with title := title}
-  | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with title := title}
   | .Game => modifyCurGame  fun game => pure {game with
-      title := t.getString
+      title := title
-      tile := {game.tile with title := t.getString}}
+      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"`.
+/-- A list of Languages the game is translated to. For example `Languages "de" "en"`.
-NOTE: For the time being, only a single language is supported.
+
+The keys are ISO language codes.
  -/
 elab "Languages" t:str* : command => do
   modifyCurGame fun game => pure {game with
@@ -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

@@ -3,6 +3,8 @@ import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
+import GameServer.EnvExtensions
+import GameServer.Tactic.LetIntros
 
 namespace MyModule
 
@@ -60,8 +62,8 @@ open Snapshots
 open JsonRpc
 
 /--
-Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
+Game-specific state to be packed on top of the `Server.FileWorker.WorkerState`
-used by the lean server.
+used by the Lean server.
 -/
 structure WorkerState :=
   /--
@@ -84,7 +86,7 @@ structure WorkerState :=
 deriving ToJson, FromJson
 
 /--
-Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad
+Pack the our custom `WorkerState` on top of the normal worker monad
 `Server.FileWorker.WorkerM`.
 -/
 abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
@@ -102,16 +104,6 @@ def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext)
       pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
       data     := s }}
 
-/-- Deprecated! -/
-def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
-    Elab.Command.CommandElabM Unit := do
-  modify fun st => { st with
-    messages := st.messages.add {
-      fileName := inputCtx.fileName
-      severity := MessageSeverity.error
-      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-      data     := s }}
-
 -- TODO: use HashSet for allowed tactics?
 /--
 Find all tactics in syntax object that are forbidden according to a
@@ -131,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`
@@ -178,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.
+          match workerState.inventory.find? (· == n.toString) with
-          addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+          | 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
@@ -262,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
@@ -308,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,74 +322,136 @@ where
     uri : String
   deriving ToJson, FromJson
 
-  /-- Checks whether game level has been completed and sends a notification to the client -/
+structure GameDiagnostics where
-  def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
+  diagnostics : List Diagnostic
-    -- check if there is any error or warning
+deriving ToJson, FromJson
-    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 }
 
-  /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
+structure GameParams where
-  private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
+  uri : String
-      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams)
+  diagnostics : GameDiagnostics
-      : AsyncElabM (Option Snapshot) := do
+deriving ToJson, FromJson
-    cancelTk.check
-    let s ← get
-    let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
-    if lastSnap.isAtEnd then
-      publishGameCompleted m ctx.hOut s.snaps
-      publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
-      publishProgressDone m ctx.hOut
-      -- This will overwrite existing ilean info for the file, in case something
-      -- went wrong during the incremental updates.
-      publishIleanInfoFinal m ctx.hOut s.snaps
-      return none
-    publishProgressAtPos m lastSnap.endPos ctx.hOut
-    -- 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 }
-    -- TODO(MH): check for interrupt with increased precision
-    cancelTk.check
-    /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
-      while preferring newer versions over old ones. The former is necessary because we do
-      not explicitly clear older diagnostics, while the latter is necessary because we do
-      not guarantee that diagnostics are emitted in order. Specifically, it may happen that
-      we interrupted this elaboration task right at this point and a newer elaboration task
-      emits diagnostics, after which we emit old diagnostics because we did not yet detect
-      the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
-      because we cannot guarantee that no further diagnostics are emitted after clearing
-      them. -/
-    -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
-    -- because empty diagnostics clear existing error/information squiggles. Therefore we always
-    -- want to publish in case there was previously a message at this position.
-    publishDiagnostics m snap.diagnostics.toArray ctx.hOut
-    publishIleanInfoUpdate m ctx.hOut #[snap]
-    return some snap
 
-  /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
+-- `snap` and `initParams` are unused
-  def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
+set_option linter.unusedVariables false in
-      (startAfterMs : UInt32) (gameWorkerState : WorkerState)
+
-      : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
+/-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/
-    let ctx ← read
+def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) :
-    let some headerSnap := snaps[0]? | panic! "empty snapshots"
+    IO Unit := do
-    if headerSnap.msgLog.hasErrors then
+  -- let text := m.text
-      -- Treat header processing errors as fatal so users aren't swamped with
+
-      -- followup errors
+  -- -- `snap` is the one snapshot containing the entire proof.
-      publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
+  -- let mut goals : Array <| InteractiveGoalsWithHints := #[]
-      publishIleanInfoFinal m ctx.hOut #[headerSnap]
+  -- for pos in text.positions do
-      return AsyncList.ofList [headerSnap]
+  --   let source := text.getLineBefore pos
-    else
+  --   -- iterate over all newlines in the proof and get the goals and hints at each position
-      -- This will overwrite existing ilean info for the file since this has a
+  --   if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? text pos then
-      -- higher version number.
+  --     pure ()
-      publishIleanInfoUpdate m ctx.hOut snaps
+  --     let goalAtPos : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
-      return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
+  --       fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
-        IO.sleep startAfterMs
+  --         -- TODO: What does this function body do?
-        AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
+  --         -- let ciAfter := { ci with mctx := ti.mctxAfter }
+  --         let ci := if useAfter then
+  --             { ci with mctx := tacticInfo.mctxAfter }
+  --           else
+  --             { ci with mctx := tacticInfo.mctxBefore }
+  --         -- compute the interactive goals
+  --         let goalMvars : List MVarId ← ci.runMetaM {} do
+  --           return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
+
+  --         let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
+  --           goalMvars.mapM fun goal => do
+  --             let hints ← findHints goal m initParams
+  --             let interactiveGoal ← goalToInteractive goal
+  --             return ⟨interactiveGoal, hints⟩
+  --         -- TODO: This code is way old, can it be deleted?
+  --         -- compute the goal diff
+  --         -- let goals ← ciAfter.runMetaM {} (do
+  --         --     try
+  --         --       Widget.diffInteractiveGoals useAfter ti goals
+  --         --     catch _ =>
+  --         --       -- fail silently, since this is just a bonus feature
+  --         --       return goals
+  --         -- )
+  --         return interactiveGoals
+  --     let goalAtPos : Array InteractiveGoalWithHints := ⟨goalAtPos.foldl (· ++ ·) []⟩
+  --     goals := goals.push ⟨goalAtPos, source⟩
+  --   else
+  --     -- No goals present
+  --     goals := goals.push default
+
+  -- -- Question: Is there a difference between the diags of this snap and the last snap?
+  -- -- Should we get the diags from there?
+  -- let diag : Array Widget.InteractiveDiagnostic := snap.interactiveDiags.toArray
+
+  -- -- Level is completed if there are no errrors or warnings
+  -- let completed : Bool := ¬ diag.any (fun d =>
+  --   d.severity? == some .error ∨ d.severity? == some .warning)
+
+  -- let param : ProofState := {
+  --   steps := goals,
+  --   diagnostics := diag,
+  --   completed := completed }
+
+  -- TODO
+  let param := { uri := m.uri : GameCompletedParams}
+
+
+  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 }
+
+/-- 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
+
+  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 })
 
 end Elab
 
@@ -439,7 +501,7 @@ def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
         validSnaps := validSnaps.dropLast
     -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
     -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-    unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
+    unfoldCmdSnaps newMeta validSnaps.toArray cancelTk s ctx
       (startAfterMs := ctx.initParams.editDelay.toUInt32)
   StateT.lift <| modify fun st => { st with
     doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
@@ -453,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
@@ -488,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 }
@@ -505,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 {})
@@ -513,49 +581,52 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     publishDiagnostics m headerSnap.diagnostics.toArray hOut
     return (headerSnap, srcSearchPath)
 
+/-- Copied from `Lean.Server.FileWorker.initializeWorker`. Added `gameDir` and
+`gameWorkerState` arguments and use custom `unfoldCmdSnaps`. -/
+-- @[inherit_doc Lean.Server.FileWorker.initializeWorker]
 def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
     (gameDir : String) (gameWorkerState : WorkerState) : IO (WorkerContext × Server.FileWorker.WorkerState) := do
   let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-
   let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-    gameDir gameWorkerState.levelInfo.module
+    (gameDir := gameDir) (module := gameWorkerState.levelInfo.module)
   let cancelTk ← CancelToken.new
-  let ctx :=
+  let ctx := {
-    { hIn  := i
+    hIn  := i
-      hOut := o
+    hOut := o
-      hLog := e
+    hLog := e
-      headerTask
+    headerTask
-      initParams
+    initParams
-      clientHasWidgets
+    clientHasWidgets
-    }
+  }
   let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-    | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+    | Except.ok (s, _) => unfoldCmdSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
     | Except.error e   => throw (e : ElabTaskError))
   let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
-  return (ctx,
+  return (ctx, {
-  { doc             := doc
+    doc                := doc
-    initHeaderStx   := headerStx
+    initHeaderStx      := headerStx
     currHeaderStx      := headerStx
     importCachingTask? := none
-    pendingRequests := RBMap.empty
+    pendingRequests    := RBMap.empty
-    rpcSessions     := RBMap.empty
+    rpcSessions        := RBMap.empty
   })
 
 end Initialization
 
 section NotificationHandling
 
+/-- Copied from `Lean.Server.FileWorker.handleDidChange` but with our custom `WorkerM` and
+`updateDocument` -/
+-- @[inherit_doc Lean.Server.FileWorker.handleDidChange]
 def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
   let docId := p.textDocument
   let changes := p.contentChanges
-  let oldDoc := (← StateT.lift get).doc
+  let oldDoc := (← StateT.lift get).doc -- needed a lift to our custom `WorkerM`
-  let some newVersion ← pure docId.version?
+  let newVersion := docId.version?.getD 0
-    | throwServerError "Expected version number"
+  if ¬ changes.isEmpty then
-  if newVersion ≤ oldDoc.meta.version then
-    -- TODO(WN): This happens on restart sometimes.
-    IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
-  else if ¬ changes.isEmpty then
     let newDocText := foldDocumentChanges changes oldDoc.meta.text
+    -- modification: set the `DependencyBuildMode` from
+    -- `oldDoc.meta.dependencyBuildMode` to `.always`
     updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 end NotificationHandling
@@ -591,39 +662,34 @@ end MessageHandling
 section MainLoop
 
 /--
-Erase finished tasks if there are no errors.
+The main-loop. Copied from `Lean.Server.FileWorker.mainLoop`. Use custom `WorkerM` as well
--/
+as custom `handleNotification`.
-private def filterFinishedTasks (acc : PendingRequestMap) (id : RequestID)
-    (task : Task (Except IO.Error Unit)) : IO PendingRequestMap := do
-  if (← hasFinished task) then
-    /- Handler tasks are constructed so that the only possible errors here
-    are failures of writing a response into the stream. -/
-    if let Except.error e := task.get then
-      throwServerError s!"Failed responding to request {id}: {e}"
-    pure <| acc.erase id
-  else pure acc
-
-/--
-The main-loop.
 -/
+--@[inherit_doc Lean.Server.FileWorker.mainLoop]
 partial def mainLoop : WorkerM Unit := do
   let ctx ← read
   let mut st ← StateT.lift get
   let msg ← ctx.hIn.readLspMessage
-  let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
+  -- Erase finished tasks if there are no errors.
-    filterFinishedTasks acc id task) st.pendingRequests
+  let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
+      : IO PendingRequestMap := do
+    if (← hasFinished task) then
+      if let Except.error e := task.get then
+        throwServerError s!"Failed responding to request {id}: {e}"
+      pure <| acc.erase id
+    else pure acc
+  let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
   st := { st with pendingRequests }
-  -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
   for (id, seshRef) in st.rpcSessions do
     let sesh ← seshRef.get
     if (← sesh.hasExpired) then
       st := { st with rpcSessions := st.rpcSessions.erase id }
 
   set st
-
   -- Process the RPC-message and restart main-loop.
   match msg with
   | Message.request id "shutdown" none =>
+    --added. TODO: why do we need that? Or has it just removed in Lean since when we started?
     ctx.hOut.writeLspResponse ⟨id, Json.null⟩
     mainLoop
   | Message.request id method (some params) =>
@@ -633,6 +699,7 @@ partial def mainLoop : WorkerM Unit := do
   | Message.notification "exit" none =>
     let doc := st.doc
     doc.cancelTk.set
+    doc.cmdSnaps.cancel
     return ()
   | Message.notification method (some params) =>
     -- Custom notification handler
@@ -643,10 +710,15 @@ partial def mainLoop : WorkerM Unit := do
 
 end MainLoop
 
-
+/-- Modified from `Lean.Server.FileWorker.initAndRunWorker`.
+Added `gameDir` argument, -/
+-- @[inherit_doc Lean.Server.FileWorker.initAndRunWorker]
 def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
+
+
+  -- BIG MODIFICATION
   let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
   o.writeLspResponse {
     id     := initRequest.id
@@ -662,16 +734,16 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
   discard $ i.readLspNotificationAs "initialized" InitializedParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
 
+
   let doc := param.textDocument
-  /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
+  -- modification: using `.always`
-    "\n", which should be enough to handle both LF and CRLF correctly.
-    This is because LSP always refers to characters by (line, column),
-    so if we get the line number correct it shouldn't matter that there
-    is a CR there. -/
   let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
+
+
+    -- BIG MODIFICATION
     let game ← loadGameData gameDir
     -- TODO: We misuse the `rootUri` field to the gameName
     let rootUri? : Option String := some (toString game.name)
@@ -691,6 +763,8 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
     -- Run the main loop
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
       StateT.run (s := gameWorkerState) <| (mainLoop)
+
+
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
@@ -703,8 +777,12 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
 /--
 The main function. Simply wrapping `initAndRunWorker`.
 
+Copied from `Lean.Server.FileWorker.workerMain`. We add `args` as an argument to pass on
+the `gameDir`.
+
 TODO: The first arg `args[0]` is always expected to be `--server`. We could drop this completely.
 -/
+-- @[inherit_doc Lean.Server.FileWorker.workerMain]
 def workerMain (opts : Options) (args : List String): IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
@@ -712,9 +790,6 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
   try
     let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
     let exitCode ← initAndRunWorker i o e opts gameDir
-    -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit,
-    -- but we definitely don't want to do that in the case of the worker processes,
-    -- which can produce non-terminating tasks evaluating user code.
     o.flush
     e.flush
     IO.Process.exit exitCode.toUInt8

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

@@ -1,74 +1,19 @@
-/- This file is mostly copied from `Lean/Widget/InteractiveGoal.lean`. -/
+import GameServer.Structures
 
-import Lean.Widget.InteractiveGoal
+/-!
+This file is a modified copy of `Lean.Widget.InteractiveGoal`.
 
-/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/
+Note that the structures have been moved to `Structures.lean`, but most of the
+functions here must be duplicated from `Lean.Widget.InteractiveGoal` in order
+to use the duplicated structures.
+-/
 
 namespace GameServer
+
 open Lean Lean.Widget Lean.Server
 
-structure GameHint where
+-- duplicated with custom `InteractiveGoalCore`
-  text : String
+-- @[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
-  hidden : Bool
-deriving FromJson, ToJson
-
-/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered
-as `h₁ h₂ : α`. We call this a 'hypothesis bundle'. We use `none` instead of `some false` for
-booleans to save space in the json encoding. -/
-structure InteractiveHypothesisBundle where
-  /-- The user-friendly name for each hypothesis. -/
-  names : Array Name
-  /-- The ids for each variable. Should have the same length as `names`. -/
-  fvarIds : Array FVarId
-  type : CodeWithInfos
-  /-- The value, in the case the hypothesis is a `let`-binder. -/
-  val? : Option CodeWithInfos := none
-  /-- The hypothesis is a typeclass instance. -/
-  isInstance? : Option Bool := none
-  /-- The hypothesis is a type. -/
-  isType? : Option Bool := none
-  /-- The hypothesis's type is of type `Prop` -/
-  isAssumption? : Option Bool := none
-  /-- If true, the hypothesis was not present on the previous tactic state.
-  Only present in tactic-mode goals. -/
-  isInserted? : Option Bool := none
-  /-- If true, the hypothesis will be removed in the next tactic state.
-  Only present in tactic-mode goals. -/
-  isRemoved? : Option Bool := none
-  deriving Inhabited, RpcEncodable
-
-/-- The shared parts of interactive term-mode and tactic-mode goals. -/
-structure InteractiveGoalCore where
-  hyps : Array InteractiveHypothesisBundle
-  /-- The target type. -/
-  type : CodeWithInfos
-  /-- Metavariable context that the goal is well-typed in. -/
-  ctx : WithRpcRef Elab.ContextInfo
-
-/-- An interactive tactic-mode goal. -/
-structure InteractiveGoal extends InteractiveGoalCore where
-  /-- The name `foo` in `case foo`, if any. -/
-  userName? : Option String
-  /-- The symbol to display before the target type. Usually `⊢ ` but `conv` goals use `∣ `
-  and it could be extended. -/
-  goalPrefix : String
-  /-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.) -/
-  mvarId : MVarId
-  /-- If true, the goal was not present on the previous tactic state. -/
-  isInserted? : Option Bool := none
-  /-- If true, the goal will be removed on the next tactic state. -/
-  isRemoved? : Option Bool := none
-  hints : Array GameHint := #[]
-  deriving RpcEncodable
-
-/-- An interactive term-mode goal. -/
-structure InteractiveTermGoal extends InteractiveGoalCore where
-  /-- Syntactic range of the term. -/
-  range : Lsp.Range
-  /-- Information about the term whose type is the term-mode goal. -/
-  term : WithRpcRef Elab.TermInfo
-  deriving RpcEncodable
-
 def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
     (goalPrefix : String) : Format := Id.run do
   let indent := 2 -- Use option
@@ -79,8 +24,7 @@ def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option Str
     ret := addLine ret
     let names := hyp.names
         |>.toList
-        |>.filter (not ∘ Name.isAnonymous)
+        |>.filter (· != toString Name.anonymous)
-        |>.map toString
         |> " ".intercalate
     match names with
     | "" =>
@@ -97,16 +41,24 @@ where
   addLine (fmt : Format) : Format :=
     if fmt.isNil then fmt else fmt ++ Format.line
 
+-- duplicated with custom `InteractiveGoal`
+-- @[inherit_doc Lean.Widget.InteractiveGoal.pretty]
 def InteractiveGoal.pretty (g : InteractiveGoal) : Format :=
   g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix
 
+-- duplicated with custom `InteractiveTermGoal`
+-- @[inherit_doc Lean.Widget.InteractiveTermGoal.pretty]
 def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format :=
   g.toInteractiveGoalCore.pretty none "⊢ "
 
+-- duplicated with custom `InteractiveGoal`
+-- @[inherit_doc Lean.Widget.InteractiveGoals]
 structure InteractiveGoals where
   goals : Array InteractiveGoal
   deriving RpcEncodable
 
+-- duplicated with custom `InteractiveGoals`
+-- @[inherit_doc Lean.Widget.InteractiveGoals.append]
 def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
   goals := l.goals ++ r.goals
 
@@ -114,9 +66,10 @@ instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
 instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
 
 open Meta in
-/-- Extend an array of hypothesis bundles with another bundle. -/
+-- duplicated with custom `InteractiveHypothesisBundle` and therefore added `isAssumption?`
+@[inherit_doc Lean.Widget.addInteractiveHypothesisBundle]
 def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
-    (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) :
+    (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) :
     MetaM (Array InteractiveHypothesisBundle) := do
   if ids.size == 0 then
     throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle."
@@ -125,11 +78,12 @@ def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
   return hyps.push {
     names
     fvarIds
-    type           := (← ppExprTagged type)
+    type        := (← ppExprTagged type)
-    val?           := (← value?.mapM ppExprTagged)
+    val?        := (← value?.mapM ppExprTagged)
-    isInstance?    := if (← isClass? type).isSome then true else none
+    isInstance? := if (← isClass? type).isSome then true else none
-    isType?        := if (← instantiateMVars type).isSort then true else none
+    isType?     := if (← instantiateMVars type).isSort then true else none
-    isAssumption?  := if (← inferType type).isProp then true else none
+    -- Added:
+    isAssumption? := if (← inferType type).isProp then true else none
   }
 
 open Meta in
@@ -142,13 +96,15 @@ def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α)
   withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl)
 
 open Meta in
-/-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
+
-def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM InteractiveGoal := do
+-- Duplicated from `Lean.Widget.goalToInteractive` with custom structures
+@[inherit_doc Lean.Widget.goalToInteractive]
+def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
   let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
   let showLetValues := pp.showLetValues.get (← getOptions)
   withGoalCtx mvarId fun lctx mvarDecl => do
-    let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
+    let pushPending (ids : Array (String × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
         : MetaM (Array InteractiveHypothesisBundle) :=
       if ids.isEmpty then
         pure hyps
@@ -156,7 +112,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
         match type? with
         | none      => pure hyps
         | some type => addInteractiveHypothesisBundle hyps ids type
-    let mut varNames : Array (Name × FVarId) := #[]
+    let mut varNames : Array (String × FVarId) := #[]
     let mut prevType? : Option Expr := none
     let mut hyps : Array InteractiveHypothesisBundle := #[]
     for localDecl in lctx do
@@ -165,7 +121,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
       else
         match localDecl with
         | LocalDecl.cdecl _index fvarId varName type _ _ =>
-          let varName := varName.simpMacroScopes
+          let varName := toString varName
           let type ← instantiateMVars type
           if prevType? == none || prevType? == some type then
             varNames := varNames.push (varName, fvarId)
@@ -174,7 +130,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
             varNames := #[(varName, fvarId)]
           prevType? := some type
         | LocalDecl.ldecl _index fvarId varName type val _ _ => do
-          let varName := varName.simpMacroScopes
+          let varName := toString varName
           hyps ← pushPending varNames prevType? hyps
           let type ← instantiateMVars type
           let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
@@ -190,11 +146,10 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
     return {
       hyps
       type := goalFmt
-      ctx := ⟨← Elab.ContextInfo.save⟩
+      ctx := ⟨{← Elab.CommandContextInfo.save with }⟩
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId
-      hints
     }
 
 end GameServer

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,5 +1,7 @@
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
+import GameServer.Hints
+import I18n
 
 open Lean
 open Server
@@ -7,7 +9,6 @@ open Widget
 open RequestM
 open Meta
 
-
 /-! ## GameGoal -/
 
 namespace GameServer
@@ -103,49 +104,240 @@ 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) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
+def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
   goal.withContext do
-    let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
+    let some level ← getLevelByFileName? initParams m.mkInputContext.fileName
-      | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
+      | throwError "Level not found: {m.mkInputContext.fileName}"
     let hints ← level.hints.filterMapM fun hint => do
       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
 
-open RequestM in
+def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
-def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do
+    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)
+    (completedWithWarnings : Bool) (pos : Lsp.Position)
+    (startDiags : Array InteractiveDiagnostic := #[]) :
+    RequestM <| Array InteractiveDiagnostic := do
+  let mut out : Array InteractiveDiagnostic := startDiags
+  if goalCount == 0 then
+    if completed then
+      out := out.push {
+        -- 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
+          }
+        severity? := Lsp.DiagnosticSeverity.information }
+    else if completedWithWarnings then
+      out := out.push {
+        message := .text t!"level completed with warnings… 🎭"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information }
+    else
+      pure ()
+  else if goalCount < prevGoalCount then
+    -- 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
+
+
+/-- 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.
+ -/
+def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option ProofState)) := do
   let doc ← readDoc
   let rc ← readThe RequestContext
   let text := doc.meta.text
+
+  withWaitFindSnap
+    doc
+    -- TODO (Alex): I couldn't find a good condition to find the correct snap. So we are looking
+    -- for the first snap with goals here.
+    -- NOTE (Jon): The entire proof is in one snap, so hoped that Position `0` is good enough.
+    (fun snap => ¬ (snap.infoTree.goalsAt? doc.meta.text 0).isEmpty)
+    (notFoundX := return none)
+    fun snap => do
+      -- `snap` is the one snapshot containing the entire proof.
+      let mut steps : Array <| InteractiveGoalsWithHints := #[]
+
+      -- Question: Is there a difference between the diags of this snap and the last snap?
+      -- Should we get the diags from there?
+      -- Answer: The last snap only copied the diags from the end of this snap
+      let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray
+
+      -- Level is completed if there are no errrors or warnings
+      let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error)
+      let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)
+
+      let mut intermediateGoalCount := 0
+
+      -- only the positions that have non-whitespace characters since the last position
+      -- should add a new proof step.
+      let positionsWithSource : Array (String.Pos × String) :=
+        text.positions.zipWithIndex.filterMap (
+          fun (pos, i) => match i with
+          | 0 => some (pos, "")
+          | i' + 1 =>
+            let source : String := Substring.toString ⟨text.source, text.positions.get! i', pos⟩
+            if source.trim.length == 0 then
+              none
+            else
+              some (pos, source))
+
+      -- Drop the last position as we ensured that there is always a newline at the end
+      for ((pos, source), i) in positionsWithSource.zipWithIndex do
+        -- iterate over all steps in the proof and get the goals and hints at each position
+
+        -- diags are labeled in Lsp-positions, which differ from the lean-internal
+        -- positions by `1`.
+        let lspPosAt := text.utf8PosToLspPos pos
+
+        let mut diagsAtPos : Array InteractiveDiagnostic := filterUnsolvedGoal <|
+          -- `+1` for getting the errors after the line.
+          match i with
+          | 0 =>
+            -- `lspPosAt` is `(0, 0)`
+            diag.filter (fun d => d.range.start == lspPosAt )
+          | i' + 1 =>
+            diag.filter (fun d =>
+              ((text.utf8PosToLspPos <| (positionsWithSource.get! i').1) ≤ d.range.start) ∧
+              d.range.start < lspPosAt )
+
+        if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text pos then
+          let goalsAtPos' : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
+            fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
+              -- TODO: What does this function body do?
+              -- let ciAfter := { ci with mctx := ti.mctxAfter }
+              let ci := if useAfter then
+                  { ci with mctx := tacticInfo.mctxAfter }
+                else
+                  { ci with mctx := tacticInfo.mctxBefore }
+              -- compute the interactive goals
+              let goalMvars : List MVarId ← ci.runMetaM {} do
+                return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
+
+              let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
+                goalMvars.mapM fun goal => do
+                  let hints ← findHints goal doc.meta rc.initParams
+                  let interactiveGoal ← goalToInteractive goal
+                  return ⟨interactiveGoal, hints⟩
+              -- TODO: This code is way old, can it be deleted?
+              -- compute the goal diff
+              -- let goals ← ciAfter.runMetaM {} (do
+              --     try
+              --       Widget.diffInteractiveGoals useAfter ti goals
+              --     catch _ =>
+              --       -- fail silently, since this is just a bonus feature
+              --       return goals
+              -- )
+              return interactiveGoals
+          let goalsAtPos : Array InteractiveGoalWithHints := ⟨goalsAtPos'.foldl (· ++ ·) []⟩
+
+          diagsAtPos ← completionDiagnostics goalsAtPos.size intermediateGoalCount
+            completed completedWithWarnings lspPosAt diagsAtPos
+
+          intermediateGoalCount := goalsAtPos.size
+
+          steps := steps.push ⟨goalsAtPos, source, diagsAtPos, lspPosAt.line, lspPosAt.character⟩
+        else
+          -- No goals present
+          steps := steps.push ⟨#[], source, diagsAtPos, lspPosAt.line, none⟩
+
+      -- Filter out the "unsolved goals" message
+      diag := filterUnsolvedGoal diag
+
+      let lastPos := text.utf8PosToLspPos positionsWithSource.back.1
+      let remainingDiags : Array InteractiveDiagnostic :=
+        diag.filter (fun d => lastPos ≤ d.range.start)
+
+      return some {
+        steps := steps,
+        diagnostics := remainingDiags,
+        completed := completed,
+        completedWithWarnings := completedWithWarnings,
+        lastPos := lastPos.line
+        }
+
+open RequestM in
+
+-- The editor apparently uses this
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option <| InteractiveGoals)) := do
+  let doc ← readDoc
+  -- let rc ← readThe RequestContext
+  let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
   -- TODO: I couldn't find a good condition to find the correct snap. So we are looking
   -- for the first snap with goals here:
   withWaitFindSnap doc (fun s => ¬ (s.infoTree.goalsAt? doc.meta.text hoverPos).isEmpty)
     (notFoundX := return none) fun snap => do
       if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        let goals : List InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+        let goals : List <| Array InteractiveGoal ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
           let ciAfter := { ci with mctx := ti.mctxAfter }
           let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
           -- compute the interactive goals
@@ -153,8 +345,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
             return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
           let goals ← ci.runMetaM {} do
              goals.mapM fun goal => do
-              let hints ← findHints goal doc rc.initParams
+              -- let hints ← findHints goal doc.meta rc.initParams
-              return ← goalToInteractive goal hints
+              return ← goalToInteractive goal
           -- compute the goal diff
           -- let goals ← ciAfter.runMetaM {} (do
           --     try
@@ -163,8 +355,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           --       -- fail silently, since this is just a bonus feature
           --       return goals
           -- )
-          return {goals}
+          return goals
-        return some <| goals.foldl (· ++ ·) ⟨#[]⟩
+        return some <| ⟨goals.foldl (· ++ ·) #[]⟩
       else
         return none
 
@@ -172,7 +364,16 @@ builtin_initialize
   registerBuiltinRpcProcedure
     `Game.getInteractiveGoals
     Lsp.PlainGoalParams
-    (Option InteractiveGoals)
+    (Option <| InteractiveGoals
+    )
     getInteractiveGoals
 
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Game.getProofState
+    Lsp.PlainGoalParams
+    (Option ProofState)
+    getProofState
+
+
 end GameServer

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

@@ -0,0 +1,102 @@
+import Lean.Widget.InteractiveGoal
+import Lean.Widget.InteractiveDiagnostic
+import Lean.Data.Lsp.Diagnostics
+
+/-!
+This file contains the custom data structures use by the server.
+
+Some of them overwrite built-in structures from Lean.
+
+In particular, the structures from `Lean.Widget.InteractiveGoal` are duplicated with
+the following extension:
+
+* `isAssumption?` in `InteractiveHypothesisBundle`: stores if a hypothesis is of type `Prop`.
+
+NOTE: Changes here need to be reflected in  the corresponding `interface` in `rcp_api.ts`
+on the client-side.
+-/
+
+open Lean Server Widget
+
+namespace GameServer
+
+/-- Extend the interactive hypothesis bundle with an option to distinguish
+"assumptions" from "objects". "Assumptions" are hypotheses of type `Prop`. -/
+-- @[inherit_doc Lean.Widget.InteractiveHypothesisBundle]
+structure InteractiveHypothesisBundle extends Lean.Widget.InteractiveHypothesisBundle where
+  /-- The hypothesis's type is of type `Prop` -/
+  isAssumption? : Option Bool := none
+deriving RpcEncodable
+
+-- duplicated but with custom `InteractiveHypothesisBundle`
+@[inherit_doc Lean.Widget.InteractiveGoalCore]
+structure InteractiveGoalCore where
+  hyps : Array InteractiveHypothesisBundle
+  type : CodeWithInfos
+  ctx : WithRpcRef Elab.ContextInfo
+
+-- duplicated but with custom `InteractiveGoalCore`
+@[inherit_doc Lean.Widget.InteractiveGoal]
+structure InteractiveGoal extends InteractiveGoalCore where
+  userName? : Option String
+  goalPrefix : String
+  mvarId : MVarId
+  isInserted? : Option Bool := none
+  isRemoved? : Option Bool := none
+deriving RpcEncodable
+
+-- duplicated with custom `InteractiveGoalCore`
+@[inherit_doc Lean.Widget.InteractiveTermGoal]
+structure InteractiveTermGoal extends InteractiveGoalCore where
+  range : Lsp.Range
+  term : WithRpcRef Elab.TermInfo
+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. -/
+structure InteractiveGoalWithHints where
+  goal : InteractiveGoal
+  /-- Extended the `InteractiveGoal` by an array of hints at that goal. -/
+  hints : Array GameHint
+deriving RpcEncodable
+
+structure InteractiveGoalsWithHints where
+  goals : Array InteractiveGoalWithHints
+  /-- The content of the line evaluated. -/
+  command : String
+  diags : Array InteractiveDiagnostic := default
+  line : Option Nat -- only for debugging
+  column : Option Nat -- only for debugging
+
+deriving RpcEncodable
+
+instance : Inhabited InteractiveGoalsWithHints := ⟨default, default, default, none, none⟩
+
+/-- Collected goals throughout the proof. Used for communication with the game client. -/
+structure ProofState where
+  /-- goals after each line. includes the hints. -/
+  steps : Array <| InteractiveGoalsWithHints
+  /-- diagnostics contains all errors and warnings.
+
+  TODO: I think they contain information about which line they belong to. Verify this.
+  -/
+  diagnostics : Array InteractiveDiagnostic := default
+  /-- Whether the level is considered solved. -/
+  completed : Bool
+  completedWithWarnings : Bool
+  lastPos : Nat -- only for debugging
+deriving RpcEncodable

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,6 +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
+
 
 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
+Statement My.add_assoc (n m x : Nat) : (m + n) + x = m + (n + x) := by
-  rw [Nat.add_comm]
+  rw [Nat.add_assoc]
 
-example (n m : Nat) : n + m = m + n := by
+example (n m : Nat) : (m + n) + x = m + (n + x) := by
   simp
 
-#check My.add_comm
+#check My.add_assoc
+
+Statement My.add_comm (preamble := simp [add_comm m n]) (n m : Nat) : n + (m + 0) = m + n := by
+  rw [Nat.add_comm]

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: {