Installing Hypatheon Version 1.0 4 Dec 2012 ------------------ 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. 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.0-nasalib-5.8.tgz). Unpack this tar file to create the directory /Hypatheon-1.0. A script is provided to check for required software. Change directory (cd) to /Hypatheon-1.0 and run this script: 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.0/bin/launch_client You may now issue queries as desired. Ignore the remaining instructions. Choosing a Configuration Hypatheon does not yet support the SBCL and CMUCL versions of PVS. Those without an Allegro version of PVS are limited to the no-PVS configuration described above until support is added for other Lisp implementations. NOTE: After the release of PVS 6.0, Hypatheon will be bundled as part of the NASA library distribution. This will be the easiest way to establish a working setup. In the meantime, users will need to install the Hypatheon software distribution, then retrieve a pre-built database file as described below. To install the software, retrieve the Hypatheon tar file (Hypatheon-1.0.tgz) and unpack the distribution into a directory D. Make sure your PVS_LIBRARY_PATH includes a path to D. Unpacking will create the subdirectory /Hypatheon-1.0. Also add a symbolic link in directory : ln -s Hypatheon-1.0 Hypatheon Now proceed to retrieve a database file, if desired, then continue with the Installation Procedure. 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. Installation Procedure 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 The installer checks for required software and creates additional scripts. 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. This installation procedure needs to be carried out only once. If a new version of Hypatheon is acquired by refreshing your NASA PVS libraries, it will be usable without any action on your part. 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', provided ~/bin is on your PATH. Missing Software If the installation script determines that your platform is missing some key software packages, here are some pointers for proceeding. First of all, determine whether they are really missing or merely inaccessible using the current environment variables. If you have upgraded to Python 2.5 or later, for example, and the installation script reports that Pysqlite is missing, it could be that the old version of Python is being invoked instead of the new. If the new Python is reached from /usr/local/bin, try setting the PATH variable to place it first: export PATH=/usr/local/bin:$PATH Alternatively, Hypatheon will recognize an environment variable called PYTHON_BINARY that you can set to override the default version of Python. For other types of missing software problems, there are several choices for obtaining the missing 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/ 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. 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. -----------