coq - 配置 OPAM 开关以安装 Coq 包

Question

从 OPAM 2.0 开始，安装后需要在安装包之前创建/选择一个“开关”。如果我使用 OPAM 只是 Coq 包，我应该使用什么作为我的开关？

标签： coqopam

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

应该就是这样。

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