如何在Proof General中更改Coq版本？
如何在Proof General中更改Coq版本？
提问于 2020-04-22 15:06:43
我有一些代码只编译coq 8.09.0中的Coq代码。我通常使用的版本是现在最新的版本，也就是Coq 8.11.0。我使用opam switch创建了一个新环境，并在那里安装了Coq8.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切换来改变emacs的用途？有没有办法显式地告诉Proof General它应该使用哪个Coq实例？我是否应该直接使用pacman卸载Coq8.11.0并安装Coq8.09.0(我使用的是manjaro)？
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-04-22 21:38:16
使用M-x和搜索"opam version“给了我一个很有希望的选择
tuareg-opam-update-env这允许一个人切换环境。在打开coq文件之前切换到vst，并且不自动检查Coq的版本似乎工作得很好。当然，这里假设已经安装了tuareg。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/61359163
复制相关文章
相似问题
腾讯云开发者
