3

我最近从 Windows 切换到 Mac，现在 CoqIde 的行为不像我以前那样。我正在使用 Coq 8.9.1，我不记得我曾经使用的版本，但它最后一次更新是 2018 年秋季。

在我的旧机器上，我可以编译一个文件（例如 file1.v 以获取 file1.vo 和 file1.glob），然后将其导入或导出到同一目录中的另一个文件（例如 writing Require Export file1.），而无需更改加载路径。现在我必须将当前目录显式添加到加载路径，否则会出现“无法找到库...”错误。

这是预期的行为吗？我已经离开 Coq 一段时间了，但我很确定我以前不必这样做。将当前目录添加到加载路径不在我的任何旧工作中。有没有办法让当前目录始终位于加载路径中？

我阅读了这个问题和答案，但那里的建议看起来都归结为将我正在使用的任何目录添加到加载路径（在我正在处理的文件中或其他地方）。

更新：

我能够在文件所在位置从终端打开解决方案（导致当前文件的路径位于 LoadPath 中），但这比我习惯使用 Windows 时更令人头疼。

我不得不在 ~/bin/coqide 中编写一个小 Bash 脚本，它只调用/Applications/CoqIDE_8.8.0/Contents/MacOS/coqide. 在我的主用户的二进制文件目录中添加符号链接找不到它期望与调用符号链接的位置相关的文件。

我无法使用 _CoqProject 文件在 CoqIde 中获得第二个解决方案，最终看到了一些奇怪的行为。使用 coqc 从终端编译有效。

我已将此添加到 Coq GitHub 问题跟踪器（请参阅此处和此处）。

4

1 回答 1

4

当您使用 CoqIDE 打开文件时，它不会找到您依赖的其他文件，相对于您打开的文件的位置，但相对于您打开 CoqIDE 的位置（另请参阅https://github.com/coq/ coq/issues/5124）。

因此，一种可能的解决方案是我在上面的评论中提到的解决方案（从文件所在的控制台打开 CoqIDE）。但幸运的是，当您正在处理一个包含多个文件的项目时，我会推荐另一种解决方案，它的优点是允许您随心所欲地打开 CoqIDE：它是使用_CoqProject文件。

因此，只需在您的 Coq 文件所在的任何位置创建一个_CoqProject文件，只需使用以下行：

-R . MyProjectNamespace

然后一切都应该神奇地工作（前提是您重新编译所有文件）。

于 2019-05-25T00:06:30.803 回答