update lean-toolchain-tutorial

Author: RexWzh

docs/install.md

@@ -1,26 +1,30 @@
-# LEAN 4 安装教程 
+# LEAN 4 安装教程
 
-Lean 4 工作环境由以下几部分组成：
+Lean 是一个开源的定理证明助手和函数式编程语言，由微软研究院开发。它既可以用于形式化数学证明，也可以用于通用程序设计。
 
-1. [elan](https://github.com/leanprover/elan)：Lean 版本管理器。功能类似于 Rust 的 `rustup` 或 Node.js 的 `nvm`，用于安装、管理和切换不同版本的 Lean。
-2. [lake](https://github.com/leanprover/lake)：Lean 的包管理器，全称 Lean Make，已合并为 Lean 4 仓库源码的一部分。用于创建 Lean 项目，构建 Lean 包，配置 Mathlib 和编译 Lean 可执行文件。
-3. （非必须）[Mathlib](https://leanprover-community.github.io/mathlib4_docs/)：Lean 的数学库。
+## Lean 4 工具链
 
-为了使用 Lean，你需要先安装 [VS Code](https://code.visualstudio.com/) 和 Git，然后安装 elan，elan 会自动帮你安装 Lean 4 stable 以及 lake 包管理器，接下来就可以使用 lake 创建自己的 Lean 项目。
+Lean 4 的完整开发环境由以下核心组件构成：
 
-> 如果希望快速了解和使用 Lean，除了在本地安装，也可以通过 [live.lean-lang.org](https://live.lean-lang.org) 或 [live.leanprover.cn](https://live.leanprover.cn) 在线体验。
+1. [elan](https://github.com/leanprover/elan)：Lean 的版本管理工具，用于安装、管理和切换不同版本的 Lean，类似于 Rust 的 `rustup` 或 Node.js 的 `nvm`。
+2. [lake](https://github.com/leanprover/lake)（Lean Make）：Lean 的包管理器和构建器，已集成到 Lean 4 核心仓库中。用于创建 Lean 项目，构建 Lean 包,编译 Lean 可执行文件等。
+3. [lean](https://github.com/leanprover/lean4)：语言本身的核心组件，负责实际的代码编译和语言服务器协议（LSP）支持，用户不需要直接与 `lean` 交互。
 
-## Linux 安装 elan
+此外，还有 Lean 的标准数学库 [Mathlib](https://leanprover-community.github.io/mathlib4_docs/)，包含大量数学定义和定理，以及实用的证明工具和策略。
+
+为了使用 Lean，需要先安装 [VS Code](https://code.visualstudio.com/) 和 Git，然后安装 elan。再通过 elan 安装各个 Lean4 版本以及 lake 包管理器，接下来就可以使用 lake 创建自己的 Lean 项目。工具链的用法示例参见 [Lean 工具链](tutorial/elan-lake.md) 一节或 [lake 文档](references/lake-doc.md)。
 
-以下内容在 Ubuntu 22.04 系统上测试通过。
+> 如果希望快速了解和使用 Lean，除了在本地安装，也可以直接访问 [live.lean-lang.org](https://live.lean-lang.org) 或 [live.leanprover.cn](https://live.leanprover.cn) 在线体验。
+
+## Linux 安装 elan
 
 如果没有网络问题，用一行命令安装：
 
 ```bash
 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
 ```
 
-脚本执行内容包括：检查并安装 VsCode，Lean 插件以及 elan。
+脚本内容包括：检查并安装 VsCode，Lean 插件，并安装 elan。
 
 如果访问 GitHub 存在问题，可以在安装 vscode 后，手动安装 elan。
 
@@ -72,11 +76,11 @@ powershell -ExecutionPolicy Bypass -f elan-init.ps1
 del elan-init.ps1
 ```
 
-如果遇到了 `"SSL connect error", "Timeout was reached","Failed to connect to github.com port 443"...` 等错误，就是说明你的网络环境不理想。如果这样可以通过[上交镜像源](https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/mirror_clone_list.html)安装。下面演示在网络环境不理想的条件下的安装。
+如果遇到了 `"SSL connect error", "Timeout was reached","Failed to connect to github.com port 443"...` 等错误，就是说明你的网络环境不理想。如果这样可以通过[上交镜像源](https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/elan/releases/download/mirror_clone_list.html)下载安装。下面演示在网络环境不理想的条件下的安装。
 
 打开 cmd 或 Powershell，运行
 ```
-curl -O --location https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/elan/releases/download/eager-resolution-v5/elan-x86_64-pc-windows-msvc.zip
+curl -O --location https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/elan/releases/download/v4.0.0-rc1/elan-x86_64-pc-windows-msvc.zip
 unzip -o elan-x86_64-pc-windows-msvc.zip
 .\elan-init.exe
 ```

docs/tutorial/elan-lake.md

@@ -1,23 +1,49 @@
-# elan 及 Lake 用法示例
+# Lean 工具链使用指南
+
+[上篇](../install.md)安装 Lean4 提到了 Lean 项目开发的三件套：版本管理器 [elan](https://github.com/leanprover/elan) + 包管理器和构建工具 [lake](https://github.com/leanprover/lake) + 语言本身的核心组件 [lean](https://github.com/leanprover/lean4)。下边分别介绍这三个工具的基本用法。
+
+> 这类设计与其他编程语言类似，如 Rust（rustup + cargo + rustc）或 Node.js（nvm + npm + node）。
 
 ## elan 常用功能
 
-[elan](https://github.com/leanprover/elan) 是 Lean 环境版本管理器，用于安装、管理和切换不同版本的 Lean。
+[elan](https://github.com/leanprover/elan) 是 Lean 版本管理器，用于安装、管理和切换不同版本的 Lean。
+
+版本管理：
 
 ```bash
 elan --version   # 输出版本号来测试安装是否成功
 elan self update # 更新 elan
 elan show        # 显示已安装的 Lean 版本
 
-# 切换默认的 Lean 版本，例如 leanprover/lean4:v4.11.0-rc1 
-# stable 是最新稳定版本，所有版本可见 https://github.com/leanprover/lean4/releases
+# 下载指定 Lean 版本，所有版本可见 https://github.com/leanprover/lean4/releases
+elan install leanprover/lean4:v4.10.0
+
+# 下载最新稳定版本 stable
 elan default leanprover/lean4:stable 
 
-# 也可设置，只在当前目录下使用的 Lean 版本
+# 切换默认的 Lean 版本
+# 切换到 leanprover/lean4:v4.11.0-rc1 
+elan default leanprover/lean4:v4.11.0-rc1 
+
+# 设置在当前目录下使用的 Lean 版本
 elan override set leanprover/lean4:stable
+# info: info: override toolchain for 'xxx' set to 'leanprover/lean4:stable'
+```
+
+指定版本运行 `lake` 或 `lean` 命令：
+
+```bash
+lake --version # 使用 elan 默认版本
+# 使用指定版本
+elan run leanprover/lean4:v4.10.0 lake --version
+elan run leanprover/lean4:v4.10.0 lean --version
+# 创建指定版本的项目
+elan run leanprover/lean4:v4.10.0 lake new package
 ```
 
-elan 在 Windows 下的管理目录为 `%USERPROFILE%\.elan\bin`，在 Linux 下的管理目录为 `$HOME/.elan`，内容形如
+elan 配置记录可以在 `~/.elan/settings.toml` 查看。
+
+具体地，Windows 下的 elan 管理目录为 `%USERPROFILE%\.elan\bin`，Linux/Mac 下的管理目录为 `$HOME/.elan`，内容形如
 
 ```bash
 ❯ tree .elan -L 2
@@ -45,12 +71,12 @@ elan 在 Windows 下的管理目录为 `%USERPROFILE%\.elan\bin`，在 Linux 下
 - `settings.toml` 是 elan 的配置文件。
 - `bin` 存放常用的二进制文件，比如 `lake`。
 
-## 通过 Lake 创建 Lean 项目
-
-对创建 Lean 项目的详细介绍参考[这个教程](https://www.leanprover.cn/fp-lean-zh/hello-world/starting-a-project.html)。此处演示最基本的用法。
+## Lake 基本用法
 
 [lake](https://github.com/leanprover/lake) 全称 Lean Make，是 Lean 4 的包管理器，用于创建 Lean 项目，构建 Lean 包和编译 Lean 可执行文件。
 
+本节介绍 `lake` 的基本用法，[Lean 函数式编程](https://www.leanprover.cn/fp-lean-zh/hello-world/starting-a-project.html)也提供了创建 Lean 项目的例子，而更全面的参数介绍可参考 [lake 文档](../references/lake-doc.md)。
+
 在终端中运行（`your_project_name` 替换为你自己起的名字）
 
 ```bash
@@ -73,7 +99,8 @@ your_project_name
 └── ...
 ```
 
-其中 `lakefile.lean` 是当前项目的配置文件，`lean-toolchain` 是当前项目使用的 Lean 版本。其他文件的功能以及更多细节请参考[这个教程](https://www.leanprover.cn/fp-lean-zh/hello-world/starting-a-project.html)。
+
+其中 `lakefile.lean` 是当前项目的配置文件，`lean-toolchain` 是当前项目使用的 Lean 版本。
 
 初次让 Lean Server 运行该项目时会添加
 
@@ -152,4 +179,47 @@ lake update
 lake run <script>
 ```
 
-关于 Lake 的更多用法可参考 [lake 文档](../references/lake-doc.md)。
+## lean
+
+[lean](https://github.com/leanprover/lean4)：语言本身的核心组件，通常不需要直接与 `lean` 交互。
+
+这里介绍常见的两个操作：运行 Lean 脚本，以及验证 Lean 代码。
+
+执行 Lean 脚本，入口为 `main` 函数：
+
+```lean
+-- hello.lean
+def main : IO Unit := IO.println s!"Version: {Lean.versionString}"
+```
+
+在终端中运行：
+
+```bash
+elan default leanprover/lean4:v4.11.0-rc1
+lean --run hello.lean
+# Version: 4.11.0-rc1
+elan run leanprover/lean4:v4.10.0 lean --run hello.lean
+# Version: 4.10.0
+```
+
+验证 Lean 代码：
+
+```lean
+-- proof.lean
+theorem my_first_theorem : 1 + 1 = 2 := by
+  simp
+
+theorem my_false_theorem : 1 + 1 = 1 := by
+  simp
+
+theorem my_syntax_error_themore 1 + 1 = 2 := by
+  simp
+```
+
+在终端中运行：`lean proof.lean`，返回错误信息：
+
+```bash
+hello.lean:5:40: error: unsolved goals
+⊢ False
+hello.lean:8:31: error: unexpected token; expected ':'
+```

mkdocs.yml

@@ -70,7 +70,7 @@ nav:
   - 主页: 
     - Lean-zh: index.md
     - 安装指南: install.md
-    - 版本管理与包管理: tutorial/elan-lake.md
+    - Lean4 工具链: tutorial/elan-lake.md
     - Lake 包管理: references/lake-doc.md   
   - 交互工具:
     - LeanDojo 教程: tutorial/lean-dojo.md