I was trying to use coq in vscode but I can’t seem to make it to work.
Error:
Could not start coqtop (coqtop)
which is puzzling since my terminal seems to know just fine where coq is:
(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
So my questions are:
- Why is this error happening when I open vscode if my terminal can find coq just fine?
- How do I fix this? What path do I need to set and why?
I was suggested to do:
eval $(opam env); dirname $(which coqtop)
but it didn’t do anything or at least it didn’t fix the problem…
related:
- How to set the coq path for vscode (how to find coqtop)? · Issue #243 · coq-community/vscoq · GitHub
- coqtop could not be started: Error: spawn coqidetop.opt ENOENT · Issue #78 · coq-community/vscoq · GitHub
- Coqtop not found
- visual studio code - How to tell vscode where Coq is? (fixing Could not start coqtop (coqtop)) - Stack Overflow
- Installation issues -- No package named coq-hammer-tactics found · Issue #122 · lukaszcz/coqhammer · GitHub issues with coqhammer