* 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 now open source. This describes the build process, 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 either the ALLEGRO_HOME or CMULISP_HOME environment variable 
* Run configure and make Contents [hide]

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

PVS currently works with Allegro Common Lisp, which is proprietary ($$$),
and with CMU Common Lisp, which is 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.0, and probably
won't work at all for versions before 6.0.

CMU Lisp is free. Note that you can build CMU Lisp from source, but it's not
necessary (and apparently it is not easy). Also note that PVS has only been
tested with 19c and 19d. Finally, there seems to be a problem with 19d for
powerpc Macs, in that it runs out of heap space for us.  Let us know if you
find a workaround.

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 or CMULISP_HOME environment variable
----------------------------------------------------------------

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.

Note: if you have both lisps, you can set both variables and the make will
create both images.  [edit] 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 add them here.

NOTE: The foreign functions (file_utils, BDD, and WS1S) do not currently
build in 64 bit Linux - you must build these on a 32 bit machine, or modify
them.
