Coq 中同一个库的不同版本

Posted 2023-03-31

【中文标题】Coq 中同一个库的不同版本

【英文标题】：Diffent versions of same library in Coq

【发布时间】：2018-10-28 16:39:50

【问题描述】：

是否可以在 Coq 中安装同一个库的多个版本？如果是，我该如何选择要使用的版本？

我在 Windows 中工作，因此任何使用 OPAM 的解决方案都对我没有帮助。

【问题讨论】：

您是指不同版本的 Coq（8.4、8.5、8.8 等）还是某些开发的不同版本（Coq 读取的.v 文件）？对于后者，只需将它们放在不同的目录中并指定 LoadPath。

我的意思是一组 .v 文件的不同版本。如果我不走运，我还需要更改为旧版本的 Coq，但我希望 Coq 足够向后兼容。当您说“指定加载路径”时，我是否需要在库的每个 .v 文件中执行此操作，还是可以在安装时以某种方式全局完成？这个库非常大，我想避免手动更改 100 多个文件。

【参考方案1】：

最好的解决方案是将库实际安装在单独的目录中，使用 coq_makefile 中正确的 DESTDIR 变量，然后设置 COQPATH 以包含正确的目录。这就是 Nix 和 OPAM 的风格。

Makefile 来自 coq_makefile 的未经测试的示例：

$ ( cd lib-v1 && DESTDIR=~/coqlib/lib-v1 make install )
$ ( cd lib-v2 && DESTDIR=~/coqlib/lib-v2 make install )

$ export COQPATH=~/coqlib/lib-v1:$COQPATH
$ coqtop

【讨论】：

这听起来像是我正在寻找的东西。然而，我还不太清楚你的意思是什么。图书馆只有makefile，但没有coq_makefile，我需要创建一个吗？ “Makefile 来自coq_makefile”是什么意思。我需要在makefile 或控制台中输入命令吗？对不起，如果这些是愚蠢的问题，但整个 makefile 内容目前对我来说只是黑魔法。

我的意思是，如果您使用标准 coq_makefile 设置构建 coq 库 [大多数 coq 库都以这种方式工作]，那么 make 将理解 DESTDIR 变量以将库安装在特定目录。

【参考方案2】：

您可以使用-R 告诉coq 某个目录对应某个名称空间。 （注意-R 有两个参数，目录和命名空间！）

让我们创建两个目录，并编译这两个版本。请注意，我们必须在编译时告诉coqc，目录中的文件应该在MyLib 命名空间中，而不是在默认命名空间中。

D1=~/Desktop/libv1
D2=~/Desktop/libv2

mkdir $D1; echo "Definition a:=1." > $D1/MyLib.v
(cd $D1; coqc -R . MyLib MyLib.v)

mkdir $D2; echo "Definition a:=2." > $D2/MyLib.v
(cd $D2; coqc -R . MyLib MyLib.v)

现在将libv1 用于MyLib

echo "Require Import MyLib. Print a." | \
coqtop -R $D1 MyLib

（将打印a := 1.）并将libv2 用于MyLib

echo "Require Import MyLib. Print a." | \
coqtop -R $D2 MyLib

（将打印a := 2.）

您也可以将-R 标志及其参数放在_CoqProject 文件中，这样您就不必一直将它放在命令行中。 Proof General 也理解这一点。

---

编辑：使用 COQPATH 变量而不是 -R 标志：

(cd $D1; coqc MyLib.v) # compile without -R
(cd $D2; coqc MyLib.v)

# specify the dir using COQPATH
echo "Require Import MyLib. Print a." | COQPATH=$D1 coqtop

# or add it to the LoadPath when you're in coqtop interactively
echo "Add LoadPath \"$D1\". Require Import MyLib. Print a." | coqtop

【讨论】：

如果库很好并且打包并带有makefile等，您应该使用@ejgallego的答案。

我认为使用COQPATH而不是-R加载外部库总是更好。特别是，在_CoqProject 中，您只能为您正在编写的库设置-R，而不是它的依赖项。 （详情请参阅this link）

其实我是建议使用-R 编译，COQPATH 引用库。您应该将MyLib.v 放在目录libv1/MyLib 和libv2/MyLib 中。然后COQPATH=libv1 或COQPATH=libv2 允许加载MyLib.MyLib。