17370845950

本工具使用前请先准备以下环境：

• 操作系统为 Windows 10 或更高版本
• 确保 C 盘有至少 5GB 的可用存储空间
• 已安装 git-for-windows 客户端
• 检查路径 C:\Users\你的用户名\.elan 是否存在。若存在，请将其删除或备份，因安装过程会覆盖该目录

【使用方法】

1. 下载本工具

2. 解压下载的压缩包，推荐使用 WinRAR 或 7-Zip 进行解压。解压后运行 FIRC.exe

温馨提示：部分杀毒软件可能会误报此程序，建议将其添加至白名单或临时关闭杀毒软件。如对软件安全性存疑，请立即删除并停止使用。启动后可见，当前集成的 Lean4 版本为 4.19.0-rc2，该版本稳定性较好，故作为默认安装版本。截至发布时，最新版本为 4.20.0-rc5，后续将逐步支持新版本。

3. 输入邀请码，点击“验证”，验证通过后点击“开始安装”即可自动完成安装流程

4. 安装完成后，打开 VSCode，安装 Lean4 插件，并创建一个新的文件夹，例如：

testcode

在该文件夹中创建文件：

test.lean

在 test.lean 中输入以下内容：

#eval Lean.versionString
#eval 1+1

再创建一个名为 lean-toolchain 的文件（无后缀名），内容为：

leanprover/lean4:v4.19.0-rc2

注意：此处版本号必须与你实际安装的 Lean4 版本一致

完成后，右侧将显示代码执行结果