Stream: Coq users

Topic: ✔ coqtop is not running

Xiyu Zhai (Sep 27 2022 at 02:51):

Hi, everyone, I find it really really hard to make vscoq work on vscode. I installed coq using opam and set
coqtop.binPath as "/home/xiyuzhai/.opam/default/bin/", only to get a notice "coqtop is not running"; there is no error message anywhere, including Coq Language Server output.

Updated project root to .
Coqtop binPath is:
Updated project root to .
Coqtop binPath is: /home/xiyuzhai/.opam/default/bin/
Updated project root to .
Coqtop binPath is: /home/xiyuzhai/.opam/default/bin/

Xiyu Zhai (Sep 27 2022 at 02:54):

From a programming point of view, I expect the extension to be more verbose about what's going on.

Xiyu Zhai (Sep 27 2022 at 02:55):

It would be great if the extension can automatically install things needed.

Xiyu Zhai (Sep 27 2022 at 02:55):

Just like Lean/Lean4/Haskell extensions

Xiyu Zhai (Sep 27 2022 at 02:57):

Is it possibly that there aren't many people using vscode for Coq? So that weird bugs are not spotted that fast.

Xiyu Zhai (Sep 27 2022 at 02:59):

Also, I couldn't find what is the default package manager for Coq. I would like to do things like lake init or cargo new in Coq. I'm a newbie, I'm basically confused about everything

Notification Bot (Sep 27 2022 at 03:17):

Xiyu Zhai has marked this topic as resolved.

Notification Bot (Sep 27 2022 at 03:17):

Xiyu Zhai has marked this topic as resolved.

Xiyu Zhai (Sep 27 2022 at 03:18):

I understand. Coq is different from Lean in that it needs to first interpret to end.
I got confused from Lean experience.

abab9579 (Sep 27 2022 at 03:24):

Curious, how does Lean work in this aspect?

Huỳnh Trần Khanh (Sep 27 2022 at 05:19):

I have to admit I don't understand the OP's question, but in Lean, the goal state in the "infoview" (the stuff on the right, similar to Coq) changes every time you change the cursor position.

Huỳnh Trần Khanh (Sep 27 2022 at 05:21):

Maybe the VsCoq extension can be configured to do this too. But I prefer the default settings. If I want to see the current state I have to hit Alt+Right.

Huỳnh Trần Khanh (Sep 27 2022 at 05:23):

OP, you don't have to worry about the "coqtop is not running" message. That's normal. Just hit Alt+Right to view the current goal state.

abab9579 (Sep 27 2022 at 07:37):

I see, that behavior sounds quite similar to Coq except for the cursory details (like how "proof cursor" moves)

Ana de Almeida Borges (Sep 27 2022 at 10:14):

Xiyu Zhai said:

Also, I couldn't find what is the default package manager for Coq. I would like to do things like lake init or cargo new in Coq. I'm a newbie, I'm basically confused about everything

If I understand your question correctly, that's opam, which apparently you are already using.

Last updated: Oct 03 2023 at 21:01 UTC