Merge pull request #11 from Lean-zh/rex/update-tutorial

Update tutorial

Author: RexWzh

docs/tutorial/repl.md

@@ -2,27 +2,27 @@
 
 ## 项目概要
 
-REPL (Read-Eval-Print Loop) 是一个交互式编程环境，它允许用户输入命令，执行并看到结果。Lean 4 REPL 基于 JSON 通信的交互式环境，它支持三种工作模式。
+REPL (Read-Eval-Print Loop) 是一个交互式编程环境，允许用户输入命令，执行并查看结果。Lean 4 REPL 基于 JSON 通信，支持三种工作模式。
 
 ### 命令模式 (Command Mode)
 
-在命令模式下，你可以发送完整的 Lean 命令（如声明、定义等）到 REPL。命令以 JSON 格式发送，可以选择性地指定环境：
+在命令模式下，可以发送完整的 Lean 命令（如声明、定义等）到 REPL，比如：
 
 ```json
 { "cmd": "def f := 2" }
 ```
 
 ### 文件模式 (File Mode)
 
-文件模式是命令模式的一个简单封装，允许你直接读取和执行整个 Lean 文件的内容。例如：
+文件模式是命令模式的简单封装，允许直接读取和执行整个 Lean 文件的内容。例如：
 
 ```json
 { "path": "test/file.lean", "allTactics": true }
 ```
 
 ### 策略模式 (Tactic Mode)
 
-策略模式允许你使用 Lean 的证明策略（tactics）来交互式地构建证明。这个模式通常从一个包含 `sorry` 的命令开始，然后逐步完成证明。
+策略模式允许使用 Lean 的证明策略（tactics）来交互式地构建证明。这个模式通常从一个包含 `sorry` 的命令开始，然后逐步完成证明。
 
 ## 安装与基本使用
 
@@ -40,21 +40,25 @@ lake update -R && lake build
 
 ### 基本使用
 
-REPL 通过标准输入输出流进行通信，并使用 JSON 格式：
+进入仓库，通过 `lake exe repl` 启动交互式终端，输入 JSON 块，获取相应的输出。
+
+此外，也可以通过标准输入输出流进行通信，比如：
 
 ```bash
 echo '{ "cmd": "def f := 2" }' | lake exe repl
 ```
 
 ## REPL 命令模式
 
-下边，我们分别介绍 REPL 的这三种模式，以及 Pickle 特性。先从最基础的 **命令模式** 开始。
+下边，我们详细介绍 REPL 的三种模式，以及 Pickle 特性。先从最基础的 **命令模式** 开始。
 
 ### 状态跟踪
 
-REPL 的命令模式通过 `env` 字段跟踪环境状态，每次执行 `cmd` 命令后会返回一个新的环境编号。这种机制允许我们：
-1. 在已有环境的基础上执行新命令
-2. 通过指定特定的 `env` 值回溯到之前的状态
+REPL 的命令模式通过 `env` 字段跟踪环境状态，每次执行 `cmd` 命令后会返回一个新的环境编号。这种机制有很多好处：
+
+1. **状态追踪**：允许在一个交互终端中启用多个环境，比如 `import` 不同的模块，每个命令执行后都会生成新的环境编号
+2. **环境选择**：允许通过指定 `env` 值回溯到之前的状态，在该环境的基础上执行新命令
+3. **环境隔离**：不同环境的变量相互独立
 
 ### 示例解析
 
@@ -77,28 +81,21 @@ REPL 的命令模式通过 `env` 字段跟踪环境状态，每次执行 `cmd` 
 4. 基于 env 1 执行相同操作，并创建新环境 env 3
 5. 基于 env 2 重新定义 `f3`，报错：`'f3' has already been declared`，并创建新环境 env 4
 
-### 特性概括
-
-1. **状态追踪**：每个命令执行后都会生成新的环境编号
-2. **环境选择**：可以通过 `env` 字段选择在哪个环境基础上执行新命令
-3. **错误处理**：重复定义等错误会被捕获并返回错误信息
-4. **环境隔离**：不同环境之间的定义是独立的
 
 ## REPL 策略模式
 
 策略模式（Tactic Mode）是 REPL 的核心功能，用于交互式证明构建。
 
-### 工作流程
+策略模式有以下特性：
 
-策略模式通过以下步骤展开：
-
-1. 使用 `sorry` 创建证明占位符
-2. REPL 返回 `proofState` 标识证明状态
-3. 通过策略命令逐步完成证明
+1. **状态创建**：使用 `sorry` 创建证明占位符，
+2. **状态追踪**：通过 `proofState` 标识状态索引，每个 `sorry` 按顺序生成 `proofState`，策略作用也会产生新的证明状态
+3. **多目标处理**：支持 pick 指定目标来进行下一步证明
+4. **灵活性**：支持各种证明策略，包括 `have, calc` 等，且允许分步构建复杂证明
 
 ### 示例解析
 
-为展示方便，我们将输出结果拼接到对应的输入行后边：
+为展示方便，我们将输出结果拼接到对应输入行后边：
 
 ```python
 # 步骤1：创建定理
@@ -158,13 +155,6 @@ REPL 的命令模式通过 `env` 字段跟踪环境状态，每次执行 `cmd` 
  "goals": ["x : Int\nh : x = 1\n⊢ x = 1"]}
 ```
 
-### 特性概括
-
-1. **状态追踪**：每个 `sorry` 按顺序生成 `proofState`，策略作用得到新的证明状态
-
-2. **多目标处理**：支持 pick 指定目标来进行下一步证明
-
-3. **灵活性**：支持各种证明策略，包括 `have, calc` 等，且允许分步构建复杂证明
 
 ## REPL 文件模式
 
@@ -208,20 +198,15 @@ echo '{"cmd" : "def f : Nat := 37\\ndef g := 2\\ntheorem h : f + g = 39 := by ex
 
 Pickle 特性允许我们将环境状态（env）或证明状态（proofState）保存到文件中，并在需要时重新加载。
 
-### 使用场景
-
-在 REPL 中，**每次输入命令都是作为独立的会话处理的**。这意味着：
-
-1. 如果我们想在之前的工作基础上继续，需要重新执行所有命令
-2. 对于复杂的证明过程，重复执行可能会很耗时
-3. 在多机协作时，可能需要共享证明状态
+**使用场景**：REPL 是以 Json 数据形式交互的，如果我们想还原当前的证明状态或环境，需要重新执行所有命令。对于复杂的证明过程，重复执行会很耗时。此外，在多机协作时，我们也需要共享证明状态。
 
 ### Pickle 的基本操作
 
-Pickle 支持两个基本操作：
+Pickle 的基本操作：
 
-1. **保存状态**（pickleTo）
+1. **保存环境/状态**（pickleTo）
 2. **加载状态**（unpickleProofStateFrom）
+3. **加载环境**（unpickleEnvFrom）
 
 ### 示例分析
 
@@ -247,7 +232,7 @@ Pickle 支持两个基本操作：
 
 ## 配置 Mathlib 依赖
 
-REPL 本身不依赖 Mathlib，但在实际使用中可能需要处理依赖 Mathlib 的项目。以 Lean 4.14.0 版本为例，有两种配置方式：
+REPL 本身不依赖 Mathlib，但我们可能需要处理包含 Mathlib 依赖的项目。以 Lean 4.14.0 版本为例，有两种解决方式：
 
 **方式一：直接添加 Mathlib 依赖**
 
@@ -280,7 +265,6 @@ echo '{ "cmd": "import Mathlib" }' | lake exe repl
 echo '{ "cmd": "import Mathlib" }' | lake env /path/to/repl/.lake/build/bin/repl
 ```
 
-
 ## 更多示例
 
 最后，附上 REPL 测试代码提供的示例，为展示方便，我们将输出结果拼接到对应的输入行后边。

mkdocs.yml

@@ -70,6 +70,8 @@ nav:
   - 主页: 
     - Lean-zh: index.md
     - 安装指南: install.md
+    - 版本管理与包管理: tutorial/elan-lake.md
+    - Lake 包管理: references/lake-doc.md   
   - 交互工具:
     - LeanDojo 教程: tutorial/lean-dojo.md
     - REPL 教程: tutorial/repl.md
@@ -78,7 +80,4 @@ nav:
   - 项目教程:
     - Lean4web 在线编译器: tutorial/lean4web.md
     - jixia 数据分析: tutorial/jixia.md
-    - Lean4Game 教程: tutorial/lean4game.md
-  - 其他:
-    - 版本管理与包管理: tutorial/elan-lake.md
-    - Lake 包管理: references/lake-doc.md    
+    - Lean4Game 教程: tutorial/lean4game.md