Stream: VsCoq devs & users

Topic: Coq master branch and VSCoq

view this post on Zulip Enzo Crance (Dec 03 2020 at 16:14):

Hello. After installing an instable version of Coq (the current master branch), I keep getting this error when interpreting the first line of a file:

coqtop closed with code: Error: spawn coqidetop.opt ENOENT

Does any reason come to your mind to explain this error? When coming back to another opam switch and relaunching the IDE, the error vanishes, and I have made sure the error happens on a line that is linked with no external library.

Thanks in advance for your help.

view this post on Zulip Fabian Kunze (Dec 03 2020 at 16:27):

I can't reproduce this with a newly build coqidetop.
Can you describe your setup (OS) a bit more? can you do where coqidetop.opt in the terminal? Can you close all vscode-windows and then call vscode using code from the same terminal and test if the error persists?

view this post on Zulip Enzo Crance (Dec 03 2020 at 16:38):

Here is the setup: macOS Catalina (10.15.6) - OCaml 4.11.1 - dune pinned to master - Coq pinned to master
It cannot find the executable. Is there an option to activate when building Coq to build coqidetop at the same time?
Using the command open /Applications/Visual\ Studio\ does not change the error.

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 18:22):

If you build with dune -p coq, then yes, coqidetop is not included, and you need to also do dune -p coqide-server.

view this post on Zulip Enzo Crance (Dec 03 2020 at 18:38):

@Théo Zimmermann Do you know how to run this command in an opam context? The Coq install is from the master branch, but has been done through opam pin. I have no clue how to control the script that is run to build Coq to include that additional target.

view this post on Zulip Notification Bot (Dec 07 2020 at 10:07):

This topic was moved by Théo Zimmermann to #Coq users > Installing coqidetop dev with opam

Last updated: Jun 04 2023 at 23:30 UTC