Guillaume Dubach (Oct 24 2020 at 14:12): Guillaume Dubach (Oct 24 2020 at 14:12):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.
Paolo Giarrusso (Oct 24 2020 at 15:01):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.
Paolo Giarrusso (Oct 24 2020 at 15:01):Which OS are you on?
Théo Winterhalter (Oct 24 2020 at 16:14):This should be on the VsCoq stream instead. cc @Théo Zimmermann
Guillaume Dubach (Oct 24 2020 at 16:28):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.
Paolo Giarrusso (Oct 24 2020 at 16:29):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.
Paolo Giarrusso (Oct 24 2020 at 16:30):(Discussions can be moved, so we can continue in this thread for now)
Paolo Giarrusso (Oct 24 2020 at 16:31):But I’d add Windows to the title; I don’t use Windows and can’t really answer the question.
Paolo Giarrusso (Oct 24 2020 at 16:32):IIRC, you need to find where coqtop.exe is installed, and provide vscoq with the path to the folder where coqtop.exe lives.
Paolo Giarrusso (Oct 24 2020 at 16:33):How did you install Coq on Windows?
Guillaume Dubach (Oct 24 2020 at 16:35):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'...
Paolo Giarrusso (Oct 24 2020 at 18:20):@Guillaume Dubach re “vscode still says”, have you given to vscode the path to vscoq, and how exactly?
Paolo Giarrusso (Oct 24 2020 at 18:21):Given your question I thought you had found the right vscode setting.
Notification Bot (Oct 24 2020 at 19:28):This topic was moved here from #Coq users > Using Coq with VScode under windows 10 by Théo Zimmermann
Théo Zimmermann (Oct 24 2020 at 19:30):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...
Guillaume Dubach (Oct 24 2020 at 20:21):@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?
Guillaume Dubach (Oct 24 2020 at 20:29):@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.
Théo Zimmermann (Oct 24 2020 at 20:32):Do you think this is part of the problem for VsCode?
No.
Théo Zimmermann (Oct 24 2020 at 20:34):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.
Théo Zimmermann (Oct 24 2020 at 20:37):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 coqtop.exe / coqidetop.exe. I wonder if there's a way to change the name of the program.
Théo Zimmermann (Oct 24 2020 at 20:38):It's also possible that you will have better luck with the opam-based install if you manage to find where it is.
Paolo Giarrusso (Oct 24 2020 at 21:04):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.
Paolo Giarrusso (Oct 24 2020 at 21:04):Or rather, I vaguely remember I don’t like that particular bit of code on Windows...
Paolo Giarrusso (Oct 24 2020 at 21:06):Nevermind, I think I do. https://github.com/coq-community/vscoq/commit/8b71a367dd90161812117bb95e2f2a20f213d547
Paolo Giarrusso (Oct 24 2020 at 21:10):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)
Paolo Giarrusso (Oct 24 2020 at 21:10):(Don’t mix them for now at least)
Paolo Giarrusso (Oct 24 2020 at 21:11):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
Guillaume Dubach (Oct 27 2020 at 15:40):@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.
Guillaume Dubach (Oct 27 2020 at 15:43):@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!
Paolo Giarrusso (Oct 27 2020 at 15:43):@Guillaume Dubach I am afraid to ask, but is your computer 32 or 64 bit?
Guillaume Dubach (Oct 27 2020 at 15:44): Paolo Giarrusso (Oct 27 2020 at 15:46):It shouldn’t, but some of the involved code checks if the platform is win32, so I don’t know. Hopefully not.
Paolo Giarrusso (Oct 27 2020 at 15:47):also VsCoq tests for win32 for both ways of setting the path...
Théo Zimmermann (Oct 27 2020 at 15:52):AFAIK win32 as nothing to do with 32 bits vs 64 bits despite the confusing name.
Théo Zimmermann (Oct 27 2020 at 15:53):@Guillaume Dubach Did you locate the opam root at all?
Guillaume Dubach (Oct 27 2020 at 16:04):@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.
Théo Zimmermann (Oct 27 2020 at 16:12):The mysteries of Windows...
Théo Zimmermann (Oct 27 2020 at 16:13):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.
Paolo Giarrusso (Oct 27 2020 at 19:09):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