Two issues, one suggestion

[Peter Gumm]

Hi Paolo,

here is an issue that I have had with VSCode-PVS since a long time. 

When I start a proof (by clicking on "prove") above the Lemma, usually

a new tagged window opens with the tag saying "Proving formula ...".

Most of the time, however, this windows remains empty, otherwise, as 

you can see here. 

If I close this window and try it again, I get the same result. Sometimes 

on the third or fourth try, I obtain the desired proof sequent. However if after the first unsuccessful try I keep the (empty) window open then starting "prove" again, the desired proof task displays.

I have had this in the previous version of Ubuntu as well as in the most recent one. 

The behaviour is the same in ll PVS-files, although, there are cases, when the proof sequent occurs in the first try.

This is the bug that I mentioned. 

I frequently make the mistake, trying to complete a keyword or unicode symbol by entering "space"  in VSCodePVS, only with the result that I have to erase the partially written keyword and have to start typing it again from the beginning, for otherwise the menu loses its functionality. 

I would love, if as  a user I could have the choice of using either "space" or "Enter" for keyword-completion. Is that possible, or would that run counter to the VSCode philosophy.

   

Secondly, there may be an issue with the datatype feature of VSCode-PVS. When I create an abstract datatype, then with old style PVS I would do a M-x tc to create an "...-adt.pvs" file. Apparently , this somehow works in VSCode-PVS too. However, I could not figure out how to make the the newly created "..._adt.pvs" file visible in PVS. The way I go currently is: closing VSCode, leaving the Working directory and restarting VSCode on that directory again.  

And finally my "wish in the sky" as a possible suggestion: Regarding the pop-up-menus, offering keyword completion when editing, or command-completion when proving, I am still finding it somehow confusing that I should use the "Enter"-Key to make the choice. 

From other software that I use on Windows I am used to make such choices either 

with the "Space" key or with the "Tab" key. I personally use that a lot when writing LaTeX in Lyx, or doing LaTeX in any of the Windows-Office programs that I use. 

 

 Best regards, Your

H. Peter 

[Paolo Masci]

Thanks for this feedback

- I will look into the issue of the prover console not rendering the content. I've seen it happening sometimes, but could not reproduce the problem consistently. The content and the prompt are ready, but for some reason they are not rendered in the console. If you type a (skip) command followed by Enter in the blank console, you will force a refresh and you should see the sequents.

- I think I can introduce "Space" as autocompletion key, at least in the prover console. I can also add a configuration option so you can choose which keys trigger autocomplete.

- The _adt.pvs files are actively hidden by vscode-pvs to declutter the view. Probably this was a bad design decision, I will update the distribution so the files are visible.

Two additional remarks:

- the autocompletion tooltip is now much smaller and you can view only one hint. The other hints are there but you need to scroll the tooltip to actually see them. This design change has been introduced because the larger tooltip was covering the sequents, and some users complained about this. Feedback is welcome on this.

- your pvs students are welcome to join this google group, and post questions and doubts on both pvs, vscode-pvs, and vscode.

Best,

Paolo

[Michael Harrison]

I find that as soon as I issue a prover command (for example (skosimp*) in the blank screen) the window shows the sequents.

Michael

[Alberto Ercolani]

Also pressing F4 issues an undo and forces the screen to refresh and show the contents.

Alberto

[Paolo Masci]

I have now fixed the problem with the blank console.

I have also implemented (in the prover console) autocompletion for math symbols with "Space", and improved the behavior of autocompletion with "Enter".

A pre-release vscode-pvs-1.0.53-delta with these changes is available at the following link.

https://drive.google.com/file/d/1ntiHLTV0AWz_Qk3TW1B9FwEAi-PcwoCL/view?usp=sharing

I'm making the pre-release available so you are aware that a new version is coming up, and can provide feedback before the new version is published on the VSCode marketplace.

To install the pre-release:
1. Download the .vsix file vscode-pvs-1.0.53-delta.vsix from the link above
2. Click on the Extensions icon in the Activity Bar of VSCode
3. Click on the ... menu in the title bar, and use 'Install from VSIX' to select the downloaded .vsix file

See also https://groups.google.com/g/pvs-group/c/CaWHzWyxSX8 for additional info on this pre-release

 - Paolo