PVS Snapshots

These snapshots are freely available, but the Allegro versions require a license agreement. If you have ever done the "click-through" license on the PVS Download page by downloading an earlier version of PVS, you don't need to do it again. Otherwise, follow that link, choose an Allegro version, and click "I Accept" at the bottom of the license page. You can interrupt the download, if you don't actually want that file.

Note: if the above link is down, read the LICENSE and make sure you agree to its terms before downloading an Allegro version.

The SBCL versions are under GPL, no need for a click-through.

Windows users can use virtualbox or vmware and run it in Linux under that. PVS was developed under Ubuntu 16.04, but it shouldn't matter which recent Linux (or even BSD) is used.

Before installing PVS, make sure you have Emacs installed. Under Linux, use your package manager ("sudo apt install emacs" for Ubuntu).

For Mac, the default Emacs (/usr/bin/emacs) works, but it's old, and doesn't support window displays. You actually need to use the -nw flag to use it with PVS. It's better to install a newer Emacs: GNU Emacs or Aquamacs work with PVS (search for these). But you must then set PVSEMACS to point to the right emacs. It's not enough to put, e.g., GNU Emacs, in your path, because the executable is named "Emacs". PVS invokes "emacs", not "Emacs", and though Mac is case-insensitive on files, this doesn't hold for commands (it will skip past "Emacs" and find the older "emacs"). Shell aliases for emacs also won't work, as PVS is run from a shell script, which ignores aliases.

After installing Emacs, untar the PVS tar file, which will create a pvs-7.0.NNN subdirectory. cd to it, and run ./install-sh. It's a good idea to add the pvs-7.0.NNN directory to your path, but not necessary.

It's fine to move the PVS directory, or change PVSEMACS or the path for "emacs", at any time, but you must rerun ./install-sh.

tree v1.8.0 © 1996 - 2018 by Steve Baker and Thomas Moore
HTML output hacked and copyleft © 1998 by Francesc Rocher
JSON output hacked and copyleft © 2014 by Florian Sesser
Charsets / OS/2 support © 2001 by Kyosuke Tokoro