Building PVS

From SRI PVS
Revision as of 10:59, 27 April 2011 by Kiniry (Talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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 download 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

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 it, or have extra money, it is preferred. In addition, the Intel Mac is not supported by CMU Lisp. You can get it from franz.com. It 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 gets a hardware error for me. Let me 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.

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.

Known Problems and Solutions

ld: cannot find -lbsd

Fix: Simply erase the -lbsd from BDD/ix86-Linux/Makefile.

libbsd is a compatibility library, which seems no longer being needed. It is not provided on Debian and it is empty on Fedora Core.


Error in KERNEL::UNBOUND-SYMBOL-ERROR-HANDLER: the variable | is unbound

This happens with GNU make 3.81, for instance in Debian Etch. It is cause by an incompatible change about continuation lines within single quotes.

Fix: Apply this patch (PVS 4.0, PVS 4.1), and ./configure again.
patch Makefile.in pvs-4-X-patch-makefile-quote

Personal tools