INSTALLING PVS To install, simply create a new directory, cd to it, untar the files, and run ./bin/relocate to set the path. Then run ./pvs, which should start up a new Emacs window running PVS. After running bin/relocate, the pvs shell script may be copied or linked to a different directory. However, if the PVS directory is moved, ./bin/relocate must be rerun. If you have already signed a license for PVS, you do not need to sign a fresh one for later releases. If you obtained the system by anonymous ftp, or by some other means that did not require you to sign the License Agreement beforehand, gunzip and print out the file license.ps.gz, read it, have it signed by someone who can legally bind your institution, and return it to SRI. Licenses are available to individuals as well as corporations and universities. General Remarks: Emacs: PVS uses GNU Emacs as its interface; you need GNU Emacs or XEmacs version 20 or later to get all the features of PVS; earlier versions of Emacs generally work adequately, but some PVS capabilities will be missing. The Emacs command M-x emacs-version will tell you what version of Emacs you have installed at your site. GNU Emacs is available by FTP from a number of sites (such as prep.ai.mit.edu) or from the Free Software Foundation. XEmacs is available from ftp://ftp.xemacs.org/pub/xemacs. Tcl/Tk: Some PVS functions make use of Tcl/Tk. To use these functions, you must have Tcl/Tk (versions 7.3/3.6 or later) installed at your site, and the "wish" executable must be on your path. Type "wish" to a shell to check that this works; then type "info tclversion" and "set tk_version" to the % prompt to check the versions. Ctrl-c to exit. You can get Tcl/Tk from ftp.scriptics.com. LaTex: To make use of the PVS LaTeX and alltt output commands, LaTeX must also be available. A LaTeX previewer must be available for the latex-theory-view command. Type "latex" to a shell to make sure this is available ("\bye" and "x" to quit). The previewer is likely to be called "xdvi". You can get TeX and LaTeX stuff from any CTAN archive. (Point a WWW browser at ftp://ftp.cdrom.com/pub/tex/ctan/) If you have questions or suggestions, send email to pvs-bugs@csl.sri.com. To get on the PVS mailing list, send a message to pvs-request@csl.sri.com. We hope you find PVS useful and fun.