coq - Coq 模块“找不到绑定到逻辑路径匹配后缀 <> 和前缀的物理路径”和“在加载路径中找不到”

Question

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

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

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

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

COQDEP VFILES

*** 警告：在文件 Auto.v 中，库 LF.Maps 是必需的，但在加载路径中没有找到！

我的目标是编译和运行该Induction.v文件。在出现这些错误之前，我使用 coqide 的选项首先“make makefile”然后“make”。

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.