Tutorial

Question

Tutorial

Opened this issue 2 years ago · 6 comments

fblanqui commented 2 years ago

Hello. Here are remarks about the tutorial:

https://github.com/nasa/vscode-pvs/blob/master/vscode-pvs/docs/TUTORIAL.md: https://github.com/nasa/vscode-pvs/blob/master/vscode-pvs/docs/README.md is a broken link
it is written ~\Workspaces with a backslash, but it is ~/Workspaces with a slash on Linux systems
vscode-pvs gives feedback very slowly on my machine: fater copy-paste helloworld example, if a replace BEGIN by BEGN, it gets underlined several seconds after (~6-7s); if I replace BEGN by BEGIN, the underlining is removing several seconds after.
with the second example, I do not see any TCC. I can see them only in the 3rd example: in this case, when I click on "prove", vscode displays the PVS workspace explorer on the left.

Answer 1 · 2023-01-03T14:15:54.000Z

Hi, thank you for your feedback!

I will soon push a new version on github that resolves the typos in the tutorial
Regarding the slow feedback on parse errors, the short answer is: to obtain immediate feedback, save the file :)
The long answer is: vscode-pvs parses the file after a timeout or when the file is saved. This is done to implement a "calm" behavior where the tool does not disrupt the user when typing.
Regarding Workspace Explorer, as you noticed the view is automatically opened when you start a proof. You can also manually open the view by clicking the PVS icon located in the side bar.
Regarding the TCCs, you may need to share a screenshot of the example you are playing with, as I don't fully understand which example you are looking at.

Hope this helps.
Thanks!
-Paolo

Answer 2 · 2023-01-03T14:21:28.000Z

fblanqui commented 2 years ago

Answer 3 · 2023-01-03T14:28:17.000Z

Ok, if you typecheck that version of the helloworld example you should see 2 TCCs generated in Workspace Explorer, see screenshot below

Answer 4 · 2023-01-03T14:52:53.000Z

Hi.

Concerning the slow feedback, is it possible to change the timeout?
Concerning TCCs: If I just do code helloworld.pvs from $HOME, and click on typecheck-file, it is said that typechecking is successful but nothing else. However, I have seen afterwards that a file helloworld.tccs is created. Even if I click on this file, I do not get your window. It's only when I add always_positive: THEOREM FORALL (x: real): abs(x) >= 0 and click on prove that I get your window.

Answer 5 · 2023-01-03T14:59:12.000Z

Another problem I just got is: when I click on prooflite, vscode freezes and I need to kill it.

Answer 6 · 2023-01-03T15:34:39.000Z

The timeout cannot be changed at this point in time. I will consider adding an option in settings so this can be customized.

I'll look into the problem you reported for proof lite, at the moment I can't replicate the problem.

For Workspace Explorer, if you click the PVS icon highlighted in the screenshot below you will see Workspace Explorer and the TCCs. Please share the screenshot if you see something different.