编辑“︁Lean项目自动化”︁（章节）

== 核心概念 ==  
Lean项目自动化依赖以下关键组件：  
* '''Lake构建系统'''：Lean的官方构建工具，支持依赖管理、任务定义和跨平台脚本。  
* '''宏（Macros）'''：在编译期生成或转换代码，减少重复劳动。  
* '''自定义属性（Attributes）'''：通过注解触发自动化行为（如自动生成证明）。  
* '''Elaborators'''：控制Lean类型推导过程的元程序。  

=== Lake基础示例 ===  
以下是一个简单的`lakefile.lean`配置，定义自动下载依赖并编译项目：  

<syntaxhighlight lang="lean"> 
-- 声明项目元数据  
require mathlib from git "https://github.com/leanprover-community/mathlib4"  

-- 定义自定义任务  
def greet : Lake.Task := fun args => do  
  IO.println "Automating Lean projects with Lake!"  

-- 将任务注册到Lake  
module_data greet_task := greet  
</syntaxhighlight>  

执行命令：  
<syntaxhighlight lang="bash"> 
lake greet  # 输出: Automating Lean projects with Lake! 
</syntaxhighlight>