如何告诉 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 给我的提示，它似乎已经修复了，因为我的脚本已被正确检查。但是，我发现这个令人不安的 cu 我不知道它做了什么或为什么会起作用。

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

---

fyi 安装代码使用他们的平台安装脚本：https://github.com/coq/platform/blob/main/doc/README_macOS.md 我想在这样做之后上面的 PATH 会被更新为正确的东西我从 vscode 复制粘贴到 set global。

---

相关：

• https://github.com/coq-community/vscoq/issues/243
• 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 和 hombrew/brew。 （请注意，您似乎可以在 linux/ubuntu 的 coda 中管理

   opam

   ）
2. 我使用他们的二进制文件安装了 coq 平台 https://github.com/coq/platform/blob/main/doc/README_macOS.md 并运行

   bash coq_platform_make.sh

   用

   $(opam env)

   更新了我的路径（问：不是用

   eval $(opam env)

   ？奇怪...）
3. 确保 vscode 设置中的 coqtop 路径 (

   VSCode settings (usually with Cmd and comma ,)

   ) 具有来自我的 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 settings (usually with Cmd and comma ,)

去那里）：

---

相关但安装新插件时：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

一定是在我安装平台时的不同时间设置的，但现在我忽略了它并且我不在那个开关中所以我认为它不会很重要。