如何告诉 vscode Coq 在哪里？ （修复无法启动coqtop（coqtop））

Question

我试图在 vscode 中使用 coq，但似乎无法使其工作。

错误：

Could not start coqtop (coqtop)

我得到这个选项：

令人费解，因为我的终端似乎知道 coq 在哪里：

(meta_learning) brandomiranda~/sketching-learning-coq ❯ coqc -v
The Coq Proof Assistant, version 8.14.1
compiled with OCaml 4.10.2
(meta_learning) brandomiranda~/sketching-learning-coq ❯ echo $PATH
/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.14~2022.01/bin:/Users/brandomiranda/opt/anaconda3/envs/meta_learning/bin:/opt/homebrew/bin:/usr/bin:/bin:/usr/sbin:/sbin

所以我的问题是：

1. 如果我的终端可以很好地找到 coq，为什么当我打开 vscode 时会发生此错误？
2. 我该如何解决这个问题？我需要设置什么路径以及为什么？

---

有人建议我这样做：

eval $(opam env); dirname $(which coqtop)

但它没有做任何事情，或者至少没有解决问题...

---

我确实复制粘贴：

/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.14~2022.01/bin

到 vscode 给我的提示，并且似乎已经修复了它，因为我的脚本被正确检查。然而，我发现这令人不安，因为我不知道它做了什么，也不知道为什么会起作用。

有人可以向我解释为什么这有效吗——特别是因为查看我的 PATH（上面打印的）coq 已经在全球范围内可用？

---

仅供参考，使用其平台安装脚本安装代码：https://github。 com/coq/platform/blob/main/doc/README_macOS.md 我想在这样做之后，上面的 PATH 将被更新为我从 vscode 复制粘贴到设置全局的正确内容。

---

相关：

• https://github.com/coq-community/vscoq/issues/243< /a>
• https://github.com/coq-community/vscoq/issues/78
• https://coq.discourse.group/t/coqtop-not-found/856
• https://coq.discourse.group/ t/how-to-have-vscode-fidn-coq/1582?u=brando90

Answer 1

好吧，我想我修好了。这就是我所做的：

1. 创建一个新开关，例如 opam switch create Hammer_switch ocaml-base-compiler.4.12.0 并确保我有 xcode &家庭酿造/酿造。 （请注意，您似乎可以在 linux/ubuntu 中的 coda 中管理 opam ）
2. 我使用其二进制文件安装了 coq plataform https://github.com/coq/platform/blob/main/doc/README_macOS.md 并运行 bash coq_platform_make.sh
   使用 $(opam env) 更新了我的路径（问：不是使用 eval $(opam env)？奇怪...）
3. 确保 vscode 设置中的 coqtop 路径（< code>VSCode 设置（通常使用 Cmd 和逗号,））具有我的 PATH 中的路径，例如/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.15~beta1/bin 或 echo $PATH 将 coq 部分复制到 vscode 的设置中。请注意，您的交换机中可能没有 coq 这个词，但它已经安装了，所以对我来说，我复制了 /Users/brandomiranda/.opam/4.12.1/bin 并且这也有效。更多详细信息请参见下文。
4. 重新启动 vscode 几次以确保它正在运行上述路径。

请参阅：https:// coq.discourse.group/t/how-to-have-vscode-find-coq/1582/2?u=brando90

对于 cotop vscode 请参阅（做VSCode 设置（通常使用 Cmd 和逗号 ,） 前往此处）：

---

相关，但安装新插件时：https://github.com/lukaszcz/coqhammer/issues/122

vscode gitissue：https://github.com/coq-community/vscoq/issues/243

--

不使用官方平台脚本安装 Coq 的其他方式（使用 coq 设置 HPC 机器可能更容易？）

似乎你也可以这样安装 coq：

# - install opam
# brew install opam # for mac
conda install -c conda-forge opam
opam init
# if doing local env? https://stackoverflow.com/questions/72522412/what-does-eval-opam-env-do-does-it-activate-a-opam-environment
# eval $(opam env)

# - install coq
# local install
#opam switch create . 4.12.1
#eval $(opam env)
#opam repo add coq-released https://coq.inria.fr/opam/released
#opam install coq

# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create 4.12.1
opam switch 4.12.1
# eval $(opam env)  # why don't I need this in the global, what makes this global?
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq

虽然我需要弄清楚 eval $(opam env) 去哪里。

---

额外：关于放入 vscode 中的路径名的讨论

我的路径如下所示：

(iit_synthesis) brandomiranda~ ❯ echo $PATH
/Users/brandomiranda/.opam/4.12.1/bin:/Users/brandomiranda/miniconda/envs/iit_synthesis/bin:/Users/brandomiranda/miniconda/condabin:/usr/local/bin:/Users/brandomiranda/.opam/4.12.1/bin:/opt/homebrew/bin:/usr/bin:/bin:/usr/sbin:/sbin

但我已经在交换机 4.12.1 上，并在其中安装了 coq，因为我运行了：

# - install opam
brew install opam
# https://stackoverflow.com/questions/72522266/how-does-one-install-opam-with-conda-for-mac-apple-os-x
# conda install -c conda-forge opam
opam init
# if doing local env? https://stackoverflow.com/questions/72522412/what-does-eval-opam-env-do-does-it-activate-a-opam-environment
#eval $(opam env)

# - install coq
# local install
#opam switch create . 4.12.1
#eval $(opam env)
#opam repo add coq-released https://coq.inria.fr/opam/released
#opam install coq

# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create 4.12.1
opam switch 4.12.1
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq

在该状态下，我测试了 coq终端就在那里：

(iit_synthesis) brandomiranda~ ❯ opam switch
#  switch                                 compiler                    description
→  4.12.1                                 ocaml-base-compiler.4.12.1  4.12.1
   __coq-platform.2022.01.0~8.14~2022.01  ocaml-base-compiler.4.10.2  __coq-platform.2022.01.0~8.14~2022.01
(iit_synthesis) brandomiranda~ ❯ coqtop
Welcome to Coq 8.15.1

Coq < ^C
Error: User interrupt.

Coq < ^D

还有开关 __coq-platform.2022.01.0~8.14~2022.01 ocaml-base-compiler.4.10.2 __coq-platform.2022.01.0~8.14~2022.01 必须是在我进行平台安装时的不同时间设置的，但现在我忽略它并且我不在那个开关中，所以我不认为这很重要。