Merge remote-tracking branch 'subfish/main' into mkdoc

docs/tutorial/install.md

@@ -1,6 +1,50 @@
-## LEAN4 安装教程 
+# LEAN 4 安装和配置教程 
 
-Windows 可以参考 [子鱼的博客](https://subfish-zhou.github.io/theorem_proving_in_lean4_zh_CN/setup.html)，Mac 系统按[官网教程](https://leanprover-community.github.io/install/macos_details.html)使用 homebrew 来快速配置。当前教程针对 Ubuntu 系统，其他系统待实测后更新。
+Lean 4 工作环境由以下几部分组成：
+
+1. [elan](https://github.com/leanprover/elan)：Lean 环境版本管理器。它的功能类似于 Rust 的 `rustup` 或 Node.js 的 `nvm`，用于安装、管理和切换不同版本的 Lean。
+2. [lake](https://github.com/leanprover/lake)：Lean 4 的包管理器，全称 Lean Make，已合并到 Lean 4 仓库，作为源码的一部分。它用于创建 Lean 项目，构建 Lean 包，配置 Mathlib 和编译 Lean 可执行文件。
+3. （非必须）[Mathlib](https://leanprover-community.github.io/mathlib4_docs/)：Lean 的数学库。
+
+为了使用 Lean，你需要先安装 [VS Code](https://code.visualstudio.com/) 和 Git，然后安装 elan，elan 会自动帮你安装 Lean 4 stable 以及 lake 包管理器，接下来就可以使用 lake 创建自己的 Lean 项目。
+
+## Windows 安装 elan
+
+你可以在这里下载安装 [VS Code](https://code.visualstudio.com/download) 和 [Git](https://gitforwindows.org/)。
+
+安装 VS Code 后，需要安装 lean4 扩展（extension）。如果你的网络环境顺畅，可以在 lean4 扩展的欢迎页选择 Get Start 来完成安装，或者创建空的 Lean 文件时扩展会弹出提示提醒你安装 elan 和 Lean 4。
+此外你还可以在 cmd 或 powershell 中运行命令
+
+```
+curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
+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)安装。下面演示在网络环境不理想的条件下的安装。
+
+打开 cmd 或 Powershell，运行
+```
+curl -O --location https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/elan/releases/download/v3.1.1/elan-x86_64-pc-windows-msvc.zip
+unzip -o elan-x86_64-pc-windows-msvc.zip
+.\elan-init.exe
+```
+会在终端中开始安装程序。单击回车在默认位置 `~\.elan` 安装。
+
+安装完成后可以删除刚刚下载的临时文件：
+
+```
+del elan-init.exe
+del elan-x86_64-pc-windows-msvc.zip
+```
+
+添加 elan 的安装地址到 PATH 环境变量（如果是默认安装，那么是 `%USERPROFILE%\.elan\bin`）。
+
+重启终端输入 `elan --version`，如果能正常输出版本号，那么你已经装好了 elan 和 Lean 4 stable 版本。
+
+## Linux 安装 elan
+
+以下内容在 Ubuntu 22.04 系统上测试通过。
 
 如果没有网络问题，用一行命令安装：
 
@@ -10,18 +54,16 @@ wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/s
 
 该命令执行了一个脚本：[install_debian.sh](https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh)，主要安装了 VsCode，Lean 插件，以及 elan。
 
-如果访问 GitHub 存在问题，可以在安装 VsCode 和 Lean 插件后，手动安装 elan。
-
-### 安装 elan
-
-elan 是一个用于管理 Lean 环境的工具。它的功能类似于 Rust 的 `rustup` 或 Node.js 的 `nvm`，用于安装、管理和切换不同版本的 Lean。
+如果访问 GitHub 存在问题，可以在安装 VS Code 和 Lean 插件后，手动安装 elan。
 
 在 GitHub [release 页面](https://github.com/leanprover/elan/releases)根据系统版本下载新版 elan，比如 `linux-x86_64` 系统的 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
@@ -61,7 +103,34 @@ stable (default)
 Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)
 ```
 
-elan 的管理目录为 `$HOME/.elan`，内容形如
+## Mac 安装 elan
+
+Mac 系统类似，用脚本一键安装：
+
+```bash
+/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile
+```
+
+或者在 GitHub [release 页面](https://github.com/leanprover/elan/releases) 或 [上交镜像源](https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/mirror_clone_list.html) 手动下载运行安装程序。
+
+不鼓励使用 homebrew 提供的 elan-init 包，因为用户经常发现这落后于官方版本的更新。
+
+## elan 常用功能
+
+```
+elan --version   # 输出版本号来测试安装是否成功
+elan self update # 更新 elan
+elan show        # 显示已安装的 Lean 版本
+
+# 切换默认的 Lean 版本，例如 leanprover/lean4:v4.11.0-rc1 
+# stable 是最新稳定版本，所有版本可见 https://github.com/leanprover/lean4/releases
+elan default leanprover/lean4:stable 
+
+# 也可设置，只在当前目录下使用的 Lean 版本
+elan override set leanprover/lean4:stable
+```
+
+elan 在 Windows 下的管理目录为 `%USERPROFILE%\.elan\bin`，在Linux下的管理目录为 `$HOME/.elan`，内容形如
 
 ```bash
 ❯ tree .elan -L 2
@@ -83,24 +152,101 @@ elan 的管理目录为 `$HOME/.elan`，内容形如
     └── stable
 ```
 
-下载的 LEAN 版本在 `toolchains` 目录下，`settings.toml` 是 elan 的配置文件。
+下载的 Lean 版本在 `toolchains` 目录下，`settings.toml` 是 elan 的配置文件。
 
 elan 的二进制文件中，`lake` 经常会用到。
 
-### Lake 管理器
+## 通过 Lake 创建 Lean 项目
+
+对创建 Lean 项目的详细介绍参考[这个教程](https://www.leanprover.cn/fp-lean-zh/hello-world/starting-a-project.html)。此处演示最基本的用法。
 
-[lake](https://github.com/leanprover/lake) 全称 Lean Make，是 LEAN4 的包管理器，已合并到 LEAN4 仓库，作为源码的一部分。
+在终端中运行（`your_project_name` 替换为你自己起的名字）
 
-下边用一个简单的例子演示 `lake` 的基本用法。
+```
+lake new your_project_name
+
+# 或者手动创建一个新文件夹并在原地建立项目
+mkdir your_folder_name && cd your_folder_name && lake init your_project_name
+```
 
-创建项目，目录为 `hello`
+以创建一个名为 `your_project_name` 的空白新项目。这个项目的内容形如
+
+```
+your_project_name
+├── YourProjectName
+│   └── Basic.lean
+├── lakefile.lean
+├── lean-toolchain
+├── Main.lean
+├── YourProjectName.lean
+└── ...
+```
+
+其中 `lakefile.lean` 是当前项目的配置文件，`lean-toolchain` 是当前项目使用的 Lean 版本。其他文件的功能以及更多细节请参考[这个教程](https://www.leanprover.cn/fp-lean-zh/hello-world/starting-a-project.html)。
+
+初次让 Lean Server 运行该项目时会添加
+
+```
+├── .lake
+   ├── lakefile.olean.trace
+   └── ...
+├── lake-manifest.json
+```
+
+如果你想在这个现有的工程中引用 Mathlib4，你需要在 `lakefile.lean` 文件尾中加入
+
+```
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4"
+```
+
+保存文件后 VS code 会提示 "Restart Lean"，点不点都没关系。
+
+下面要下载 Mathlib，注意让终端路径在你的项目文件夹下。如果你的网络情况好，那么在终端中运行
+```
+curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
+lake update
+```
+
+保存运行缓存会让每次编译节省一两个小时，但它当然也不是必须的：
+
+```
+lake exe cache get
+```
+
+否则（会相当艰难），参考[这个解决方案](https://zhuanlan.zhihu.com/p/680690436)。（不保证该参考方案的可靠性）
+
+如果你看到终端中显示了类似如下的提示：
+
+```
+Decompressing 1234 file(s)
+unpacked in 12345 ms
+```
+
+同时你的项目文件夹中出现了 `.lake\packages` 文件夹，那么证明你安装 Mathlib 成功了，此时 "Restart Lean" 即可使用。**注意：你要在项目所在的目录中运行 VS code，才能让 Lean 使用Mathlib。**
+
+这里提供一个实例来测试你的安装：
+```
+import Mathlib.Data.Real.Basic
+example (a b : ℝ) : a * b = b * a := by
+  rw [mul_comm a b]
+```
+如果你的 Lean infoview 没有任何报错，并且光标放在文件最后一行时会提示 "No goals"，证明你的 Mathlib 已经正确安装了。
+
+如果你想更新 Mathlib，在终端中运行
+
+```
+curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
+lake update
+lake exe cache get
+```
+
+*关于 Mathlib 的更多内容请参考 [Mathlib Wiki](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency)*
+
+lake 的其他常用功能：
 
 ```bash
-# 创建包
-lake new hello
-## 或者
-mkdir hello && cd hello && lake init hello
-# 构建包
+# 构建项目可执行文件
 lake build
 # 运行
 lake exec hello # Hello, world!
@@ -110,4 +256,6 @@ lake clean
 lake update
 # 运行 lakefile.lean 的脚本
 lake run <script>
-```
+```
+
+关于 Lake 的更多用法可参考[ lake 文档](references/lake-doc.md)。