如何更改 Proof General 中的 Coq 版本?

How to change Coq Version in Proof General?

我有一些代码只能在 Coq 8.09.0 中编译 coq 代码。我通常使用的版本是现在最新的版本,即 Coq 8.11.0。我能够使用 opam 开关创建一个新环境并在那里安装 Coq 8.09.0。我用这个版本成功编译了所有文件;但是,我不能在 emacs 中使用 proof general,因为它仍在使用 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 switch 来更改 emacs 使用的内容?有没有办法明确告诉 Proof General 它应该使用哪个 Coq 实例?我是否应该卸载 Coq 8.11.0 并直接使用 pacman(我正在使用 manjaro)安装 Coq 8.09.0?

使用 M-x 并搜索 "opam version" 给了我有前途的选择

tuareg-opam-update-env

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