# ===============================================================
# This document tells you how to install MathServe from a binary 
# release package on a state-of-the-art IBM compatible Linux machine.
#  @author Juergen Zimmer, Saarland University, Germany
#  @version $Date: 2006/08/24 13:44:05 $ $Revision: 1.8 $
# ===============================================================

#------------------------------------------------------------------
#                    Preliminaries
#------------------------------------------------------------------
# MathServe is a Java application and you need a Java 
# Runtime Environment (JRE) or the Development Environment (Version 1.4.2)
# available at the Sun Java website. The latter is also available for 
# i386 Linux platforms at 
 
  http://www.ags.uni-sb.de/~jzimmer/j2sdk1.4.2.tar.gz

# should put something similar to the the following commands 
# in your .tcshrc or .bashrc

setenv JAVA_HOME <wherever-it-is>/j2sdk1.4.2
setenv JDK_HOME ${JAVA_HOME}
setenv PATH ${JAVA_HOME}/bin:${PATH}

#------------------------------------------------------------------
#                    Installation
#------------------------------------------------------------------
# Best put your MathServe installation on a disk with some free space
# because it's rather large depending on the available services (but <= 80MB). 
# First, download the binary distribution file from 

http://www.ags.uni-sb.de/~jzimmer/MathServe-<VERSION>-bin.tar.gz

# Replace <VERSION> by the actual version number.
# Gunzip and untar the package which will create a directory MathServe 
# containing all necessary files, including a Tomcat web server. 
# On a Linux platform you do this with

tar xvzf MathServe-<VERSION>-bin.tar.gz
cd MathServe 

# The MathServe directory contains several subdirectories whose contents is briefly 
# described in the README file. 
# We recommend that you put the directory MathServe/bin in your command path.

# --------------------------------------------------------
# Unfortunately, some TPTP Library tools have to be re-compiled on some platforms. 
# To do this execute 

cd thirdParty/TPTPWorld/ServiceTools/
make 
cd ../../../

# --------------------------------------------------------
# Now you should be able to start MathServe with a script in the bin directory of MathServe

bin/tmStart

# if everything went well (wait 3-4 secs) you should see the 
# tomcat web server and the Axis Web Service servlet available in your browser at 

#  http://localhost:8080/
#  http://localhost:8080/axis/servlet/AxisServlet  and 

# respectively. 

#------------------------------------------------------------------
#                    Testing
#------------------------------------------------------------------
# If the server is running you can try to invoke the SPASS service by 

bin/runt org.mathweb.atp.SpassClient

# This calls SPASS on the problem described in the file 

  examples/owl/fof2.owl

# in the MathServe directory. The output you get should look similar to 
# the one shown in the file 

  examples/owl/spass-proof2.owl

# --------------------------------------------------------
# You can also call the MathServe broker directly with a problem formulated in 
# the new TPTP syntax (see http://www.tptp.org/) and a time limit in seconds. 
# The broker analyses the incoming problem and chooses a suitable ATP system for that 
# problem according to performance data on the TPTP Library. 

bin/runt org.mathweb.broker.BrokerClient localhost 8080 proveProblemOpt <tptp-file> <time-limit>

So, for instance, to call the broker on the problem PUZ001+1 in the TPTP library (which is installed 
in your home under TPTP/), you can call

bin/runt org.mathweb.broker.BrokerClient localhost 8080 proveProblemOpt /home/${USER}/TPTP/Problems/PUZ/PUZ001+1.p 10
 
# --------------------------------------------------------
# To kill the web server (and MathServe) type

bin/mStop

# The latter also kills all java processes on the machine, to make sure, the tomcat
# server is really dead. 


#------------------------------------------------------------------
#             XML-RPC interface to the MathServe Broker
#------------------------------------------------------------------
#    THE FOLLOWING FEATURE IS EXPERIMENTAL!
# You can start MathServe with an XML-RPC interface to the broker 
# running on a port, e.g. 12345. 
# This should open an xterm with the server running in it.
# Make sure you have stopped the web server before starting it again.

bin/tmStart -p 12345

# If that port is busy, the XML-RPC server searches for the next free port from 12345 upwards. 
# It tells you at the end of the output which port it is using.
# The interface methods are shown on the AXIS service page at the above URL.

# You can look at 
#    src/org/mathweb/broker/XmlRpcBrokerClient.java 
# for an example
# of how to access the XML-RPC server from Java. You can run the client, e.g.,  with

bin/run org.mathweb.broker.XmlRpcBrokerClient localhost 12345 /home/${USER}/TPTP/Problems/PUZ/PUZ001+1.p 10

where 12345 is the port number of the XML-RPC server.