Stream: Coq users

Topic: ✔ coqtop is not running


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

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

view this post on Zulip Xiyu Zhai (Sep 27 2022 at 02:55):

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

view this post on Zulip Xiyu Zhai (Sep 27 2022 at 02:55):

Just like Lean/Lean4/Haskell extensions

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

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

view this post on Zulip Notification Bot (Sep 27 2022 at 03:17):

Xiyu Zhai has marked this topic as resolved.

view this post on Zulip Notification Bot (Sep 27 2022 at 03:17):

Xiyu Zhai has marked this topic as resolved.

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

view this post on Zulip abab9579 (Sep 27 2022 at 03:24):

Curious, how does Lean work in this aspect?

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

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

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

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

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