Installation Notes for NASA PVS Library (Version 6.0.9)

The distribution of the NASA PVS Library 6.0.9 comes in 3 sizes nasalib-6.0.9-nobin.tgz ⊂ nasalib-6.0.9.tgz ⊂ nasalib-6.0.9-full.tgz. All the distribution files include the same PVS specification and proof files, i.e., *.pvs and *.prf. The distribution file nasalib-6.0.9.tgz includes everything in nasalib-6.0.9-nobin.tgz and PVS binary files, i.e., .pvscontext and *.bin. The distribution file nasalib-6.0.9-full.tgz includes everything in nasalib-6.0.9.tgz and pre-installed versions of Hypatheon 1.1, MetiTarski 2.2, and Z3 4.3.1.

Installation

The following instructions assume that PVS 6.0 is installed in the directory <pvsdir>/nasalib, i.e., in the instructions below replace <pvsdir> by the absolute path where PVS is installed.

Download one of the distributions file, e.g., nasalib-6.0.9-full.tgz into the PVS installation directory, e.g, <pvsdir>. Then execute

   tar xvfz nasalib-6.0.9-full.tgz  

The NASA PVS library will be installed in the subdirectory <pvsdir>/nasalib. You must set the the environment variable PVS_LIBRARY_PATH such that it points to this directory. Depending upon your shell, put one of the following lines in your startup script. In C shell (csh or tcsh), put this line in ~/.cshrc:

  setenv PVS_LIBRARY_PATH "<pvsdir>/nasalib"

In Bourne shell (sh or bash), put this line in either ~/.bashrc or ~/.profile:

  export PVS_LIBRARY_PATH="<pvsdir>/nasalib"

If you had a previous installation of the NASA PVS Library, either remove the file ~/.pvs.lisp or, if you have a special configuration of that file, remove the line

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

from ~/.pvs.lisp.

Finally, go to the directory <pvsdir>/nasalib and run the shell script

[nasalib]$ ./install-scripts

If you forget this step, you will get errors when using proveit, provethem, or pvsio, e.g.,

Error executing (progn (proveit)): the value of string is nil, which is not of type string.

Full Distribution

If you installed nasalib-6.0.9-full.tgz, visit Hypatheon for instructions on how to use the library search utility.

The full distribution includes pre-installed binaries of MetiTarski 2.2 and Z3 4.3.1 for Mac OSX 10.7.3 and higher and 64-bits Linux. Please, see METIT-LICENSE.txt and Z3-LICENSE.txt before using these pre-installed binaries.

No-Binary Distribution

The no-binary distribution file nasalib-6.0.9-nobin.tgz is much smaller than the other distribution files. When binary files are not available, PVS will type-check all library dependencies the first time a theory depending on the library is type-checked. In some cases, this process may take a few minutes. For this reason, if you installed the no-binary distribution, we recommend recreating the binary files in your computer before using the NASA PVS Library. This can be accomplished through the Unix command typecheck-all, which is avaialable as part of the distribution of the NASA PVS Library. The execution of this command will take several minutes.

The UNIX command typecheck-all doesn't reprove the library. Therefore, if you installed the no-binary distribution of the NASA PVS Library, the status of proofs that depend on the library may appear as proven but incomplete. The whole library can be reproved using the UNIX command prove-all, which is also available in the distribution. Reproving the NASA PVS Library may take a few hours. However, once this is done, the proof status of formulas that depend on the library will be displayed correctly.

Cleaning, Type-checking, Reproving, and Searching the Library

In some cases, it is useful to clean, type-check, or reprove part or the whole NASA PVS Library. As discussed before, the distribution includes the UNIX commands typecheck-all and prove-all for type-checking and reproving the library. It als includes the commands cleanbin-all and find-all for cleaning binary files and for searching the library.

These commands accept several options for selecting a subset of the library for processing. For instance, to type-check the libraries up to the PVS development vectors, the following command can be issued:

./typecheck-all -to vectors 

To re-prove only the PVS developments of ints and reals, the following command can be issued:

./prove-all -do ints,reals

The command find-all finds strings matching a regular expressions in the library. For instance, to find the string "sqrt" in any PVS development after reals (exclusive), type the following command:

./find-all sqrt -after reals

To include the PVS development reals in the search, use the option -from instead of -after. The order in which libraries are processed for all these commands is specified in the file nasalib.all. Please don't modify this file. Furthermore, note that the utility Hypatheon provides a much more sophisticated interface to search the NASA PVS Library.

The tag identifies links that are outside the NASA domain