辅酶模块"Cannot find a physical path bound to logical path matching suffix <> and prefix"和"not fou

Question

我正在阅读逻辑基础，并下载了它附带的coq脚本。

我正在使用 coq v8.8.1，通过 opam 安装。

我在标题中遇到了两个错误，我不确定应该如何调试它们。

第二个错误的完整错误消息是

COQDEP VFILES

警告：在文件 Auto.v 中，库 LF。地图是必需的，在装载路径中找不到！

我的目标是编译并运行Induction.v文件。在出现这些错误之前，我使用 coqide 的选项首先"制作 makefile"，然后"制作"。

Answer 1

这对我有用：

在与 Basics.v 相同的目录中运行它

coqc -Q . LF Basics.v

然后。。。

• 我能够编译Induction.v：

  coqc -Q . LF Induction.v
  

• 我能够做到这一点：

  coqtop -Q . LF
  {* now that coqtop is open... *}
  From LF Require Export Basics.