Stream: VsCoq devs & users

Topic: How do you get VSCoq to work?

view this post on Zulip Luna Tuna (Sep 02 2022 at 23:50):

image.png

Output pane:

starting coqtop
exec: C:\Coq-Platform~8.15~2022.04\bin\coqtop -v
Listening at 127.0.0.1:64165
Listening at 127.0.0.1:64166
Listening at 127.0.0.1:64167
Listening at 127.0.0.1:64168
starting coqtop
exec: C:\Coq-Platform~8.15~2022.04\bin\coqtop -v
Listening at 127.0.0.1:64170
Listening at 127.0.0.1:64171
Listening at 127.0.0.1:64172
Listening at 127.0.0.1:64173
Detected coqtop version 8.15.2
Coqtop version parsed into semver version 8.15.2
exec: C:\Coq-Platform~8.15~2022.04\bin\coqidetop.opt -main-channel 127.0.0.1:64165:64166 -control-channel 127.0.0.1:64167:64168 -async-proofs on -topfile file:///c%3A/Users/fruit/OneDrive/Desktop/CoqPractice/practice1
coqtop started with pid 2676
Detected coqtop version 8.15.2
Coqtop version parsed into semver version 8.15.2
exec: C:\Coq-Platform~8.15~2022.04\bin\coqidetop.opt -main-channel 127.0.0.1:64170:64171 -control-channel 127.0.0.1:64172:64173 -async-proofs on -topfile file:///c%3A/Users/fruit/OneDrive/Desktop/CoqPractice/practice1
coqtop started with pid 12216
Client connected on main channel R (port 64165)
Client connected on main channel W (port 64166)
Client connected on control channel R (port 64167)
Client connected on control channel W (port 64168)
--------------------------------
Call Init()
Client connected on main channel R (port 64170)
Client connected on main channel W (port 64171)
Client connected on control channel R (port 64172)
Client connected on control channel W (port 64173)
--------------------------------
Call Init()
coqtop-stderr: Error:
Invalid character ':' in identifier "file:///c%3A/Users/fruit/OneDrive/Desktop/CoqPractice/practice1".


[Error - 4:49:09 PM] Error on main channel (R): read ECONNRESET
onCoqClosed(undefined)
coqtop exited with code: null
coqtop closed with code: null
coqtop-stderr: Error:
Invalid character ':' in identifier "file:///c%3A/Users/fruit/OneDrive/Desktop/CoqPractice/practice1".


[Error - 4:49:09 PM] Error on control channel (R): read ECONNRESET
onCoqClosed(undefined)
coqtop exited with code: null
coqtop closed with code: null

view this post on Zulip Paolo Giarrusso (Sep 03 2022 at 01:04):

on all platforms, the file name should end in .v and be a valid identifier — so practice1.v would work

view this post on Zulip Paolo Giarrusso (Sep 03 2022 at 01:06):

does that fix the problem?

view this post on Zulip Paolo Giarrusso (Sep 03 2022 at 01:09):

VSCoq is reported to work on Windows, that's why I hope that adding the extension is enough and that the error message is just inaccurate (if it were accurate good luck!).

view this post on Zulip Notification Bot (Sep 03 2022 at 10:26):

This topic was moved here from #Coq users > How do you get VSCoq to work? by Karl Palmskog.

view this post on Zulip Luna Tuna (Sep 03 2022 at 11:37):

Paolo Giarrusso said:

VSCoq is reported to work on Windows, that's why I hope that adding the extension is enough and that the error message is just inaccurate (if it were accurate good luck!).

I think that fixed it

Last updated: Jun 04 2023 at 22:30 UTC