https://subfish-zhou.github.io/theorem_proving_in_lean4_zh_CN/setup.html
https://blog.csdn.net/qq_59376271/article/details/134941312
问题
3.1：windows系统可能报错识别不了-L选项：
执行Remove-item alias:curl命令删除别名可解决 lean4 Infoview不见了
使用快捷键 Ctrl+Shift+P 打开命令面板，然后输入 Lean: Open Infoview。重启You might need to open 'c:makerlean4' as a workspace in your editor：
打开命令面板：
使用快捷键 Ctrl+Shift+P 打开命令面板。
添加文件夹到工作区：
在命令面板中输入 Add Folder to Workspace，然后选择 Workspaces: Add Folder to Workspace...。
在弹出的文件选择对话框中，导航到你想添加的文件夹（例如 c:\maker\lean4），然后点击“选择文件夹”或“打开”按钮。
保存工作区：
添加文件夹后，可以选择保存工作区设置。点击文件菜单（File），选择“保存工作区为...”（Save Workspace As...），然后选择一个位置和文件名保存工作区文件。
==== 在菜单file -- add folder to 。。
Imports are out of date and must be rebuilt; use the "Restart File" command in your editor.
重启文件：
打开 VSCode 的命令面板（使用快捷键 Ctrl+Shift+P）。
输入 Lean: Restart File 并选择它。这将重启当前文件并重新编译导入。
更新依赖：
在终端中导航到你的 Lean 项目目录。
运行 lake update 命令来更新项目的依赖。
sh
Copy
lake update
重启 Lean 服务器：
打开 VSCode 的命令面板（使用快捷键 Ctrl+Shift+P）。
输入 Lean: Restart Lean Server 并选择它。这将重启 Lean 服务器并重新加载所有文件。
清理项目：
有时，清理项目并重新编译可以解决问题。在终端中运行以下命令：
sh
Copy
lake clean
lake build
lean4game:
https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md
https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md
安装npm，node
下载game
git clone https://github.com/hhu-adam/GameSkeleton.git
or: git clone git@github.com:hhu-adam/GameSkeleton.git
cd GameSkeleton
lake update -R
lake build
下载lean4game：
cd ..
git clone https://github.com/leanprover-community/lean4game.git
or: git clone git@github.com:leanprover-community/lean4game.git
cd lean4game
npm install *不要用代理
npm start
This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace with the folder name of your local game.GameSkeleton
问题：
time.cpp无法编译c++
通过 vs安装工具安装 cl，通过mingw64安装c++ g++ 。路径都需要加入系统变量path