Installing Hypatheon Version 1.1 28 Mar 2013 ------------------ 1. Required Software The Hypatheon database application runs on Unix/Linux and Mac OS X (Darwin) platforms using commonly available open-source packages. It has been tested on OS X and Red Hat family Linux distributions. Hypatheon requires a standard Python suite in the version 2 series (version 2.5.x or later), a contemporary SQLite distribution (version 3.x or later), and the Tcl/Tk GUI toolkit (version 8.4.x or later). Recent versions of Linux include suitable implementations of these as standard software. OS X 10.4 and later should have these components as well. Note that Python now has a 3.x series, which is not supported by the current version of Hypatheon. 2. Running Without PVS Hypatheon may be used without a PVS installation. This might be of interest to non-PVS users who only want to search and browse existing PVS libraries. To create such a setup, first retrieve a copy of the Hypatheon distribution that includes a pre-built database, (e.g., Hypatheon-1.1-nasalib-6.1.tgz). Unpack this tar file into a directory D using the command tar xfz Hypatheon-1.1-nasalib-6.x.y.tgz to create the directory /Hypatheon-1.1. An optional script is provided to check for required software. To use it, change directory (cd) to /Hypatheon-1.1 and issue this command: build/check_nopvs If any problems are reported, see the section below on Missing Software. Otherwise, the Hypatheon GUI interface can be started (from any location) using this command: /Hypatheon-1.1/bin/launch_client You may now issue queries as desired. Ignore the remaining instructions. 3. Choosing a Configuration NOTE: Hypatheon does not yet support the SBCL and CMUCL versions of PVS. Users without an Allegro version of PVS are limited to the no-PVS configuration described above until support is added for other Lisp implementations. Several configuration choices are available for a normal, PVS-aware installation. If you are a user of the NASA PVS libraries, you can retrieve Hypatheon as part of the library collection, which offers the easiest setup process. When you retrieve the libraries they will come with a pre-built database file. This will ensure you have a database consistent with the latest libraries. Hypatheon software will reside in a subdirectory of the library collection. If you have chosen this option, skip ahead to the Installation Procedure section. If you do not use the NASA PVS libraries, or you wish to establish a separate Hypatheon installation, first retrieve the Hypatheon tar file (Hypatheon-1.1.tgz). Change directory (cd) to a directory D of your choice and unpack the Hypatheon distribution using this command: tar xfz /Hypatheon-1.1.tgz Make sure your PVS_LIBRARY_PATH includes a path for D. Unpacking will create the subdirectory /Hypatheon-1.1. Change directory (cd) to , then add a symbolic link in directory D: ln -s Hypatheon-1.1 Hypatheon Now proceed to retrieve a pre-built database file, if desired, then continue with the Installation Procedure. 4. Pre-built Database Files At the Hypatheon web page (http://shemesh.larc.nasa.gov/people/bld/hypatheon.html) are links to several pre-built database files that can be downloaded and used immediately. These databases have indexed the prelude and core PVS libraries as well as the full NASA Langley library distribution. Database files can be placed in /Hypatheon/data/ or any directory reachable from PVS_LIBRARY_PATH. 5. Installation Procedure NOTE: This installation procedure needs to be carried out only once per PVS release. If a new version of Hypatheon is acquired by refreshing your NASA PVS libraries, it should be usable without any additional action on your part. Begin by starting up a fresh instance of PVS, then start an inferior shell within this PVS/Emacs process using the command M-x shell. Make sure that this PVS instance is configured for your normal, everyday PVS usage. In the shell buffer, change to the directory /Hypatheon, then run this script: build/quick_install (If you are using the NASA libraries, will be $PVSPATH/nasalib; otherwise, it is the mentioned above.) The installer checks for required software and creates additional scripts to place in your home directory. It is important that quick_install be run from PVS so that it inherits the PVS-relevant environment variables. Be sure the PVS instance carries a value for PVS_LIBRARY_PATH that will be used during subsequent proof activity. In other words, all libraries you expect to need should be reachable from the directories on PVS_LIBRARY_PATH. The installation script will start Hypatheon in Stand-alone mode as a test. If it comes up and appears to be working, you may restart it in PVS-client mode using the instructions below. First close the Hypatheon window and exit PVS as well. Starting Hypatheon from PVS (to run it in PVS-client mode) requires a simple bootstrapping process. To support this process, the file '.hypatheon-emacs' will be copied by quick_install to the user's home directory. Then the following two lines will be appended to your .pvsemacs file: (load-file "~/.hypatheon-emacs") ;(start-hypatheon-client) ;; uncomment for automatic starting If there are other actions that need to occur after starting up Hypatheon, edit the .pvsemacs file manually as needed. 6. Running Hypatheon Within a PVS instance that was started using the .pvsemacs lines above, issue M-x start-hypatheon-client to bring up the GUI. Alternatively, if the function call (start-hypatheon-client) appears uncommented in your .pvsemacs file, Hypatheon will be launched automatically during the PVS startup phase. For stand-alone operation, run the script 'hypatheon', which the installation script should have created in your ~/bin directory. It can be invoked from the command line simply as 'hypatheon' if ~/bin is on your PATH, otherwise as '~/bin/hypatheon'. 7. Missing Software Hypatheon relies on standard software found on nearly every platform. It is unlikely you will need to install anything else. If, however, the installation script determines that your platform is missing some key software packages, here are some pointers for proceeding. There are several choices for obtaining missing software packages. Besides the standard distributions provided by the developers, there are distributions for Linux available as binary packages (via yum, apt-get, etc.), and for OS X available from Fink, Macports, etc. SQLite is available from http://www.sqlite.org Download page: http://www.sqlite.org/download.html Binaries for Tcl/Tk are available from ActiveState. Download page: http://www.activestate.com/Products/activetcl/index.mhtml Python and Pysqlite are available from http://www.python.org Download page: http://www.python.org/download For OS X users, Pysqlite might be missing from the Python suite that ships with OS X. We recommend upgrading to the Python 2.7 distribution, which includes Pysqlite. Download link: http://www.python.org/download/ 8. Multiple PVS Configurations With most installations, there is only one version of PVS and one version of PVS_LIBRARY_PATH to be concerned with. If, however, you need to work with different versions of PVS or the variable PVS_LIBRARY_PATH, you can do so using different instances of the Hypatheon scripts in ~/bin. (The scripts are named 'hypatheon' and 'hypfind'.) If you refrain from storing working database files in /Hypatheon/data, i.e., you keep them in the directories found on PVS_LIBRARY_PATH, then you can share the /Hypatheon setup for multiple PVS configurations. If you use the Hypatheon scripts in ~/bin, you will need to copy them and adjust the settings for PVS_LIBRARY_PATH. In other cases you will first need to create another copy of the Hypatheon distribution in a suitable directory. Then you can start the alternative PVS in its desired configuration and run the quick_install script as described above. The quick_install script will detect the presence of previously created Hypatheon script files having the standard names 'hypatheon' and 'hypfind'. When found, it creates distinct names for the new scripts by appending a timestamp suffix. Afterwards, you can rename these files by changing the suffix to a meaningful string. 9. Upgrading Hypatheon If you use the NASA library collection, you will receive updates to Hypatheon automatically when you refresh the libraries. No special action on your part should be required. If you are not using the NASA libraries, you will need to do a little more work. To upgrade to a newer version, first close any running instances of Hypatheon. Unpack the new distribution in the same directory as the current version. Change the symbolic link to point to the new version, e.g., rm Hypatheon ln -s Hypatheon-1.2.3 Hypatheon Start the Hypatheon client as you normally do. When it comes up, it will detect the old version and offer you a chance to carry over previous user-preference and database files, to the extent this is feasible. The old Hypatheon directory can be removed once you are confident the new version meets your needs. -----------