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

5

is this a good answer? visual studio code - How to tell vscode where Coq is? (fixing Could not start coqtop (coqtop)) - Stack Overflow

Ok I fixed it I think. This is what I did:

  1. create a new switch e.g. opam switch create hammer_switch ocaml-base-compiler.4.12.0 and made sure I had xcode & hombrew/brew. (note you can have opam managed in coda in linux/ubuntu it seems)
  2. I installed the coq plataform using their binaries platform/README_macOS.md at main · coq/platform · GitHub and ran bash coq_platform_make.sh
    updated my path with $(opam env) (Q: not with eval $(opam env)? weird…)
  3. made sure coqtop path in the vscode settings had the path from my PATH e.g. /Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.15~beta1/bin or do echo $PATH copy the coq part into vscode’s setting. Note that your switch might not have the word coq in it but it istall has it installed so for me I copied /Users/brandomiranda/.opam/4.12.1/bin and that worked too. More details in extra bellow.
  4. restarted vscode several times to make sure it was running the above path.

see: How to have vscode find coq? - #2 by Blaisorblade

for the cotop vscode see

enter image description here

related but when installing new plugin: Installation issues -- No package named coq-hammer-tactics found · Issue #122 · lukaszcz/coqhammer · GitHub

vscode gitissue: How to set the coq path for vscode (how to find coqtop)? · Issue #243 · coq-community/vscoq · GitHub

–

Other way to install Coq not using the official plataform scripts (might be easier to set up HPC machines with coq?)

Seems you can install coq this way too:

# - 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

though I need to figure out where eval $(opam env) goes.

Extra: discussion on path names to put in vscode

My path looked as follows:

(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

but I was already on the switch 4.12.1 already and installed coq in it because I ran:

# - 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

In that state I test coq in terminal and it was there:

(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

and the switch __coq-platform.2022.01.0~8.14~2022.01 ocaml-base-compiler.4.10.2 __coq-platform.2022.01.0~8.14~2022.01 must have been set up at a different time when I did plataform install but now I’m ignoring it and I’m not in that switch so I don’t think it will matter much.

6

related: How to import Basics.v in Induction.v of LF using VS Coq extension - #7 by onlychans1