Open fblanqui opened 1 year ago
Hi, thank you for your feedback!
Hope this helps. Thanks! -Paolo
Ok, if you typecheck that version of the helloworld example you should see 2 TCCs generated in Workspace Explorer, see screenshot below
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.
Another problem I just got is: when I click on prooflite, vscode freezes and I need to kill it.
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.
Hello. Here are remarks about the tutorial:
~\Workspaces
with a backslash, but it is~/Workspaces
with a slash on Linux systems