可能是一个coq新手问题,但我找不到现成的解决方案,所以我会在这里询问以供参考。cocq版本是8.5pl2
我试图构建
coqfj。第一次make
尝试失败,在第 37 行出现了一些错误src/FJ/ClassTable.v
。这个问题与那个错误无关。
仔细一看,我ClassTable.v
在 emacs proofgeneral 中打开并按下C-c C-n
,或者运行coqc src/FJ/ClassTable.v
。结果是第 1 行中的错误:
File "./src/FJ/ClassTable.v", line 1, characters 15-23:
Error: Cannot find a physical path bound to logical path matching suffix FJ.
似乎require import FJ.Lists
无法解析导入(尽管 FJ 用作前缀,而不是后缀)。我注意到make
已经创建了一个编译文件src/Lists.vo
,应该由 coqc 获取。
*.vo
如何通过查看文件夹中的or*.v
文件来告诉 coqc 它应该解决这个“后缀” src
?