coqIDE未正确连接项目中的文件，因此未进行编译

Question

我刚开始使用coq/coqIDE，我也不精通计算机，所以我不知道哪里出了问题，也不知道该怎么称呼这个问题。我试着翻阅“软件基础”这本书，但是coqIDE不能正常工作。我使用的是最新的windows 10和coqIDE 8.10.2

第一个问题是，当我在Basics.v中打开compile -> compile buffer选项卡时，coqIDE没有创建.vo文件或.glob。其他按钮也都不起作用。以管理员身份运行coqIDE也无法使其正常工作，但我发现可以通过手动将Basics.v拖动到coqc应用程序文件中来解决此问题。

在第一课中，我对coq的工作没有任何问题，但是在下一课中，我们打算将定义从Basics.v导入到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“。

我也可以通过编写“要求导出基础知识”来绕过这个错误。直到我实际尝试调用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无论如何都没有改变任何东西。

我想我什么都没忘，提前谢谢你。

Answer 1

而不是选择Compile > Compile buffer，而是尝试Compile > Make (当浏览逻辑基础中的任何一个本地文件时)-我认为这就是其他人所说的“在顶层点击make”的意思。但首先，您可能想要删除您在Induction.v中添加的变通方法，并在Basics.v中保存一些微不足道的更改，例如在某个地方添加/删除换行符，以便说服make重新编译它。