是否可以在 Coq 中安装同一个库的多个版本？如果是，我该如何选择要使用的版本？
我在 Windows 中工作，因此任何使用 OPAM 的解决方案都对我没有帮助。
【问题讨论】：
标签： libraries coq multiple-versions
最好的解决方案是将库实际安装在单独的目录中，使用 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 变量以将库安装在特定目录。
您可以使用-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
【讨论】：
COQPATH而不是-R加载外部库总是更好。特别是，在_CoqProject 中，您只能为您正在编写的库设置-R，而不是它的依赖项。 （详情请参阅this link）
-R 编译，COQPATH 引用库。您应该将MyLib.v 放在目录libv1/MyLib 和libv2/MyLib 中。然后COQPATH=libv1 或COQPATH=libv2 允许加载MyLib.MyLib。