update lean4game tutorial

docs/tutorial/install.md

@@ -52,36 +52,21 @@ del elan-x86_64-pc-windows-msvc.zip
 wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile
 ```
 
-该命令执行了一个脚本：[install_debian.sh](https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh)，主要安装了 VsCode，Lean 插件，以及 elan。
+该命令通过执行脚本 [install_debian.sh](https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh) 安装了 VsCode，Lean 插件，以及 elan。
 
-如果访问 GitHub 存在问题，可以在安装 VS Code 和 Lean 插件后，手动安装 elan。
+如果访问 GitHub 存在问题，可以手动安装 VS Code 和 Lean 插件以及 elan。
 
-在 GitHub [release 页面](https://github.com/leanprover/elan/releases)根据系统版本下载新版 elan，比如 `linux-x86_64` 系统的 elan 安装器地址为：
+具体地，访问 GitHub [release 页面](https://github.com/leanprover/elan/releases)或者 [上交镜像源](https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/mirror_clone_list.html) ，根据系统版本下载新版 elan。
 
-```bash
-https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz
-```
-
-或者在[上交镜像源](https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/mirror_clone_list.html)下载，查询你自己系统对应的 elan 版本。
-
-如果不确定系统架构，执行 `uname -s` 和 `uname -m` 查看：
-
-```bash
-❯ uname -s
-Linux
-❯ uname -m
-x86_64
-```
-
-下载文件并解压：
+比如 `linux-x86_64` 系统的 elan 工具并解压：
 
 ```bash
 # 如果网络不行就本地下载再上传
-curl https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
+curl -L https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
 tar xf elan.tar.gz
 ```
 
-解压得到 `elan-init` 文件，赋予可执行权限并执行：
+解压得到 `elan-init` 文件，赋予可执行权限并执行安装：
 
 ```bash
 chmod +x elan-init
@@ -95,6 +80,7 @@ export PATH="$HOME/.elan/bin:$PATH"
 ```
 
 重启终端，检查 `elan` 版本和默认安装的 Lean 版本：
+
 ```bash
 ❯ elan -V
 elan 3.1.1 (71ddc6633 2024-02-22)

docs/tutorial/lean4game.md

@@ -3,7 +3,7 @@
 
 本篇介绍如何用 Lean4Game 添加 Lean4 游戏。这类互动游戏不仅利于 Lean 本身的学习，还能促进对学科知识的理解，让关联的学科群体对 Lean 有更直观的认识。
 
-当前在个人服务器部署了社区游戏：[nng4.leanprover.cn](https://nng4.leanprover.cn) ，后续计划写一个李代数入门的（mark 开坑）。
+当前部署了 NNG4 游戏：[nng4.leanprover.cn](https://nng4.leanprover.cn) ，可在线体验，后续计划写一个李代数入门的（mark 开坑）。
 
 ### 相关项目与资源
 
@@ -13,7 +13,7 @@
 - **GameSkeleton**：Lean4 游戏的模板代码（[GitHub 仓库](https://github.com/hhu-adam/GameSkeleton.git)）。
 - **NNG4**：自然数游戏，从皮亚诺公理开始，构建自然数的基本运算和性质（[GitHub 仓库](https://github.com/leanprover-community/NNG4)）。
 
-社区官网目前贴了自然数和集合论等游戏，也欢迎根据自己的学科知识，贡献更多的游戏~
+社区官网目前提供了自然数和集合论等游戏，也欢迎根据自己的学科知识，贡献更多的游戏~
 
 <!-- ![20240623160501](https://qiniu.wzhecnu.cn/PicBed6/picgo/20240623160501.png) -->
 
@@ -23,7 +23,7 @@
 
 ### 下载游戏模板
 
-首先，下载 GameSkeleton 模板仓库：
+首先，下载 GameSkeleton 模板仓库，这个是网页上最终展示的内容：
 
 ```bash
 git clone https://github.com/hhu-adam/GameSkeleton.git
@@ -69,36 +69,41 @@ lake build
 
 Lean4Game 是游戏的前后端框架，用于创建游戏的主页面。
 
-首先，安装 Node.js 和 npm，然后下载 Lean4Game，并将其放在游戏的**同级目录**：
+首先，安装 Node.js 和 npm
 
 ```bash
 # 安装 nvm
 curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.3/install.sh | bash
 # 安装 nodejs
 nvm install node
 nvm use node
+```
+
+下载 Lean4Game，并将其放在游戏的**同级目录**：
+
+```bash
 # 下载 Lean4Game
 git clone https://github.com/leanprover-community/lean4game.git
 cd lean4game
 # 安装依赖
 npm install --force
 ```
 
-推荐使用的 Node 版本是 `22.2.0`。执行 `npm start` 启动游戏，或者指定服务端口：
+设置环境变量（可选）：
 
 ```bash
 export PORT=8080
 export CLIENT_PORT=3000
-npm start
+export VITE_CLIENT_DEFAULT_LANGUAGE=zh
 ```
 
-这里 `PORT` 为运行 Lean 代码的后端端口，默认是 8080；`CLIENT_PORT` 为前端访问端口，默认是 3000。
+其中 `PORT` 为运行 Lean 代码的后端端口，默认是 `8080`；`CLIENT_PORT` 为前端访问端口，默认是 `3000`；`VITE_CLIENT_DEFAULT_LANGUAGE` 为界面语言，默认为 `en`。
 
-如果看到以下页面，就表示访问成功：
+执行 `npm start` 启动游戏，如果看到以下页面，就表示访问成功：
 
 ![20240623121710](https://qiniu.wzhecnu.cn/PicBed6/picgo/20240623121710.png)
 
-此外，可以在右上角的偏好设置中选择语言：
+此外，可以在右上角的偏好设置切换语言：
 
 ![20240623164430](https://qiniu.wzhecnu.cn/PicBed6/picgo/20240623164430.png)