# ===============================================================
# This document tells you how to install MathServe from the sources
# on a state-of-the-art Linux machine.
# @author Juergen Zimmer, Saarland University, Germany
# @version $Date: 2006/05/26 14:04:57 $ $Revision: 1.9 $
# ===============================================================

# MathServe is a Java application so you have to install the Java 
# Development environment (Version 1.4.2). Please use the one 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 <where-ever-it-is>/j2sdk1.4.2
setenv JDK_HOME ${JAVA_HOME}
setenv PATH ${JAVA_HOME}/bin:${PATH}

# --------------------------------------------------------
# To compile MathServe you also need the ant build tool, available at 

  http://ant.apache.org/

# and you have to set ANT_HOME, so, for instance:

setenv ANT_HOME  <where-ever-it-is>/apache-ant-1.6.2
setenv PATH ${ANT_HOME}/bin:${PATH}


# --------------------------------------------------------
# Best put your MathServe installation on a disk with more space
# because it's rather large (60MB). 
# Make a directory, however you may call it,  and cd into it. For instance:

mkdir MathServe
cd MathServe

# To get the CVS sources anonymously you do:

cvs -d:pserver:anonymous@cvs.ags.uni-sb.de:/CVS/mathserve login

# password is omega


# Or alternatively, if you have an account with write access, do:

cvs -d:pserver:${USER}@cvs.ags.uni-sb.de:/CVS/mathserve login

# password: ask me


# Now you can checkout your sources.

cvs -d:pserver:anonymous@cvs.ags.uni-sb.de:/CVS/mathserve co .

# or

cvs -d:pserver:${USER}@cvs.ags.uni-sb.de:/CVS/mathserve co .

# --------------------------------------------------------
# Get the third-party software used by MathServe:

${ANT_HOME}/bin/ant update
 
# --------------------------------------------------------
# this should have created some subdirs in ./thirdParty/
ls -l thirdParty

# total 64
# drwxr-xr-x   3 mathweb users 4096 May 17 11:18 atp
# drwxr-xr-x   2 mathweb users 4096 May 17 11:16 CVS
# drwxr-xr-x   4 mathweb users 4096 May 17 11:16 golog
# drwxr-xr-x   5 mathweb users 4096 May 17 11:16 prodigy
# drwxr-xr-x   4 mathweb users 4096 May 17 11:18 swi-prolog
# drwxr-xr-x  10 mathweb users 4096 May 17 11:17 tomcat
# drwxr-xr-x   8 mathweb users 4096 May 17 11:18 TPTPWorld
# drwxr-xr-x   3 mathweb users 4096 May 17 11:17 tramp


# --------------------------------------------------------
# Compile the system. Ignore the warnings produced by the following
# command. The phrase BUILD SUCCESSFUL is important:

${ANT_HOME}/bin/ant copyclasses

# --------------------------------------------------------
# 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/mStart

# 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

# --------------------------------------------------------
# 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 (TSTP) 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 <tstp-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
#------------------------------------------------------------------
# You can start MathServe with an XML-RPC interface 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/mStart -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 lengthy output which port it is using.
# The interface method is called  proveProblemXml and takes two parameters, 
# a string containing a valid TSTP proving problem and an integer for the 
# time limit in seconds.

#      public String proveProblemXml(String tstpProblem, int time)

# 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 <mathserve-home>/thirdParty/TPTPWorld/TPTP/Problems/GRP/GRP001-1.p