******************************************** 
* KeY Source Code Installation             * 
* Version 0.99.2                           *
********************************************


(1) Requirements: 
-------------------------------------

Operating System: Linux/Unix 

Java 2 SDK, Version 1.4.x or newer (already installed)

For optional UML/OCL support: Together Control Center, Version 6.2 
                                                      (already installed)

Needed additional Libraries:
	antlr.jar Version >= 2.7.2: parser generator
	javacc.jar Version >= 3.0 : parser generator
	dresden-ocl-demo.jar: ocl parser
	xerces.jar version 1.4.4: used by tudresden.jar
	recoder.jar version 0.73KeY: a transformation framework for java
			             patched by KeY
	junit.jar version 3.8.1: test framework
	jargs.jar
	log4j.jar

Optionally, KeY can make use of the following binaries:
	ESC Java's decision procedure `Simplify´
	Grammatical Framework

(2) Contents of the KeY-Distribution
-------------------------------------

  At the KeY-Homepage you can find the following parts:

   * README.xxx-src.txt: this file

   * KeY-xxx-src.tgz: the source code version of KeY-system
   * KeYExtLib_xxx.tgz: contains the external libraries
   * quicktour_xxx.ps.gz: a short tutorial
   * KeYDemo_xxx.tgz: example for KeY used in the tutorial


(3) Installation (Source Code)
-------------------------------------

	1) Untar the tar-gzipped file:

		tar -xvzf KeY-xxx-src.tgz

	2) Change to the created directory key-xxx

		cd key-xxx

	3) Install the needed libraries. Use the environment variable
           $KEY_LIB to point to the directory the needed libraries are
           in. If you use csh and all the needed libraries are in
           ~/key_lib use, e.g.

				setenv KEY_LIB ~/key_lib


	4) Optional (for UML/OCL support only): Tell the system where
	   the Together Control Center installation is. Do this by
	   setting the environment variable TOGETHER_HOME, e.g. (using
	   csh and Together in ~togetherj/vers6.2/linux) by
	
			setenv TOGETHER_HOME ~togetherj/vers6.2/linux


	5) (This step is only necessary if you want to make use of the
	    authoring tool Grammatical Framework and/or the decision
	    procedure Simplify.)

           If you download Simplify not from the KeY-website but
           elsewhere e.g. directly from Compaq (as part of ESC/Java)
           follow the intallation instructions given there. Then
           rename the Simplify binary which could be named something like
           Simplify Simplify-1.5.4.linux (Linux version) or 
           Simplify-1.5.4.exe (Windows) to just 'Simplify' resp. 
           'Simplify.exe'. When using Linux make sure that the file is
           is executable (you can make a file executable by issuing the
           command 'chmod a+x filename').

	   Make sure that the path where the binaries `Simplify´ and
	   `gf´ (Grammatical Framework) reside is included in your PATH
	   environment variable or in the KEY_LIB environment
	   variable. If not, use (e.g., in the csh to include Simplify
	   which is assumed to be located in ~/simplify):

		setenv PATH ~/simplify:$PATH

           In bash-syntax the above command is
       
                export PATH=$PATH:~/simplify


	6) Change to the subdirectory ./system

		cd system

	7) Compile KeY:

		 make all (or gmake all)

	   As standard Java compiler `jikes´ is the default. If you
	   want to use javac as compiler please use

	     	make JAVAC=javac all

           If you do not have Together, please use one of the
           following:

                make keybase
                make JAVAC=javac keybase 
	

(4) Start KeY 
-------------------------------
	
	Assuming you are still in the `system´ directory, run:

		../bin/startkey

	TogetherCC with the KeY extensions should then start up.

	For using the KeY prover standalone use:

		../bin/runProver


If you encounter problems please send a message to

		support@key-project.org