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

【问题标题】：Coq module "Cannot find a physical path bound to logical path matching suffix <> and prefix" and "not found in the loadpath"Coq 模块“找不到绑定到逻辑路径匹配后缀 <> 和前缀的物理路径”和“在加载路径中找不到”
【发布时间】：2019-08-25 18:56:40
【问题描述】：

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

我使用的是 coq v8.8.1，通过 opam 安装。

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

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

COQDEP VFILES

*** 警告：在 Auto.v 文件中，需要库 LF.Maps，但在加载路径中未找到！

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

【问题讨论】：

软件基础自带了自己的makefile。尝试解压 tarball 并在顶级目录中运行 make，而不使用 coqide 的 makefile。
您还可以检查是否生成了 *.vo 文件。这些是编译后的 *.v 文件，因此它们的存在表明源文件是否编译成功。

标签： coq coqide

【解决方案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.

【讨论】：