VS Code加载Lean4文件时执行c++失败（错误码2）求助

问题原因 #

Lean4的Lake构建工具不自带C++编译器，它依赖系统已安装的C编译环境来编译底层C代码（比如报错中提到的time.cpp）。你遇到的failed to execute 'c++': no such file or directory错误，本质是系统中没有可用的C++编译工具链。

解决步骤 #

Windows系统下的两种方案 #

• 方案一：安装Visual Studio Build Tools
  1. 下载并运行Visual Studio Installer
  2. 在工作负载列表中勾选「Desktop development with C++」，确保勾选MSVC编译器、Windows SDK等核心组件
  3. 安装完成后，重启VS Code或打开新终端（让环境变量生效）
• 方案二：安装MinGW-w64
  1. 下载MinGW-w64安装包，选择x86_64架构的版本
  2. 将MinGW安装目录下的bin文件夹（例如C:\mingw64\bin）添加到系统环境变量PATH中
  3. 验证：打开终端输入g++ --version，能正常输出版本信息即配置成功

验证修复 #

重启VS Code，再次点击Restart File，Lake即可调用C++编译器完成项目构建。

内容的提问来源于stack exchange，提问作者Răzvan Flavius Panda