This file describes how to install the SVRC Ergo theorem prover.

Ergo is implemented using Qu-Prolog, so you must have installed
Qu-Prolog before you can run Ergo.  In particular, the Qu-Prolog
abstract machine emulator 'qem' must be available for Ergo to run.

Installation of Ergo
====================
The minimal steps to install Ergo are (these instructions use the
word 'ROOT' to mean the absolute path to the directory containing
this INSTALL file):

1) run the install.ergo shell script in this directory.

   Eg.     ./install.ergo

   After you have successfully executed this script, you can
   execute Ergo by typing ./bin/ergo.  If this produces errors,
   you might like to add the -V (verbose) flag:  

	./bin/ergo -V

   This will cause Ergo to print out the full path of every file that
   it tries to access.  This often helps to determine which installation
   variables are set incorrectly, or which files are missing. 

   You may wish to print the Ergo User Manual.  It is available
   as a DVI file in './userman/ergo.dvi'.

The following installation steps are optional.

2) If you wish to install the hypertext help facility of Ergo, which
   accesses the Ergo user manual using a hypertext reader (emacs or info)
   edit ROOT/bin/ergo_help (the help shell script) as follows:

      * edit ERGOINFO to point to ROOT/userman

      * edit SYSINFO to be the colon separated list of directories
        that contain .info files on your system.

3) If you wish to install the Emacs19 interface to Ergo, follow the
   following instructions.

   The ROOT/emacs subdirectory contains two Emacs lisp files that define
   an Emacs19 mode for interacting with Ergo.  To use these, edit the paths
   in ROOT/emacs/ergo.el that start with /homes/... to the appropriate
   paths for your system, then add (load "ROOT/emacs/ergo") to your
   $HOME/.emacs file.  Future Emacs sessions will then go into 'ergo'
   mode whenever you edit a file with an extension of '.thy'.
   Type ^H-m (Control-H followed by m) to get help on what commands
   are available in the ergo mode.


Questions and Bug Reports
=========================
As noted in the COPYRIGHT file, Ergo is unsupported software.
However, there is a mailing list set up for Ergo users:

	  ergo@cs.uq.oz.au 

This will be used for announcements about new releases etc. and
should also be used by Ergo users for queries and error reports.
Error reports will be recorded by the Ergo maintainers and queries
may be answered by the Ergo maintainers or by other users.

To join this mailing list, please send a request to ergo@cs.uq.oz.au.

