INSTALLING the PVS2.2 System Connect to our web site at http://www.csl.sri.com/pvs.html or use ftp to access ftp.csl.sri.com:/pub/pvs/ Download the files pvs-system-2.2.tgz - mandatory pvs-sunos-2.2.tgz \ pvs-solaris-2.2.tgz \ Choose one or more pvs-linux-2.2.tgz / according to platform(s) pvs-aix-2.2.tgz / pvs-doc-2.2.tgz - optional pvs-libraries-2.2.tgz - optional Create and cd to a new directory, and unpack the downloaded files. To unpack, use one of, e.g., 1. tar -xzf pvs--2.2.tgz 2. zcat pvs--2.2.tgz | tar -xf 3. gunzip pvs--2.2.tgz; tar -xf pvs--2.2.tar The method varies according to the version of tar and other utilities available on your system. See your systems administrator if none of these work for you. After all files have been untarred, type ./bin/relocate, which updates the location of PVS in the startup script. Then run ./pvs, which should startup a new emacs window running PVS. The pvs shell script may then be copied or moved to a directory in your path, but if the directory is moved, be sure to run bin/relocate again. If you have already signed a license for PVS, you do not need to sign a fresh one for PVS 2.2. 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 Dr DWJ Stringer-Calvert, PVS Licensing, Computer Science Laboratory SRI International 333 Ravenswood Avenue Menlo Park, CA 94025, USA or fax to (+1) 650/859-2844 General Remarks: Emacs: PVS uses GNU Emacs as its interface; you need GNU Emacs version 19.28 (or later) or XEmacs version 19.13 (or later) to get all the features of PVS 2.2; 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. It's strongly suggested that you upgrade from GNU Emacs version 18, but if you insist on using it, you will need to download the pvs-ilisp18.tgz file and unpack it as explained above. Tcl/Tk: Some PVS 2 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.