Specify that logs should be created relative to the current working directory.

feat: Generate a structure of Korean document

.gitignore

@@ -3,3 +3,4 @@ client/dist
 games/
 server/.lake
 **/.DS_Store
+logs/

README.md

@@ -54,7 +54,7 @@ Providing the use access to a Lean instance running on the server is a severe se
 
 ## Credits
 
-The project has pimarily been developed by Alexander Bentkamp and Jon Eugster.
+The project has primarily been developed by Alexander Bentkamp and Jon Eugster.
 
 It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)

client/public/locales/es/translation.json

@@ -0,0 +1,94 @@
+ {
+  "Intro": "Introducción",
+  "Game Introduction": "Introducción del juego",
+  "World selection": "Seleccionar mundo",
+  "Start": "Empezar",
+  "Inventory": "Inventario",
+  "next level": "siguiente nivel",
+  "Next": "Siguiente",
+  "back to world selection": "volver a la selección de mundos",
+  "Leave World": "Abandonar mundo",
+  "previous level": "nivel anterior",
+  "Previous": "Anterior",
+  "Editor mode is enforced!": "¡El modo editor es obligatorio!",
+  "Editor mode": "Modo editor",
+  "Typewriter mode": "Modo línea a línea",
+  "information, Impressum, privacy policy": "información, Impressum, política de privacidad",
+  "Preferences": "Preferencias",
+  "Game Info & Credits": "Información del juego y reconocimientos",
+  "Game Info": "Información del juego",
+  "Clear Progress": "Limpiar el progreso",
+  "Erase": "Borrar",
+  "Download Progress": "Descargar progreso",
+  "Download": "Descargar",
+  "Load Progress from JSON": "Cargar progreso desde JSON",
+  "Upload": "Subir",
+  "Home": "Inicio",
+  "back to games selection": "volver a la selección de juegos",
+  "close inventory": "cerrar inventario",
+  "show inventory": "mostrar inventario",
+  "World": "Mundo",
+  "Show more help!": "¡Mostrar más ayuda!",
+  "Goal": "Objetivo",
+  "Objects": "Objetos",
+  "Assumptions": "Hipótesis",
+  "Current Goal": "Objetivo actual",
+  "Further Goals": "Objetivos pendientes",
+  "No Goals": "Sin objetivos",
+  "Loading goal…": "Cargando objetivo…",
+  "Click somewhere in the Lean file to enable the infoview.": "Pulsa en algún lugar del archivo Lean para habilitar la vista de información.",
+  "Waiting for Lean server to start…": "Esperando a que el servidor Lean se inicie…",
+  "Level completed! 🎉": "Nivel completado 🎉",
+  "Level completed with warnings 🎭": "Nivel completado con advertencias 🎭",
+  "Failed command": "Comando fallido",
+  "Retry proof from here": "Reintentar la prueba desde aquí",
+  "Retry": "Reintentar",
+  "Active Goal": "Objetivo activo",
+  "Crashed! Go to editor mode and fix your proof! Last server response:": "¡Error! Vaya al modo editor y corrija su prueba. Última respuesta del servidor:",  
+  "Line": "Línea",
+  "Character": "Carácter",
+  "Loading messages…": "Cargando mensajes…",
+  "Execute": "Ejecutar",
+  "Tactics": "Tácticas",
+  "Definitions": "Definiciones",
+  "Theorems": "Teoremas",
+  "Not unlocked yet": "No desbloqueado aún",
+  "Not available in this level": "No disponible en este nivel",
+  "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Un repositorio de juegos para aprender el asistente de demostración <1>Lean</1>, <i>(Lean 4)</i> y su biblioteca matemática <5>mathlib</5> ",
+  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No se ha cargado ningún juego. Use <1>http://localhost:3000/#/g/local/FOLDER</1> para abrir un juego directamente desde una carpeta local",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "<p>Como este servidor corre en máquinas de nuestra universidad, tiene una capacidad limitada. Nuestra estimación actual es de unos 70 juegos simultaneos. Esperamos afrontar y comprobar mejor esta limitación en el futuro.</p>. <1>Muchos aspectos de los juegos y la infrastructura están aún en desarrollo. No dude en abrir una <1>GitHub Issue</1> sobre cualquier problema que experimente.</1>",
+  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>Si está considerando escribir su propio juego, use el <1>GameSkeleton Github Repo</1> como plantilla y lea <3>How to Create a Game</3>.</0><1>Puede cargar directamente los juegos en el servidor y jugarlo usando la URL adecuada. Las <1>instrucciones anteriores</1> también explican los detalles sobre cómo cargar su juego en el servidor. Le animamos a ponerse en contacto con nosotros si tiene preguntas.</1><p>Los juegos incluidos en esta página son añadidos manualmente. Por favor, contactenos y añadiremos el suyo encantados.</p>",
+  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "Este  servidor se ha desarrollado como parte del proyecto <1>ADAM : Anticipating the Digital Age of Mathematics</1> en la Heinrich-Heine-Universität de Düsseldorf.",
+  "Prerequisites": "Requisitos previos",
+  "Worlds": "Mundos",
+  "Levels": "Niveles",
+  "Language": "Idioma",
+  "Lean Game Server": "Servidor de Juegos de Lean",
+  "Development notes": "Notas de desarrollo",
+  "Adding new games": "Añadir nuevos juegos",
+  "Funding": "Financiación",
+  "Level": "Nivel",
+  "Introduction": "Introducción",
+  "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>" : "<p>¿Desea eliminar su progreso guardado definitivamente?</p><p>(Esto elimina sus pruebas y su inventario recopilado. Los progresos guardados de otros juegos no se eliminan.)</p>",
+  "Delete Progress?": "¿Borrar Progreso?",
+  "Delete": "Borrar",
+  "Download & Delete": "Descargar y Borrar",
+  "Cancel": "Cancelar",
+  "Mobile": "Móvil",
+  "Auto": "Automático",
+  "Desktop": "Escritorio",
+  "Layout": "Diseño",
+  "Always visible": "Siempre visible",
+  "Save my settings (in the browser store)": "Guardar mis ajustes (en el almacenamiento del navegador)",
+  "<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Las reglas del juego determinan si se permite saltarse niveles y si el juego realiza comprobaciones para permitir únicamente tácticas y teoremas desbloqueados en las pruebas.</p><1>Nota: las tácticas (o teoremas) \"Desbloqueadas\" está determinadas por dos cosas: el conjunto mínimo de tácticas necesarias para resolver un nivel, más cualquier táctica que hayas desbloqueado en otro nivel. Esto significa que si desbloqueas <1>simp</1> en un nivel, puedes usarlo a partir de entonces en cualquier nivel.</1><p>Las opciones son:</p>",
+  "Game Rules": "Reglas del juego",
+  "levels": "niveles",
+  "tactics": "tácticas",
+  "regular": "normal",
+  "relaxed": "relajado",
+  "none": "ninguno",
+  "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Seleccione un archivo JSON con el progreso del juego guardado para cargar su progreso.</p><1><0>Advertencia:</0> Esto borrará su progreso actual en el juego. Considere <2>descargar su progreso actual</2> antes</1>",
+  "Upload Saved Progress": "Subir progreso guardado",
+  "Load selected file": "Cargar archivo seleccionado",
+  "Rules": "Reglas"
+}

client/public/locales/kr/translation.json

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

client/public/locales/zh/translation.json

@@ -1,7 +1,7 @@
 {
   "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>",
+  "Lean Game Server": "LEAN 游戏服务器",
+  "<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>游戏规则决定是否允许跳过关卡，以及游戏是否只允许在证明中使用已解锁的策略和定理。</p><1>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在其他关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp</1>，你可以在任何关卡中使用它。</1><p>选项有：</p>",
   "Game Rules": "游戏规则",
   "levels": "关卡",
   "tactics": "策略",
@@ -20,11 +20,11 @@
   "Leave World": "离开世界",
   "previous level": "上一关",
   "Previous": "上一关",
-  "Editor mode is enforced!": "编辑器模式开启！",
+  "Editor mode is enforced!": "编辑器模式已启用！",
   "Editor mode": "编辑器模式",
   "Typewriter mode": "打字机模式",
-  "information, Impressum, privacy policy": "",
-  "Preferences": "",
+  "information, Impressum, privacy policy": "信息、版权说明、隐私政策",
+  "Preferences": "偏好设置",
   "Game Info & Credits": "游戏信息和荣誉",
   "Game Info": "游戏信息",
   "Clear Progress": "清除进度",
@@ -43,14 +43,14 @@
   "Current Goal": "当前目标",
   "Objects": "对象",
   "Assumptions": "假设",
-  "Further Goals": "Further Goals",
+  "Further Goals": "进一步目标",
   "No Goals": "无目标",
-  "Loading goal…": "加载目标。。。",
-  "Click somewhere in the Lean file to enable the infoview.": "单击Lean文件中的某处以启用信息视图。",
-  "Waiting for Lean server to start…": "等待 Lean 服务器启动。。。",
-  "Level completed! 🎉": "完成关卡！🎉",
+  "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": "从这里重新试着证明",
+  "Retry proof from here": "从这里重新尝试证明",
   "Active Goal": "当前目标",
   "Crashed! Go to editor mode and fix your proof! Last server response:": "程序崩溃！请转到编辑器模式，修复您的证明！最后一次服务器响应：",
   "Line": "行",
@@ -61,34 +61,35 @@
   "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.": "",
+  "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "这是一个为证明助手 <1>Lean</1> <i>(Lean 4)</i> 及其数学库 <5>mathlib</5> 设计的学习游戏库",
+  "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "未加载游戏。访问 <1>http://localhost:3000/#/g/local/FOLDER</1> 从本地文件夹打开游戏。",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "<p>这个服务器部署在我们大学的机器上，运行能力有限，目前估计最多可同时支持约 70 个游戏。我们希望将来能更有效地解决并测试这些限制。</p><1>游戏和基础设施的许多方面仍在开发之中。如果您遇到任何问题，欢迎在 <1>GitHub</1> 上提交问题反馈。</1>",
+  "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>如果你打算编写自己的游戏，可以使用 <1>GameSkeleton Github Repo</1> 作为模板，并参阅 <3>如何创建游戏</3>。</0><1>你可以直接将游戏上传至服务器，并通过正确的 URL 进行游戏。上面的 <1>说明</1> 已详细介绍了如何将游戏加载到服务器的步骤。如果你有任何疑问，请随时联系我们。</1><p>本页上的精选游戏都是手动添加的。如果你想添加你的游戏，请与我们联系，我们非常欢迎。</p>",
+
+  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "此服务器是 Heinrich-Heine-Universität Düsseldorf 项目 <1>ADAM：预见数学的数字时代</1> 的一部分。",
   "Prerequisites": "前置条件",
-  "Worlds": "世界(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>",
+  "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>",
+  "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": ""
+  "Level": "关卡",
+  "Introduction": "介绍",
+  "Retry": "重试",
+  "Failed command": "命令失败"
 }

client/src/components/landing_page.tsx

@@ -95,6 +95,9 @@ function LandingPage() {
   const closePreferencesPopup = () => setPreferencesPopup(false);
   const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup);
 
+  const [usageCPU, setUsageCPU] = React.useState<number>()
+  const [usageMem, setUsageMem] = React.useState<number>()
+
   const { t, i18n } = useTranslation()
 
   // Load the namespaces of all games
@@ -117,6 +120,29 @@ function LandingPage() {
     return q.data?.tile
   })
 
+  /** Parse `games/stats.csv` if present and display server capacity. */
+  React.useEffect(() => {
+    fetch(`${window.location.origin}/data/stats`)
+    .then(response => {if (response.ok) {
+      return response.text() } else {throw ""}})
+    .then(data => {
+      // Parse the CSV content
+      const lines = data.split('\n');
+      const [header, line2] = lines;
+      if (!(header.replace(' ', '').startsWith("CPU,MEM"))) {
+        console.info("Not displaying server stats: received unexpected: ", header)
+      }
+      if (line2) {
+        let values = line2.split(',')
+        setUsageCPU(100 * Number(values[0]));
+        setUsageMem(100 * Number(values[1]));
+      }
+    }).catch(err => {
+      console.info('server stats unavailable')
+      console.debug(err)
+    })
+  }, [])
+
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
       <nav className="landing-page-nav">
@@ -155,6 +181,18 @@ function LandingPage() {
         ))
       }
     </div>
+    { // show server capacity from `games/stats.csv` if present
+      (usageMem >= 0 || usageCPU >= 0 ) &&
+      <section>
+        <div className="wrapper">
+          <h2>{t("Server capacity")}</h2>
+          <p>
+            { usageMem >= 0 && <> {t("RAM")}: <strong>{usageMem} % </strong> {t("used")}.<br/></> }
+            { usageCPU >= 0 && <> {t("CPU")}: <strong>{usageCPU} % </strong> {t("used")}. </> }
+          </p>
+        </div>
+      </section>
+    }
     <section>
       <div className="wrapper">
         <h2>{t("Development notes")}</h2>

client/src/config.json

@@ -21,6 +21,16 @@
       "iso": "zh",
       "flag": "CN",
       "name": "中文"
+    },
+    {
+      "iso": "es",
+      "flag": "ES",
+      "name": "Español"
+    },
+    {
+      "iso": "kr",
+      "flag": "KR",
+      "name": "한국어"
     }
   ]
 }

client/src/state/preferences.ts

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

doc/create_game.md

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

doc/hints.md

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

doc/latex.md

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

doc/npm_scripts.md

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

doc/server.md

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

index.html

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

relay/index.mjs

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

relay/stats.sh

@@ -0,0 +1,10 @@
+#!/bin/bash
+
+# first argument is the process ID
+pid="$1"
+
+# number of CPUs available
+nproc=$(nproc --all)
+
+# hacky way to print the content of a CSV file containing CPU/Mem usage of the process
+top -bn2 -p $pid | awk -v nproc=$nproc 'NR > 16 {$12=substr($0,72); printf "CPU, MEM\n%.2f, %.2f\n", $9/nproc, $10}'

server/GameServer/AbstractCtx.lean

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

server/GameServer/Commands.lean

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

server/GameServer/FileWorker.lean

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

server/GameServer/RpcHandlers.lean

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

server/GameServer/Tactic/LetIntros.lean

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

vite.config.ts

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