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/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

@@ -26,6 +26,11 @@
       "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

@@ -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/EnvExtensions.lean

@@ -190,7 +190,7 @@ def getCurLayer [MonadError m] : m Layer := do
 def getCurGameId [Monad m] : m Name := do
   match curGameExt.getState (← getEnv) with
   | some game => return game
-  | none => return (.mkSimple defaultGameName)
+  | none => return defaultGameName
 
 /-- Get the current world -/
 def getCurWorldId [MonadError m] : m Name := do
@@ -468,8 +468,8 @@ def getLevel? (levelId : LevelId) : m (Option GameLevel) := do
 
 def getCurGame [Monad m] : m Game := do
   let some game ← getGame? (← getCurGameId)
-    | let game := {name := (.mkSimple defaultGameName)}
-      insertGame (.mkSimple defaultGameName) game
+    | let game := {name := defaultGameName}
+      insertGame defaultGameName game
       return game
   return game
 

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/Helpers/PrettyPrinter.lean

@@ -3,7 +3,7 @@ import Lean.PrettyPrinter.Delaborator.Builtins
 import Lean.PrettyPrinter
 import Lean
 
-import Batteries.Tactic.OpenPrivate
+import Std.Tactic.OpenPrivate
 
 namespace GameServer
 

server/GameServer/ImportModules.lean

@@ -1,5 +1,5 @@
 import Lean.Environment
-import Batteries.Tactic.OpenPrivate
+import Std.Tactic.OpenPrivate
 import Lean.Data.Lsp.Communication
 
 open Lean

server/GameServer/Inventory.lean

@@ -124,7 +124,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
     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 (.mkSimple val)}
+      return {acc with tactics := acc.tactics.insert val}
     else
       return acc
   | .ident _info _rawVal val _preresolved =>

server/GameServer/RpcHandlers.lean

@@ -17,7 +17,7 @@ def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String)
   let fileParts := fileName.splitOn "/"
   if fileParts.length == 3 then
     if let (some level, some game) := (fileParts[2]!.toNat?, initParams.rootUri?) then
-      return some {game := .mkSimple game, world := .mkSimple fileParts[1]!, level := level}
+      return some {game, world := fileParts[1]!, level := level}
   return none
 
 def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do
@@ -123,7 +123,7 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
           let mut hintFVarsNames : Array Expr := #[]
           for fvar in hintFVars do
             let name₁ ← fvar.fvarId!.getUserName
-            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨.mkSimple s!"«\{{name₁}}»"⟩
+            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
@@ -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.

server/GameServer/Utils.lean

@@ -35,7 +35,7 @@ elab "#show_option" verbose:(ppSpace showOptArg)? id:(ppSpace Parser.rawIdent)?
     | .ofNat val => s!"Nat := {repr val}"
     | .ofInt val => s!"Int := {repr val}"
     | .ofSyntax val => s!"Syntax := {repr val}"
-    if let some val := opts.find (.mkSimple name) then
+    if let some val := opts.find name then
       msg1 := s!"{msg1}  (currently: {val})"
     msg := match verbose with
     | some opt =>

server/lake-manifest.json

@@ -1,13 +1,13 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries.git",
+ [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "51e6e0d24db9341fb031288c298b7e6b56102253",
-   "name": "batteries",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0",
+   "inputRev": "v4.7.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
@@ -22,20 +22,20 @@
   {"url": "https://github.com/hhu-adam/lean-i18n.git",
    "type": "git",
    "subDir": null,
-   "rev": "5158ce6720d88fa1f53fdb86aea8d515af69571c",
+   "rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39",
    "name": "i18n",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0",
+   "inputRev": "v4.7.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
+   "rev": "ac07367cbdd57440e6fe78e5be13b41f9cb0f896",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0",
+   "inputRev": "v4.7.0",
    "inherited": false,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "GameServer",
  "lakeDir": ".lake"}

server/lakefile.lean

@@ -6,7 +6,7 @@ package GameServer
 -- Using this assumes that each dependency has a tag of the form `v4.X.0`.
 def leanVersion : String := s!"v{Lean.versionString}"
 
-require batteries from git "https://github.com/leanprover-community/batteries.git" @ leanVersion
+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
@@ -28,4 +28,4 @@ post_update pkg do
   let rootPkg ← getRootPackage
   if rootPkg.name = pkg.name then
     return -- do not run in GameServer itself
-  discard <| runBuild gameserver.fetch
+  discard <| runBuild gameserver.build >>= (·.await)

server/lean-toolchain

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

vite.config.ts

@@ -31,6 +31,7 @@ export default defineConfig({
     })
   ],
   publicDir: "client/public",
+  base: "/", // setting this to `/leangame/` means the server is now accessible at `localhost:3000/leangame`
   optimizeDeps: {
     exclude: ['games']
   },