配置 OPAM 开关以安装 Coq 包

Question

从 OPAM 2.0 开始，安装后需要 create/select 一个“开关”才能安装包。如果我将 OPAM 用于 Coq 包，我应该使用什么作为我的开关？

Answer 1

这是我昨天应用的命令序列，用于启动 coq 和 运行 opam，在一台我没想到的机器上。它恰好是一台 fedora-32 机器，但我希望类似的脚本可以在其他架构上运行。无论如何，唯一的特定命令是安装 opam 的命令，显然这已经在您的机器上完成了。

# execute this command with root privileges, for instance via sudo
dnf install opam

对于您来说，只需要以下几行。

# the rest shoud be done without root privilege, as the plain user

opam init # I usually answer no to the questions asked
# replace coq-experiment with the name you like
opam switch create coq-experiment ocaml-base-compiler
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-interval --yes # just an example

最后一个 --yes 选项是为了让您不必回答额外的问题，但您可能希望省略此选项以查看将安装什么并同意它。

然后键入下一个命令通常很方便

eval $(opam env)

并且您应该有 coqtop、coqc，可用作 shell 命令。如果您想使用 coqide，您只需请求安装即可。

opam install coqide

应该就是这样了。

仅当您希望在计算机上同时使用多个不同版本的 Coq 时，才需要使用 opam switch 命令。如果某些软件包尚未移植到足够新的 coq 版本，有时需要这样做。