Download the gzipped tar file pXx_pvslib-full.tgz into the PVS installation directory, e.g, <pvsdir>. Then execute
tar xvfz pXx_pvslib-full.tgzThe NASA libraries will be installed in the subdirectory lib, along with the standard PVS libraries.
You will still have to add the following to your .pvsemacs file
(load-prelude-library "<pvsdir>/lib/Field")if you do not want to issue Emacs command M-x load-prelude-library manually for each new directory you work in.
Note: Since PVS 3.0, it is no longer necessary to use LIBRARY statements in your PVS specifications. The new PVS_LIBRARY_PATH environment variable 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 variable and the subdirectory <pvsdir>/lib. The variable PVS_LIBRARY_PATH is a list, so libraries can be stored in multiple places.