sublimetext3 - 为什么 Coq 不能识别已编译的库？

Question

我试图让 Coq 在 MacOS 上作为 Sublime Text 3 的插件工作。除了需要导入语句的代码外，我的一切都正常工作。

完全相同的代码在 CoqIDE（运行 Coqc 8.9 版）中运行时完美运行，但是当我尝试从 Coqc 版本 8.8（自制安装）运行时，当我到达我的声明时：

From LF Require Export Basics.

它抛出错误：

Cannot find a physical path bound to logical path matching suffix <> and prefix LF.

当我删除时，From LF我得到：

Basics.vo contains library LF.Basics and not library Basics

这表明（至少对我而言）这些库确实可以正确编译和制作，而其他一些地方是错误的。

以下是我运行的命令：

coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile -B

我的 _CoqProject 看起来像这样：

-R . LF
Basics.v
Induction.v

有人对此有任何想法或经验吗？

标签： sublimetext3coq