I am trying to use Coq with VScode and I do not understand how to make it find "the path to coqtop". Coq is installed (I have used it with CoqIde so far), VScode as well, I installed the extension and I can open .v files in VSCode but not yet compile them.
To be sure, can you confirm that in VScode, the “Interpret” commands fail? (Right click on a
.v file, then click “interpret to point”).
If so, intuitively, you need to find _where_ coq is installed.
Which OS are you on?
This should be on the VsCoq stream instead. cc @Théo Zimmermann
Thanks, I was not aware of that other stream. Is there a way to move the discussion or should I start a new one there?
@Paolo Giarrusso I am on Windows 10 and there is no "interpret" option when I right-click on a .v file.
If VsCoq is installed, maybe my instructions were unclear: that option appears when you open a .v file in vscode and right-click in the buffer.
(Discussions can be moved, so we can continue in this thread for now)
But I’d add Windows to the title; I don’t use Windows and can’t really answer the question.
IIRC, you need to find where coqtop.exe is installed, and provide vscoq with the path to the folder where coqtop.exe lives.
How did you install Coq on Windows?
I found the command "interpret to point", which says: not running. I installed coq through the official website, and then mathcomp using opam.
Now, I found coqtop.exe at this address: C:\Coq\bin. But VSCode still says 'coqtop not found here'...
@Guillaume Dubach re “vscode still says”, have you given to vscode the path to vscoq, and how exactly?
Given your question I thought you had found the right vscode setting.
This topic was moved here from #Coq users > Using Coq with VScode under windows 10 by Théo Zimmermann
You installed Coq using the installer and math-comp using opam ?? The Windows installer already contains math-comp as an optional add-on, but if you install math-comp using opam, then it will also install Coq in your opam switch. Which probably means that you have two Coq installs in parallel... and VsCoq find none of them...
@Théo Zimmermann I had no idea math-comp was automatically included by the windows installer, and somehow I assumed that the installation instructions for math-comp implied that it wasn't... At least this is not mentioned explicitly. So it might well be that I have now Coq installed twice. Do you think this is part of the problem for VsCode?
@Paolo Giarrusso When I try to make it compile a .v file, it says "could not start coqtop" in a pop-up window and allows me to click on "set path for this project", or "set path globally". So I click on one, and I am invited to write the path on a line above. If I write nonsense it just says "invalid path". If I write what I assume to be the correct path C:\Coq\bin, it says "coqtop not found here", in a red rectangle below what I write.
Do you think this is part of the problem for VsCode?
somehow I assumed that the installation instructions for math-comp implied that it wasn't...
Indeed, it's too bad that this is not documented in math-comp's README.
If I write what I assume to be the correct path C:\Coq\bin, it says "coqtop not found here", in a red rectangle below what I write.
It's possible that it looks for
coqtop (or actually
coqidetop) and not
coqidetop.exe. I wonder if there's a way to change the name of the program.
It's also possible that you will have better luck with the opam-based install if you manage to find where it is.
Any chance you need to write the actual path to coqtop, maybe including the .exe? I don’t need to, but I’m not sure what the code does.
Or rather, I vaguely remember I don’t like that particular bit of code on Windows...
Nevermind, I think I do. https://github.com/coq-community/vscoq/commit/8b71a367dd90161812117bb95e2f2a20f213d547
Among vscode settings, there should be a page for vscoq settings that you can configure. Please don’t mix user and workspace setting, that’ll only add headaches - probably best use “user” settings (for all projects)
(Don’t mix them for now at least)
There should even be a setting for the coqtop name. You shouldn’t need to add coqtop.exe there, vscoq should try automatically, but I won’t exclude some bug might get in the way
@Paolo Giarrusso Yes, thanks! It took me some time to figure it out, but indeed under "users settings" there is also a way to indicate the path to coqtop. And then, "C:\Coq\bin" actually works. It is still a mystery to me why it doesn't work the other way (no matter how I write it, with or without .exe...). But anyway, this should be fine.
@Théo Zimmermann I did not find another install of Coq on my computer, so either opam did not change anything to this, or it re-installed it in the same place. :) But thank you for your suggestions!
@Guillaume Dubach I am afraid to ask, but is your computer 32 or 64 bit?
It shouldn’t, but some of the involved code checks if the platform is
win32, so I don’t know. Hopefully not.
also VsCoq tests for
win32 for both ways of setting the path...
win32 as nothing to do with 32 bits vs 64 bits despite the confusing name.
@Guillaume Dubach Did you locate the opam root at all?
@Théo Zimmermann Now I have! Hidden somewhere in the OCaml64 folder. So indeed, there is another coqtop.exe there. But for some reason it wasn't found when I did a general search on my computer.
The mysteries of Windows...
Anyway, bottom line is: it's not a problem for you to have these two copies, but you should be aware that they are two completely separate things. Libraries installed in one place won't be available in the other.
Re win32, it did use to mean 32bit, but because of lots of code using it to mean "windows" they had to relent. But I'm happy if that's a distraction here.
Last updated: Jun 04 2023 at 22:30 UTC