Installation Notes for NASA Libraries for PVS 5.0

Download the gzipped tar file p50_pvslib-full.tgz into the PVS installation directory, e.g, <pvsdir>. Then execute

   tar xvfz p50_pvslib-full.tgz  

The NASA libraries will be installed in the subdirectory nasalib. You must set the environment variable PVS_LIBRARY_PATH to the nasalib directory. Depending upon your shell, put one of the following lines in your startup script. In C shell (csh, tcsh, etc):

  setenv PVS_LIBRARY_PATH "<pvsdir>/nasalib"
In Bourne shell (sh, bash, etc):
  export PVS_LIBRARY_PATH="<pvsdir>/nasalib"

Finally, add the following line to the file ~/.pvs.lisp (create it if it doesn't exist):

(load "<pvsdir>/nasalib/pvs-patches.lisp")

Important Remark: Binary Files

In addition to specification and proof files, e.g., *.pvs, *.prf, the distribution file p50_pvslib-full.tgz also includes pre-typed binary files, e.g., .pvscontext and *.bin. These files may cause problems in some architectures. If you prefer to type-check and proof-check the libraries on your computer, you can download the file p50_pvslib-nobin.tgz, which does not include binary files.

The no-binary distribution file is much smaller than the full distribution file. However, in this case, PVS will type-check all library dependencies the first time a theory importing one of the NASA libraries is type-checked. For some libraries, this process may take several minutes. Furthermore, the status of proofs that depend on the libraries may appear as proven but incomplete.

For those reasons, we strongly recommend recreating the binary files if you have installed the no-binary distribution. This can be accomplished by issuing the following command from the directory <pvsdir>/nasalib:

../provethem nasalib.all

Be aware that type-checking and proof-checking the PVS NASA Libraries may take a few hours. However, once this is done, type-checking of theories that use the NASA libraries will be much faster and their proof status will be displayed correctly.

Rick Butler
Last modified: Thu Jan 10 11:35:56 EST 2013