Lean 4 开发环境从零搭起来新手四步走完到第一个可运行项目【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4Lean 4 是一门兼具函数式编程与定理证明能力的语言。本文面向零基础新手跟着读完你会装好工具链、建出第一个项目并在 VSCode 中获得实时的证明反馈。先记住目标环境搭好的四个判断信号在动手之前先记住下面四组信号全部出现就说明环境就绪终端里运行lean --version能看到版本号而不是提示命令不存在。lake build执行完毕且没有报错项目目录中出现.lake目录。VSCode 打开项目后右侧 Infoview 面板出现并显示光标所在行号。运行程序后终端打印出Hello, world!。下文就是围绕这四条逐一落地的过程。动手之前先分清使用 Lean和从源码编译 Lean绝大多数新手属于第一类——写 Lean 代码。这种情况只需要安装 elan 工具链管理器它会自动下载匹配的编译器版本不需要任何额外依赖。只有当你想修改或重新编译 Lean 4 编译器本身时才需要 C 编译器、CMake、GMP、LibUV、OpenSSL 等构建依赖。Ubuntu 上一条命令即可备齐sudo apt-get install git libgmp-dev libuv1-dev libssl-dev cmake ccache clang pkgconf安装过程无报错、命令正常返回提示符说明依赖到位。源码仓库地址是 https://gitcode.com/GitHub_Trending/le/lean4 克隆后用 CMake 配置、make 并行编译仓库文档里给出了完整的构建参数与排错说明。 最短路径一条命令装 elan三条命令建项目elan 是 Lean 4 版本管理的统一入口不同项目可以依赖不同的编译器版本elan 负责自动匹配和下载。先执行官方安装脚本curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh脚本下载并执行到结束、全程没有错误输出即安装成功。接着创建第一个项目lake new hello_lean cd hello_lean lake build终端出现Build completed successfully.并且项目目录下多出一个.lake文件夹说明项目已建立并完成首次构建。验证闭环三个动作确认环境真的能跑装完不等于能用按顺序做三个动作才算闭环。动作一确认编译器版本可读取lean --version输出一行形如Lean (version 4.x, ..., Release)的文字说明 elan 与编译器已正确联动。动作二把程序跑起来lake exe hello_lean终端打印Hello, world!编译到运行的链路就通了。动作三故意制造一个错误在Main.lean任意一行加入1 a 5并保存。如果 VSCode 在该行标出红色波浪线、Infoview 同步显示类型错误信息说明实时类型检查已生效。验证完删掉这一行即可。最快接入 VSCode 的方法让安装向导替你装在扩展市场搜索 Lean 4 并安装扩展即可获得语法高亮、自动补全与错误标注这是接入成本最低的方式。首次打开项目时扩展可能自动弹出安装向导如果没有从扩展菜单的 Docs 项选择 Show Setup Guide 手动打开。向导的第一步就是安装 elan点击安装按钮后脚本会自动下载并执行。每一步完成后条目会打上对勾最后一步 Questions and Troubleshooting 则汇总了常见问题的处理文档。接入成功的标志编辑器右上角出现 Infoview 面板形如Foo.lean:2:28的位置信息和 No info found. 占位文字说明 Lean 语言服务器已经启动并跟踪当前文件。WSL 或远程开发怎么连如果代码放在 WSL 或远程机器上再装一个 VSCode 的 Remote Development 扩展包以 WSL 模式打开项目文件读写与终端都会运行在 Linux 内部。看到左侧文件树显示 WSL 中的项目、终端出现(base) userhost:~$提示符、右侧 Infoview 能正常显示当前行反馈连接即正常。日常使用边写代码边看证明反馈接入之后日常开发主要靠三个高频操作。看证明状态光标停在证明步骤末尾Infoview 会显示该位置当前的目标这是 Lean 4 交互式证明的核心用法。查常量信息把光标放在某个名称上使用 Show Term 命令即可查看完整类型与定义。插入交互组件在代码里写一行#widget命令扩展会在编辑器内渲染出可交互内容例如魔方演示#widget rubiks {seq : [U, L, R, L, R]}#widget行出现后 Infoview 显示加载条渲染完成即可直接在编辑器里转动魔方这就是 Lean 4 的 widget 能力。 版本冲突和常见卡点怎么处理项目与系统的 Lean 版本不一致这不是故障而是设计如此。elan 会读取项目内的lean-toolchain文件自动使用必要时下载项目指定的版本。若需手动调整全局默认版本elan toolchain install stable elan default stable随后运行lean --version输出的版本号变为新版即切换成功。提示lean命令不存在elan 把路径写进了新终端的环境变量。关闭并重开终端或执行source ~/.bashrc后重新验证。从源码编译时定位不到错误给 make 追加VERBOSE1参数它会逐条打印实际执行的命令便于锁定失败的那一步。延伸资源文档、示例与测试用例环境跑通后可以用仓库里三个目录继续练习doc/官方文档覆盖安装、开发指南与各语言特性章节。doc/examples/可直接编译运行的示例程序适合照着写自己的证明。tests/项目的测试用例集合是熟悉报错信息与高级语法的好素材。下一步建议在 hello_lean 项目里用by decide证明2 2 4再换成一个需要omega战术的命题。卡住时先翻安装向导里的 Questions and Troubleshooting绝大多数卡点都写在里面。【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考