Installation Notes For NASA Libraries

The best way to install the NASA libraries is through use of the gzipped tar file that contains all of the bin files, the NASA strategy packages, and the proof contexts (i.e., save the following link):

PVS 4.1 tar file with bins and Manip/Field strategies and PVSio

This can be used to install all of the libraries/strategies at one time.

It is recommended that you install them in the lib subdirectory of your PVS installation directory (i.e. PVSPATH). To do this download the tar file into the main directory (PVSPATH). Then execute

   tar xvfz p41_pvslib-full.tgz

NOTE. IF you use this procedure you will not have to perform the manual installation steps for Manip and/or Field.

You will still have to add the following to your .pvsemacs file

  (load-prelude-library "<pvs-dir>/lib/Field")

if you do not want to issue "M-x load-prelude-library" manually for each new directory you work in.

You must set the the environment variable PVS_LIBRARY_PATH to the "lib" directory (avoid a trailing '/'). For example:

   setenv PVS_LIBRARY_PATH "<pvs-dir>/lib"

   export PVS_LIBRARY_PATH="<pvs-dir>/lib"

depending upon your shell. This can be added to your PVS startup script.

Note: It is no longer necessary to use LIBRARY statements in your PVS specifications. The new PVS_LIBRARY_PATH tells PVS where to look for libraries. The system will automatically search for subdirectory names in all of the locations listed in the PVS_LIBRARY_PATH statement AND the PVS installation lib directory. For example

        IMPORTING reals@sigma,  vectors@vectors_cos

will cause the system to look for subdirectories "reals" and "vectors" to find the "sigma" and "vectors_cos" theories. This path variable is a list, so libraries can be stored in multiple places, however, we favor placing them all in one directory.

Rick Butler

Last modified: Fri Apr 22 08:10:02 EDT 2005