add meta programming example

docs/contribute/guide.md

@@ -0,0 +1 @@
+

docs/contribute/project.md

@@ -0,0 +1 @@
+# 项目教程

docs/contribute/translation.md

@@ -0,0 +1,3 @@
+# 文档翻译
+
+TODO

docs/index.md

@@ -59,7 +59,8 @@ Lean-zh 提供了一个学习与实践的平台，如果你对 Lean 感兴趣，
 **进行中**
 
 * [Lean 形式化数学(Mathematics in Lean)](https://www.leanprover.cn/math-in-lean-zh/)
-* Lean 交互工具和实用项目的教程介绍
+* Lean 交互工具的使用教程
+* Lean 项目的实践教程
 
 **计划进行**
 

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。
 
@@ -30,7 +34,7 @@ wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/s
 
 ```bash
 # 如果网络不行就本地下载再上传
-curl -L 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/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
 tar xf elan.tar.gz
 ```
 
@@ -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/projects/blueprints.md

@@ -0,0 +1,3 @@
+# Lean Bleu Print
+
+项目地址：https://github.com/PatrickMassot/leanblueprint

docs/tutorial/jixia.md → docs/projects/jixia.md

@@ -3,6 +3,7 @@
 jixia 是一个为 Lean 4 设计的新静态分析工具，其旨在支持构建具有 Lean 感知能力的集成开发环境（IDE），并为机器学习提取有用的数据。该项目是北京大学数学科学学院（BICMR）人工智能与数学程序项目的一部分。"jixia" 这个名字来源于历史上的“稷下学宫”，位于现在的山东淄博。
 
 **工具特点**：
+
 - **非侵入性**：无需对目标文件进行任何修改，这有利于提高缓存利用率，特别是在 mathlib4 上。
 - 单文件分析。
 - 源码级信息：包含每个定义函数的源码范围、参数和返回类型等信息。