3

我有一些代码只能在 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 并直接使用（我正在使用 manjaro）安装 Coq 8.09.0吗？

4

1 回答 1

3

使用M-x和搜索“opam 版本”给了我一个有希望的选择

tuareg-opam-update-env

这允许一个人切换环境。在打开 coq 文件之前执行此操作以切换到 vst 并且不自动检查 Coq 的版本似乎工作正常。当然，这假设已经安装了 tuareg。

于 2020-04-22T13:38:16.453 回答