Enzo Crance (Dec 03 2020 at 16:14): 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.
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?
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\ Code.app/ does not change the error.
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.
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.
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