PVS 8.0 (beta) is now available for installation, see below for details.
PVS releases are generally available with Allegro Common Lisp or SBCL. Current versions are for Linux and MacOSX 64-bit machines. If you have other platforms, you may be able to use Vagrant with a Linux version, use an earlier release, or contact us at pvs@csl.sri.com to discuss possibilities.
Vagrant: any operating system that supports Vagrant and Virtualbox (e.g., Windows) should be able to run PVS 7.1 or later. Simply download a Linux version of PVS, untar it, and follow the instructions in vagrant.README.
For versions 7.1 and below, we strongly suggest getting a pre-built Allegro version, unless you have concerns with the Allegro runtime click-though license, in which case get one of the SBCL Lisp images.
PVS 8.0 is now available for SBCL. Tar files are not currently being provided, because it is difficult to make images that work in all Unix-like environments. Instead, it is easiest to simply build it on your system. Here are the instructions.
At this point, you should be able to run ./pvs, which will start Emacs and show the PVS Welcome page. Let us know at pvs-bugs@csl.sri.com if you run into problems.
If you want NASA's PVS library for this version, please use the following:
git clone https://github.com/nasa/pvslib/tree/v8.0
Put it anywhere you prefer, and add it to your PVS_LIBRARY_PATH.
Note that the sources include a Dockerfile, which can be used to build a Docker container for use in Windows. The basic instructions are in the Dockerfile itself.
In PVS Version 7 and later, simply untar the file where you want, and a subdirectory will be created for you. For earlier versions you should create a subdirectory, cd to it, and untar from there.
Then read the INSTALL file to finish installation.
In general, the Allegro version is faster, but does require agreeing to a click-through license for Allegro, also included in the tar file as LICENSE-SRI. The PVS sources are under GPL.
