Stream: VsCoq devs & users

Topic: Using Coq with VScode under windows 10


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 24 2020 at 15:01):

Which OS are you on?

view this post on Zulip Théo Winterhalter (Oct 24 2020 at 16:14):

This should be on the VsCoq stream instead. cc @Théo Zimmermann

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 24 2020 at 16:30):

(Discussions can be moved, so we can continue in this thread for now)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 24 2020 at 16:33):

How did you install Coq on Windows?

view this post on Zulip 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'...

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Oct 24 2020 at 18:21):

Given your question I thought you had found the right vscode setting.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Oct 24 2020 at 20:32):

Do you think this is part of the problem for VsCode?

No.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 24 2020 at 21:04):

Or rather, I vaguely remember I don’t like that particular bit of code on Windows...

view this post on Zulip Paolo Giarrusso (Oct 24 2020 at 21:06):

Nevermind, I think I do. https://github.com/coq-community/vscoq/commit/8b71a367dd90161812117bb95e2f2a20f213d547

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Oct 24 2020 at 21:10):

(Don’t mix them for now at least)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Paolo Giarrusso (Oct 27 2020 at 15:43):

@Guillaume Dubach I am afraid to ask, but is your computer 32 or 64 bit?

view this post on Zulip Guillaume Dubach (Oct 27 2020 at 15:44):

  1. Would it make a big difference?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 27 2020 at 15:47):

also VsCoq tests for win32 for both ways of setting the path...

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Oct 27 2020 at 15:53):

@Guillaume Dubach Did you locate the opam root at all?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Oct 27 2020 at 16:12):

The mysteries of Windows...

view this post on Zulip 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.

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC