如何在Proof General中更改Coq版本？

Question

我有一些仅在Coq 8.09.0中编译coq代码的代码。我通常使用的版本是现在的最新版本，即Coq 8.11.0。我能够使用opam开关创建一个新环境，并在那里安装了Coq 8.09.0。我使用此版本成功编译了所有文件；但是，我不能在emacs中使用通用证明，因为它仍在使用Coq 8.11.0。我想知道如何通过Emacs中的opam开关使Proof General使用不同的opam实例。我尝试在eshell中执行以下操作

opam switch vst
eval $(opam env)

其中vst是交换机的名称，如我终端中opam switch的输出所示：

#   switch   compiler                                                                         description
    4.10.0   ocaml-base-compiler.4.10.0                                                       4.10.0
    default  base-bigarray.base,base-threads.base,base-unix.base,ocaml.4.02.3,ocaml-config.1  default
->  vst      ocaml-base-compiler.4.09.0                                                       vst

但是，eval $(opam env)行的输出如下：

Symbol’s function definition is void: opam

这没有意义，因为它了解opam的含义，因为它能够很好地执行第一个命令。是否有进行opam切换以更改emacs使用的正确方法？有没有一种方法可以明确地告诉Proof General，它应该使用哪个Coq实例？我应该直接使用pacman卸载Coq 8.11.0并直接安装Coq 8.09.0吗？（我使用的是manjaro）？

Answer 1

使用M-x并搜索“ opam版本”给了我一个很有前途的选择

tuareg-opam-update-env

允许切换环境。这样做是在打开coq文件之前切换到vst，并且不自动检查Coq的版本似乎很好。当然，这是假设已经安装了tuareg。