如何告诉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

所以我的问题是：

当我打开vscode时，如果我的终端可以找到coq，为什么会发生这个错误呢？

1. ？
2. ，如何解决这个问题？我需要设置什么路径?为什么？

有人建议我这样做：

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

但它什么也没做，至少也没解决问题.

我确实复制了粘贴：

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

在提示符中，vscode提供给我，它似乎已经修复了它，因为我的脚本被正确地选中了。然而，我发现这令人不安--我不知道它做了什么，也不知道为什么这样做。

有人能向我解释一下为什么会起作用吗？--尤其是看看我的路径(上面打印的) coq已经在全球范围内提供了吗？

要安装代码，请使用他们的平台安装脚本：https://github.com/coq/platform/blob/main/doc/README_macOS.md，我想在完成之后，上面的路径将被更新为正确的东西，我将从vscode复制到set全局。

有关：

• 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. 使用它们的二进制文件https://github.com/coq/platform/blob/main/doc/README_macOS.md安装coq平台，并使用$(opam env)运行bash coq_platform_make.sh更新了my path (Q:不是eval $(opam env)吗？)weird...)
3. made确定vscode设置中的coqtop路径有来自我路径的路径，例如，/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.15~beta1/bin或做echo $PATH，将coq部件复制到vscode的设置中。请注意，您的开关中可能没有coq这个词，但是它已经安装好了，所以我复制了/Users/brandomiranda/.opam/4.12.1/bin，这也很有效。在额外的bellow.
4. restarted vscode中多次提供更多细节，以确保它正在运行上面的路径.

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

有关cotop vscode的信息，请参见

​

​

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

vscode组织：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交换机一定是在我安装平台的不同时间设置的，但是现在我忽略了它，而且我不在这个开关中，所以我认为它不会有多大关系。