title: How to tell vscode where Coq is? (fixing Could not start coqtop (coqtop))
body: <p>I was trying to use coq in vscode but I can't seem to make it to work.</p>
  <p>Error:</p>
  <pre><code>Could not start coqtop (coqtop)
  </code></pre>
  <p>I get this option:
  <a href="https://i.stack.imgur.com/QeUxp.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/QeUxp.png" alt="enter image description here" /></a></p>
  <p>which is puzzling since my terminal seems to know just fine where coq is:</p>
  <pre><code>(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
  </code></pre>
  <p>So my questions are:</p>
  <ol>
  <li>Why is this error happening when I open vscode if my terminal can find coq just fine?</li>
  <li>How do I fix this? What path do I need to set and why?</li>
  </ol>
  <hr />
  <p>I was suggested to do:</p>
  <pre><code>eval $(opam env); dirname $(which coqtop)
  </code></pre>
  <p>but it didn't do anything or at least it didn't fix the problem...</p>
  <hr />
  <p>I did copy pasted:</p>
  <pre><code>/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.14~2022.01/bin
  </code></pre>
  <p>to the prompt vscode gives me and it seems to have fixed it since my script was checked correctly. However, I find this disturbing cu I don't know what it did or why this worked.</p>
  <p>Can someone explain to me why this worked -- especially since looking at my PATH (printed above) coq is globally available already?</p>
  <hr />
  <p>fyi to install code use their plataform install scripts: <a href="https://github.com/coq/platform/blob/main/doc/README_macOS.md" rel="nofollow noreferrer">https://github.com/coq/platform/blob/main/doc/README_macOS.md</a> I suppose after doing that the above PATH would have been updated to the right thing that I copy pasted to the set global from vscode.</p>
  <hr />
  <p>related:</p>
  <ul>
  <li><a href="https://github.com/coq-community/vscoq/issues/243" rel="nofollow noreferrer">https://github.com/coq-community/vscoq/issues/243</a></li>
  <li><a href="https://github.com/coq-community/vscoq/issues/78" rel="nofollow noreferrer">https://github.com/coq-community/vscoq/issues/78</a></li>
  <li><a href="https://coq.discourse.group/t/coqtop-not-found/856" rel="nofollow noreferrer">https://coq.discourse.group/t/coqtop-not-found/856</a></li>
  <li><a href="https://coq.discourse.group/t/how-to-have-vscode-fidn-coq/1582?u=brando90" rel="nofollow noreferrer">https://coq.discourse.group/t/how-to-have-vscode-fidn-coq/1582?u=brando90</a></li>
  </ul>