在 Coq 中指定导出文件的路径？答案

【问题标题】：Specifying Paths for exporting files in Coq?在 Coq 中指定导出文件的路径？
【发布时间】：2020-06-12 18:19:06
【问题描述】：

我正在编写自己的第一个 Coq 文件，但在导出另一个用户定义的文件（由《软件基础》一书定义）时遇到问题。

问题是我当前的 Coq 文件的路径为 Coq/NWA.v，而我要导入的文件的路径为 Coq/SoftwareFoundations/lf/Rel.v。我尝试了以下语法：

From Coq/SoftwareFoundations/lf Require Import Rel.v

From Coq.SoftwareFoundations.lf Require Import Rel.v

From ./../SoftwareFoundations/lf Require Import Rel.v

所有这些都给出了语法错误。如何导入 Rel.v 文件？

【问题讨论】：

阅读softwarefoundations.cis.upenn.edu/lf-current/Induction.html的第一部分可能相关
我按照以下步骤操作： (1) 我制作了一个内容为 '-Q ./../SoftwareFoundations/lf/LF' 的 _CoqProject 文件。 (2) 我在文件 NWA.v 中添加了 From 'LF Require Export Rel' 行。 (3) 从命令行我运行 cmd: "coq_makefile -f _CoqProject *.v -o Makefile" (4) 我重新编译文件 Rel.v 我仍然遇到语法错误。

标签： coq

【解决方案1】：

tl;dr: 正确的语法是

From LF Require Import Rel.

要管理 Coq 文件，需要注意两种路径：

-Q my/path/to/lf LF 选项（最终需要传递给 coqc）所做的是将逻辑路径 (LF) 映射到物理路径 (my/path/to/lf)。

在 Coq 文件中，Require Import 命令（包括From _ Require Import _）适用于逻辑路径。经验法则是，.v 文件的内容只涉及逻辑路径，尽管有几个例外（例如，Add LoadPath 和提取）。

Logical Foundations 卷是使用逻辑路径LF.ModuleName 构建的，这就是您需要在Coq/NWA.v 中使用以导入Rel：

From LF Require Import Rel.

(* or *)

Require Import LF.Rel.

【讨论】：

如何将 -Q my/path/to/lf LF 选项传递给 coqc ？
为了将 -Q my/path/to/lf LF 选项传递给 coqc，我在终端中运行了以下命令： coq_makefile -f _CoqProject *.v -o Makefile 但出现以下错误：警告：..\SoftwareFoundations\lf\（在 -R 或 -Q 中使用）不是当前目录的子目录警告：没有公共逻辑根警告：在这种情况下必须定义 INSTALLDEFAULTROOT 警告：安装文档目标正在执行安装文件警告：在 orphan_LF_Top
如果您的物理路径包含 ..，则会出现这些警告。可以忽略这些警告。