Is VSCode-PVS functional?

[Peter Gumm]

Hi,

 I have been trying to install the PVS extension for VS-Code. 

Unfortunately the system gets stuck while 

"Checking PVS versions from www.csl.sri.com"

"Source: PVS(Extension)"

How to proceed now? 

H. Peter 

[Paolo Masci]

Hi Peter,

It might be a temporary problem with the SRI server.

If the installation keeps failing from vscode-pvs, please try the following:

Manual installation of PVS: Download PVS Allegro v7.1.0 for MacOS or Linux and follow the installation instructions reported in the INSTALL file included in the downloaded package. Once PVS is installed on your machine, you can link up PVS and VSCode-PVS by indicating the location of the PVS executables in the VSCode-PVS settings.

If the problem persists, please let us know.
Thanks,
Paolo

[Peter Gumm]

Hi Paolo,

after my initial frustration, I did what you suggested - first installed pvs, then VSCode-PVS.

I am absolutely thrilled! So far it works wonderfully. This is what I had wanted for a long time:  PVS with a decent user-interface. 

Before, I had always hesitated using PVS in my classes on formal methods, because most students had too many hurdles to overcome: Linux + Emacs + PVS + HOLogic/Type theory. If VSCode-PVS holds to its promise, it saves them a lot of time and a lot of frustration. I'll give them a preconfigured virtual box and all is fine. Thanks for the great work. If I do not experience any major setback within the next few weeks, I will definitely use it in my class this coming summer semester - beginning April 12. 

For a while I had played with the "ProofNavigator", which is another excellent user interface for a PVS-like language by Wolfgang Schreiner at RISC Linz in Austria. It is pretty mature and has many features that are  very nice and would make very strong enhancements for VSCode-PVS. In particular I am thinking of the suggestion feature: If you hover over a formula in a sequent, it displays a menu at the mouse cursor, listing those commands that are reasonable to use on the current formula/sequent. Instead of typing an (rather old-fashioned) LISP-Style command, you just select one of the menu entries. I believe this could be easily accomplished in VSCode-PVS, too. 

A  .ova-virtual machine is available at https://www3.risc.jku.at/research/formal/software/ProofNavigator/. The whole thing is now part of their Program-Explorer: https://www3.risc.jku.at/research/formal/software/RISCAL/

I wish they would have joined forces with you at NASA. It might make the RISC side more powerful and the NASA side more modern, more attractive and easier usable.

Greetings, Yours

H. Peter