INSTALLING the PVS 2.3 System Connect to our web site at http://pvs.csl.sri.com/ or use ftp to access pvs.csl.sri.com:/pub/pvs/ Download the files: pvs-2.3-system.tgz - mandatory pvs-2.3-solaris.tgz \ Choose one or more pvs-2.3-redhat4.tgz | according to platform(s) pvs-2.3-redhat5.tgz / pvs-2.3-emacs19.tgz - necessary to support [X]Emacs 19 (if required) pvs-2.3-doc.tgz - optional pvs-2.3-libraries.tgz - optional Note: o the redhat 5 version supports redhat 5.x and redhat 6.x. On a redhat system do "cat /etc/redhat-release" to determine your version. o the default installation supports [X]Emacs 20 and above. If you need support for [X]Emacs 19, you must download pvs-2.3-emacs19.tgz Create and cd to a new directory, and unpack the downloaded files. To unpack, use one of, e.g., 1. tar -xzf pvs-2.3-.tgz 2. zcat pvs-2.3-.tgz | tar -xf 3. gunzip pvs-2.3-.tgz; tar -xf pvs-2.3-.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. NOTE: there may be a message from tar about 'ignoring trailing garbage' - this can be safely ignored. 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.3. 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 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 version 19.28 (or later) or XEmacs version 19.13 (or later) to get all the features of PVS 2.3; 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. PVS 2.3 does not support [X]Emacs 18, and provides support for [X]Emacs version 19 in the file pvs-2.3-emacs19.tgz. Tcl/Tk: Some PVS 2.3 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.