vscode-pvs-1.0.55 pre-release

[Paolo Masci]

A new pre-release vscode-pvs-1.0.55 is available at the following link:

https://drive.google.com/file/d/1_-4K8T9FTT5v1LTbwzwUoo0blmbX7eE3/view?usp=sharing

Please try this pre-release if you have a chance, and provide feedback if you find any problem.

This pre-release introduces the following improvements in the prover console:

- command accelerators for frequent prover commands, e.g,. e+TAB = expand, g+TAB = grind. The full list of accelerators can be found in the vscode-pvs settings, under "Prover Console -> Frequent Commands"

- help *: this command shows a compact list of all prover commands, including a brief explanation of each command and the syntax

- yes-no-cancel dialog: when quitting a proof, vscode will now use a yes-no-cancel question to ask if you want to save the proof, where: yes = quit and save the proof; no = quit and don't save; cancel = didn't mean to quit. (In the previous version, the dialog was simply yes-cancel, where cancel actually meant quit don't save.) 

- improved feedback: the cursor and the integrated help will now show some animation when the console is busy and/or a prover command is being executed.

Note: please save your pvs proofs before using this pre-release. The implementation of the yes-no-cancel dialog required some delicate changes in the server protocol for saving a proof. According to our tests, everything is working as intended. Saving your pvs proofs is just an additional precaution in the case some corner cases escaped our tests.

Thanks,

Paolo

[Paolo Masci]

There's an updated pre-release vscode-pvs-1.0.55-kappa at the following link:

https://drive.google.com/file/d/1Apst0N47XfStGK4BjO8VOFHD4eS6pSIh/view?usp=sharing

The following additional improvements have been implemented:

- *_adt declarations are now visible in workspace explorer

- tooltip in the prover console moved under the command line, so that it does not accidentally cover the command line while entering a command

- commentary line indicating branch completed is now highlighted in prover console, so it's easier to spot

Thanks,

Paolo