Gabriel Mazieri (Jan 25 2023 at 12:49): Gabriel Mazieri (Jan 25 2023 at 12:49):I think i should start making clear what i already tried, so...
Everything above i already tried, installing, reinstalling and everything, but, vscoq doesn't work when i try to use any feature.
What can i do to make vscoq work?
Notification Bot (Jan 25 2023 at 12:51):This topic was moved here from #Coq users > VSCoq extension for VSCode doesn't work by Karl Palmskog.
Paolo Giarrusso (Jan 25 2023 at 15:43):ah, also on https://github.com/coq-community/vscoq/issues/333
Paolo Giarrusso (Jan 25 2023 at 15:44):we'll need more than "doesn't work", for instance a gist with the contents of the "Coq Language Server" tab under the "Output" VsCoq pane.
Karl Palmskog (Jan 25 2023 at 15:47):one thing to note is that if Coq is installed via opam, and that's the Coq one wants to use in VsCoq, having Coq binary path /usr/bin inside VS Code is unlikely to work. opam Coq binaries generally show up in a user's home directory, e.g., /home/username/.opam/4.14.0/bin
Paolo Giarrusso (Jan 25 2023 at 15:56):ooh right, you claim to have installed Coq using _both_ opam and yay?
Paolo Giarrusso (Jan 25 2023 at 15:59):as general advice: installing more than one Coq version at a time means risking trouble.
Paolo Giarrusso (Jan 25 2023 at 16:00):or rather, it's an "advanced" configuration
Gabriel Mazieri (Jan 25 2023 at 16:58):Here is my log from "Coq Language Server" Output from vscode: https://gist.github.com/grandehe4rt/1cc88bbdcfced42c7697467d64415eab
The proof assistant never pops up, what else can i try to solve this problem?
Gabriel Mazieri (Jan 25 2023 at 17:01):Paolo Giarrusso said:
ooh right, you claim to have installed Coq using _both_ opam and yay?
I installed using both but, I noticed that could lead to problem so I uninstalled using yay -R coq and inside vscode I setup the bin path properly for the opam path
Paolo Giarrusso (Jan 25 2023 at 17:44):@Gabriel Mazieri according to that log, you've never asked to start Coq, so VsCoq hasn't tried. You need to ask vscoq to step through a file; let me search docs on the right commands
Paolo Giarrusso (Jan 25 2023 at 17:45):@Gabriel Mazieri try "step forward" or "interpret to end" in https://github.com/coq-community/vscoq#basic-usage
Paolo Giarrusso (Jan 25 2023 at 17:46):You need an open .v file for doing that
Paolo Giarrusso (Jan 25 2023 at 17:46):(to be clear, docs could explain that better)
Gabriel Mazieri (Jan 25 2023 at 17:57):I already tried this commands, unfortunetly the proof assistant never pop's up for me.
Gabriel Mazieri (Jan 25 2023 at 17:58):And the output log doesn't update at all
Gabriel Mazieri (Jan 25 2023 at 17:59):Because when you said that I wasn't calling Coq to step through a file, I tested and the output log doesn't changed.
Paolo Giarrusso (Jan 25 2023 at 18:03):Slight correction then: you did ask, but vscoq isn't trying for some reason...
Uh, is it possible the key combos are different? can you right click late in the file, then click onto "interpret to point"?
image.png
If that doesn't work, then hopefully there are logs about VsCoq under the "Extension Host" tab
Paolo Giarrusso (Jan 25 2023 at 18:03):(that screenshot is from a Mac)
Maxime Dénès (Jan 25 2023 at 18:19):@Gabriel Mazieri Just in case, what version of vscode do you have?
Gabriel Mazieri (Jan 25 2023 at 18:29):My vscode version are currently 1.74.3
Gabriel Mazieri (Jan 25 2023 at 18:31):Paolo Giarrusso said:
Slight correction then: you did ask, but vscoq isn't trying for some reason...
Uh, is it possible the key combos are different? can you right click late in the file, then click onto "interpret to point"?
image.pngIf that doesn't work, then hopefully there are logs about VsCoq under the "Extension Host" tab
This option doesn't appear for me when I try to right click on the line i want to proof assist
Gabriel Mazieri (Jan 25 2023 at 18:32):And also the extesion host shows this message:
2023-01-25 15:31:56.062 [info] ExtensionService#_doActivateExtension maximedenes.vscoq, startup: false, activationEvent: 'onCommand:extension.coq.stepForward'
Paolo Giarrusso (Jan 25 2023 at 20:25):This option doesn't appear for me when I try to right click on the line i want to proof assist
Interesting. Is that file named .v, and is it in Coq mode? See Coq in:
image.png
Paolo Giarrusso (Jan 25 2023 at 20:26):looking at the extension host log, I'm finding
2023-01-25 13:27:17.862 [info] ExtensionService#_doActivateExtension maximedenes.vscoq, startup: false, activationEvent: 'onLanguage:coq'
which (I guess) means "here's a file in Coq mode"
Gabriel Mazieri (Jan 25 2023 at 20:51):Paolo Giarrusso said:
This option doesn't appear for me when I try to right click on the line i want to proof assist
Interesting. Is that file named
.v, and is it in Coq mode? See Coq in:
image.png
It wasn't in Coq mode, wow, unbelievable.
I can proof assist now
The auto detect of vscode didn't changed automatically when editing a .v file
i had to manually change the language mode
Thanks for helping me Paolo, Karl and Maxime.
Gabriel Mazieri (Jan 25 2023 at 20:52):Everything works perfectly now
Maxime Dénès (Jan 25 2023 at 20:52):Sorry for not helping more, it is the first time I hear about this particular problem.
Maxime Dénès (Jan 25 2023 at 20:52):Glad you could fix it!
Paolo Giarrusso (Jan 25 2023 at 22:55):@Gabriel Mazieri out of curiosity, does auto-detect work now, and if not what does it pick? Any chance it picked something like _Verilog_? That also uses the .v extension. (Otherwise, no idea)
Gabriel Mazieri (Jan 25 2023 at 22:58):Once I open vscode it auto-detects to V mode instead of Coq mode.
Gabriel Mazieri (Jan 25 2023 at 23:00):But when I do it once, it stays on Coq mode.
Gabriel Mazieri (Jan 25 2023 at 23:01):I don't see any _Verilog_ in any place
Paolo Giarrusso (Jan 26 2023 at 00:08):Sounds like you might have another plugin for V files so the problem makes sense, but what's V mode?
Gabriel Mazieri (Jan 26 2023 at 00:14):
Here at the bottom right on vscode there is this "Language Mode"
That's why I said "V Mode" because V was automatically selected by vscode once he found that I was editing a .v file
Now I've changed to Coq and the proof assistant looks to work properly.
Paolo Giarrusso (Jan 26 2023 at 00:23):Yeah thanks for your patience! I was curious if there's something VsCoq should do, but no idea for now. We'll keep it in mind, and if it happens again at least we'll know and we might dig more.
Gabriel Mazieri (Jan 26 2023 at 00:29):Yeah, I feel kinda dumb for not looking to the most obvious place in vscode... but, anyways, thanks alot everyone. :hearts:️
Last updated: Jun 04 2023 at 23:30 UTC