Coq 模块 "Cannot find a physical path bound to logical path matching suffix <> and prefix"和 "not found in the loadpath"

Question

我正在阅读 logical foundations并下载了它附带的 coq 脚本。

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

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

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

COQDEP VFILES

*** Warning: in file Auto.v, library LF.Maps is required and has not been found in the loadpath!

我的目标是编译并运行 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.