Installing Hypatheon Version 1.2 18 Feb 2016 ------------------ 1. Required Software The Hypatheon database application runs on Unix/Linux and Mac OS X (Darwin) platforms using commonly available open-source packages. These include Python, Tcl/Tk and SQLite. Hypatheon does not support the SBCL and CMUCL versions of PVS. Users without an Allegro version of PVS are limited to the no-PVS configuration described below. Hypatheon has been tested on OS X and Fedora Linux distributions. 2. Installation with the NASA PVS Libraries If you have a recent nasalib distribution, it includes Hypatheon and a pre-built database file, giving you a database consistent with the latest libraries. Hypatheon software resides in a subdirectory of the nasalib collection. The installation script must be invoked from a running PVS instance. Make sure that this instance is configured for your normal, everyday PVS usage so that the script inherits the PVS-relevant environment variables, especially PVS_LIBRARY_PATH. All libraries you expect to need should be reachable from the directories on PVS_LIBRARY_PATH. 2.1 Installation Procedure From the PVS Emacs interface, issue the command M-x load-file, supplying this file name: /nasalib/Hypatheon/hyp-install.el The installation script will run, sending its output to the Emacs buffer *hyp-install*. Scan it to make sure there were no errors. The installer checks for required software and creates additional scripts to place in your home directory. It will start Hypatheon in stand-alone mode as a test. To enable Hypatheon for PVS-client mode, the file '.hypatheon-emacs' will be copied by the installer to your 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 Hypatheon, edit the .pvsemacs file manually as needed. 2.2 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 installer 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'. The script 'hypfind' is also available for issuing queries from the command line. If all is working well, you may ignore the remaining instructions. 3. Installation 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.2-nasalib-6.1.tgz). Unpack this tar file into a directory D using the command tar xfz Hypatheon-1.2-nasalib-6.x.y.tgz to create the directory /Hypatheon-1.2. An optional script is provided to check for required software. To use it, change directory (cd) to /Hypatheon-1.2 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.2/bin/launch_client You may now issue queries as desired. Ignore the remaining instructions. 4. Other Installation Methods 4.1 Pre-built Database Files Links to pre-built database files can be found at the Hypatheon web page (http://shemesh.larc.nasa.gov/people/bld/hypatheon.html). Each 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 directory /Hypatheon/data/ or any directory found in PVS_LIBRARY_PATH. 4.2 Custom Installation 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.2.tgz). Change directory (cd) to a directory D of your choice and unpack the Hypatheon distribution using this command: tar xfz /Hypatheon-1.2.tgz Unpacking will create the subdirectory /Hypatheon-1.2. Add a symbolic link in directory D: ln -s Hypatheon-1.2 Hypatheon Proceed to retrieve a pre-built database file, if desired. Make sure your PVS_LIBRARY_PATH includes a path for D, then follow the 2.1 Installation Procedure above, using D-path instead of nasalib. 5. Missing Software Hypatheon relies on standard software found on nearly every Unix-based platform. This includes 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. It is unlikely you will need to install any of these packages. If, however, the installation script determines that your platform is missing some of them, 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 Current OS X distributions include Python 2.7, which is preferred. Pysqlite might be missing from the Python suite that ships with earlier versions of OS X. 6. 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' by default.) 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 carry out the Installation Procedure as described above in 2.1. The installation 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. 7. Upgrading Hypatheon If you use the NASA PVS library collection, you will receive updates to Hypatheon automatically when you refresh the libraries. Performing the installation procedure again should be unnecessary, provided the same location is used (normally /nasalib). If the path name has changed or there is a new version of PVS, then reinstallation should be performed. To upgrade to a newer version if you are not using the NASA libraries, 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. -----------