Stream: VsCoq devs & users

Topic: Coqtop path and coq project file


view this post on Zulip Andrew Spears (Nov 29 2022 at 18:26):

Hi all - I have been using Vscoq on mac for some basic things in a file with no dependencies for a while with no issues, but recently tried opening a bigger project with some imports and ran into errors.

When I first setup coq in VScode, I first installed coq from the website, but had some issues and ended up installing it with Homebrew. In VScode, I used the "Coqtop Bin path" setting and I used the path "/Applications/Coq-Platform~8.15~2022.04.app/Contents/Resources/bin", which worked perfectly (I installed with Homebrew before I figured this out, turns out there was nothing wrong with the installation). I then tried stepping through a file with some imports (one of which was import coqutil.Word.LittleEndian), and got the error "Cannot find a physical path bound to logical path coqutil.Word.LittleEndian".

To fix this, I set the Coqproject path in VScode's settings to "bedrock2/compiler/_CoqProject", which I got from the 'copy relative path' dropdown in the explorer. I'm assuming this path is correct because if I intentionally put something incorrect, I get an error saying no such file exists. The strange part is that with this setting changed (but without modifying the coqtop bin path), I now get the error "Could not start coqtop (/Applications/Coq-Platform~8.15~2022.04.app/Contents/Resources/bin/coqtop)". This is the same error I get when trying to step through the file with no dependencies if I intentionally put an incorrect coqtop bin path, even though I only changed the CoqProject path. If I delete the CoqProject path and restart vscode, it suddenly works for the file with no dependencies.

I tried changing the coqtop path to /usr/local/Cellar/coq/8.16.0/bin to use the Brew installation, and this also works fine for the file with no dependencies but has exactly the same issues with Coqproject.

I'm mainly confused by the fact that changing the Coqproject setting gives an error which seems to indicate an issue with the coqtop path - I would appreciate any ideas on why this might be happening. Thanks!

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 18:36):

I always set the _CoqProject path to the folder containing _CoqProject.

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 18:37):

And the error doesn't say that coqtop wasn't found, just that it couldn't be started; I suspect coqtop is being passed invalid enough settings that it exits right away.

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 18:39):

If that's not enough, the "Coq Language Server" view below will show the actual command line and Coq outputs, so it might be helpful for troubleshooting. I'm on a phone so I can't give better instructions, but feel free to ping again


Last updated: Jun 04 2023 at 23:30 UTC