用于LEAN定理证明器的Windows上的Visual studio路径配置

Question

我正在尝试设置我的VS代码环境，以便使用LEAN自动定理证明器。

我在这里按照教程设置了一个新项目，并有一个名为test.lean的文件，如下所示：

import data.real.basic

我得到以下错误：

invalid import: data.real.basic
could not resolve import: data.real.basic

错误消息建议我调用lean --path，我照做了，并获得了：

PS C:Usersuserlean_test2> lean --path
{
  "is_user_leanpkg_path": false,
  "leanpkg_path_file": "C:\Users\user\lean_test2\leanpkg.path",
  "path": [
    "C:\Users\user\.elan\toolchains\leanprover-community--lean---3.35.1\bin\..\library",
    "C:\Users\user\.elan\toolchains\leanprover-community--lean---3.35.1\bin\..\lib\lean\library",
    "C:\Users\user\lean_test2\_target/deps/mathlib/src",
    "C:\Users\user\lean_test2\./src"
  ]
}

我注意到路径使用了/和\的混合，但我认为这不会成为问题。我检查了路径列表中的第三个条目，发现以下文件

C:Usersuserlean_test2_targetdepsmathlibsrcdatarealbasic.lean

确实存在。那么，可能出了什么问题？

Answer 1

我不知道问题出在哪里，但通常应该使用"打开文件夹"；功能打开包含mathlib的文件夹或打开包含依赖于mathlib项目的文件夹。还有一个leanproject global-install命令，您可以使用它全局安装mathlib，而无需在VScode中打开文件夹，但我自己从未使用过这个命令。