* Installing PVS

Installation is relatively simple:
Create a new PVS directory (name doesn't matter), cd to it, untar
the files, run 'bin/relocate', and you should be able to run
'./pvs'.  Copy this script to a directory in your path, or add the
PVS directory to your path.

* Building PVS

PVS is open source, get the latest sources using subversion:

svn checkout https://spartan.csl.sri.com/svn/public/pvs/trunk pvs

The build process is described below, please feel free
to contribute your own experiences.

Note: most users do not need to build PVS, prebuilt images are already
available on the http://pvs.csl.sri.com/download.shtml page. Even
modified sources can easily be incorporated into a built image, using
~/.pvs.lisp (or simply using the load function). However, if you wish to
port to another lisp, or explore different kinds of optimizations, etc., you
will need to build it yourself. Hopefully it will not be too difficult.

In summary, the steps you need to take are: 

* Obtain and install Common Lisp 
* Get the PVS sources 
* Set the ALLEGRO_HOME, CMULISP_HOME, and/or SBCLISP_HOME
  environment variable(s) 
* Run configure and make

Obtaining and Installing Common Lisp
------------------------------------

PVS currently works with Allegro Common Lisp, which is proprietary ($$$),
SBCL, and CMU Common Lisp, which are open source. PVS is roughly twice as fast
with Allegro, so if you already have Allegro, or have extra money, it is
preferred. In addition, the Intel Mac is not supported by CMU Lisp. You can
get Allegro from franz.com. PVS works best with Allegro 8.2, and probably
won't work at all for versions before 6.0.

SBCL and CMU Lisp are free. Note that you can build them from source,
but it's not necessary (and apparently it is not easy).

Install as directed by these sites. 

Get the PVS Sources
-------------------

Get them from the download page, create a directory, cd to it, and untar the
sources.

Set either the ALLEGRO_HOME, SBCLISP_HOME, and/or CMULISP_HOME environment
variable.  If using SBCL, you may need to chmod a+x <sbcl>/run-sbcl.sh

----------------------------------------------------------------

For Allegro, set ALLEGRO_HOME to the directory containing the license file
(devel.lic). For CMU Lisp, set CMULISP_HOME to the directory containing the
bin subdirectory.  SBCLISP_HOME is the directory containing run-sbcl.sh

Note: if you have multiple lisps, you can set all desired variables and the
make will create all images.

Run ./configure and make

Configure should be straightforward. Note you generally need to run it only
once, even if you are building for many platforms.

Make may cause some problems, we had some issues with getting the right GCC
versions, especially for Mac and Solaris. If you have problems and/or
solutions, please let us know
