我是使用 coq/coqIDE 的新手，而且我也不精通计算机，所以我不知道出了什么问题，也不知道该说什么。我试图通过软件基础这本书，但 coqIDE 工作不正常。我正在使用最新的 windows 10 和 coqIDE 8.10.2
第一个问题是当我转到 中的选项卡compile -> compile buffer时Basics.v，coqIDE 不会创建 .vo 文件或 .glob。其他按钮也没有工作。以管理员身份运行 coqIDE 也无法正常工作，但我发现我可以通过手动将 Basics.v 拖到 coqc 应用程序文件中来解决这个问题。
在第一课中我对 coq 的工作没有任何问题，但是在下一课中，当我运行他们所说的时，我们打算将定义从Basics.vinto导入Induction.v
From LF Require Export Basics.
The file C:\Users\...\Coq Files\Tutorial\lf\Basics.vo contains library Basics and not library LF.Basics即使 _CoqProject 文件应包含“-Q . LF”，我也会收到错误消息。
我也可以通过编写“Require Export Basics”来解决这个错误。正确加载，直到我真正尝试从 Basics 调用定义
跑步
Require Export Basics.
Example example: evenb 2 = true.
工作直到我到达evenb，然后给出错误
The reference evenb was not found in the current environment.，即使它在Basics.v
如果我得到更多的肛门并尝试
Add LoadPath "C:\Users\...\Coq Files\Tutorial\lf".
From LF Require Export Basics.
我得到错误
Cannot find a physical path bound to logical path matching suffix <> and prefix LF.
最后，如果我尝试
Add LoadPath "C:\Users\...\Coq Files\Tutorial\lf".
Require Export Basics.
Example example: evenb 2 = true.
正确加载。
所以我想知道我应该如何修复加载路径，以便项目在不将垃圾放入每个文件中的情况下工作，以及如何使编译选项卡工作。
有一些人在谈论“在顶层打 make”，但我不知道那是什么意思。无论如何，我尝试了它并将 Makefile 作为 .bat 运行，即使我已经正确下载了它，所以不应该有任何需要，但 Makefile 并没有改变任何东西。
我不认为我忘记了什么，提前谢谢。