[pre-release] vscode-pvs-1.0.53-delta

20 views
Skip to first unread message

Paolo Masci

unread,
Jun 13, 2021, 8:49:26 PM6/13/21
to PVS verification system
A pre-release vscode-pvs-1.0.53 is available at the following link:
https://drive.google.com/file/d/1ntiHLTV0AWz_Qk3TW1B9FwEAi-PcwoCL/view?usp=sharing

This pre-release introduces the following changes:
* Design change for auto-completion in the prover prompt: "Space" autocompletes math symbols.
* Fix for F4/F5 shortcuts in the prover session
* Fix for intermittent bug resulting in blank display shown when starting a prover session
* Design change for error messages in the prover console: when incorrect prover commands are entered at the prover console, the console shows an error message without re-displaying the (unchanged) sequent
* Design change for file explorer: ADT files are now visible in file explorer

Our current tests indicate that everything is ok with this pre-release
- If you try out the pre-release, your feedback would be welcome!
- If no major issue is found within the next 2 days, the pre-release will be published on the VSCode marketplace as version 1.0.53

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

Paolo Masci

unread,
Jun 14, 2021, 5:28:38 PM6/14/21
to PVS verification system
I have introduced some minor changes in the pre-release:
- improved rendering of the tooltip in the prover console
- case-sensitive autocompletion in the prover console

The updated .vsix file is vscode-pvs-1.0.53-epsilon.vsix, and is available at the following link:


Paolo Masci

unread,
Jun 16, 2021, 11:35:12 PM6/16/21
to PVS verification system
Some additional changes before the final release:
- added interlock mechanism in prover console, to disable user input while the prover is busy executing a command
- added new vscode-pvs setting for enabling/disabling the use of Enter as alternate autocompletion key in the prover console
- re-enabled inline tooltips showing sequent formulas in proof-explorer, when hovering the mouse over proof nodes

The updated .vsix file is vscode-pvs-1.0.53-theta.vsix, and is available at the following link:
Reply all
Reply to author
Forward
0 new messages