coqide - Coq 生成文件“顶部”。字首

Question

我正在使用自动 Coq 8.5 生成文件生成器。这个 makefile 以“Top”作为所有模块的前缀。. 现在假设您通过 make 运行了很多文件，然后想要在 IDE 中更改/调试某些文件。然后令人讨厌的事实是 Coq 抱怨它无法找到已编译的其他文件，因为在 IDE 中它假定名称没有“Top”前缀。我试图调整 makefile 以摆脱这个前缀。但我总是以一些错误信息结束。有人可以告诉我如何删除 make 中的“Top”前缀或告诉 IDE 使用“Top”前缀。

Answer 1

您可以使用以下参数启动 CoqIDE coqide -R . Top。

这将摆脱以下错误Error: The file ..../Logic.vo contains library Top.Logic and not library Logic。

Answer 2

这确实很烦人。为了避免这种烦恼，请始终从_CoqProject行列表选项开始：

-Q . MyProject

注意：您可以放在第一行的选项_CoqProject是调用时列出的选项coqtop -help。