How to have vscode find coq?

Using Coq
#1

I was trying to use coq in vscode but I can’t seem to make it to work.

Error:

Could not start coqtop (coqtop)

I get this option:
enter image description here

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:

  1. Why is this error happening when I open vscode if my terminal can find coq just fine?
  2. 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:

#2

Opening multiple threads means information isn’t collected together

You’re on a Mac, so the PATH you set in the command line (via shell configuration) is not passed to any graphical application, and macOS doesn’t allow fixing that.

Instead, you can explicitly write the path to the Coq binary in the VSCode configuration. To do that, open the VSCode settings (usually with Cmd and comma ,), search for “coq bin path”, and paste there the path to coqc — in your case, it seems to be /Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.14~2022.01/bin:

image
image2278×654 61.2 KB

Then restart VSCoq, make sure the setting was saved correctly, and things should work.

To avoid problems, you should always make sure that the path you tell vscoq and the path you use on the command line to compile files coincide. Configuration mistakes here can be recognized because you’ll get errors like

Error: File path/to/foo.vo has
bad version number 81300 (expected 81400). It is corrupted or was compiled with another version of Coq.

or

Error: Compiled library a.b.c (in file path/to/a/b/c.vo) makes inconsistent assumptions over library d.e.f.
#3

BTW, this setting is briefly documented in GitHub - coq-community/vscoq: A Visual Studio Code extension for Coq [maintainers=@maximedenes,@fakusb], but I’ve seen lots of people struggle with this, so better, step-by-step docs might be useful.

#4

as a bonus question, if you change your switch (or install a new coq package) make sure to update the path in vscode and change switch e.g. see: Installation issues -- No package named coq-hammer-tactics found · Issue #122 · lukaszcz/coqhammer · GitHub