How to have vscode find coq?

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:

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.