search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
337 stars 69 forks source link

How does the proof progress side window open? (not open despite vscoq enabled) #193

Closed brando90 closed 1 year ago

brando90 commented 3 years ago

How does the proof progress side window open? (not open despite vscoq enabled)

TheoWinterhalter commented 3 years ago

Did you try to "step" in the file? You can open the command palette and do "Coq: Interpret to point" for instance. Please just look at the commands beginning with "Coq:".

brando90 commented 3 years ago

Did you try to "step" in the file? You can open the command palette and do "Coq: Interpret to point" for instance. Please just look at the commands beginning with "Coq:".

it is asking me for a path to Coq...why doesn't it find it automatically?

brando90 commented 3 years ago

Did you try to "step" in the file? You can open the command palette and do "Coq: Interpret to point" for instance. Please just look at the commands beginning with "Coq:".

is it possible for vscode to go to the proof step automatically on its own?

TheoWinterhalter commented 3 years ago

It should find a path to Coq automatically. How have you installed Coq? And have you restarted vscode after installing it?

And what do you expect it to do automatically? It will interpret the part of the file you tell it to. There are keystrokes to do those though. The command palette will tell you what they are.

brando90 commented 3 years ago

It should find a path to Coq automatically. How have you installed Coq? And have you restarted vscode after installing it?

And what do you expect it to do automatically? It will interpret the part of the file you tell it to. There are keystrokes to do those though. The command palette will tell you what they are.

It found it after a couple of restartings and re-installings...not sure what went wrong.

Apologies if I was not clear. I come from Isabelle, where I am used to JEdit to automatically verify where my cursor is and automatically show me the proofs states (I never have to press anything for it to do it as I am seeing Coq in vscode needs).

Thanks for your time Theo.

TheoWinterhalter commented 3 years ago

I guess that's because, Coq takes processing time to compile something, maybe more than Isabelle. I'm not very familiar with it so I can't really say. On macOS, I just have to press Ctrl + Alt + Right to get to my cursor and Ctrl + Alt + Down to go one step further but I don't remember the Linux and Windows keybindings.

brando90 commented 2 years ago

hmmm... this is weird. I got a new computer and trying to get vscoq to work but it still doesn't find the coq path automatically despite closing and opening vscode. I def have coq installed:

(iit_synthesis) brandomiranda~/coq4brando ❯ coqc -v
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.12.1

why isn't vscoq finding it @TheoWinterhalter?

brando90 commented 2 years ago

related: https://stackoverflow.com/questions/71343424/how-to-tell-vscode-where-coq-is-fixing-could-not-start-coqtop-coqtop