******************************************** 
* KeY Source Code Installation             * 
* Version 0.9                              *
********************************************


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

Operating System: Linux/Unix 

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

Together Control Center, Version 6.0, 6.0.1, 6.1 (already installed)

(Remark: Although KeY supports Java2 SDK 1.4, you may have slight
problems running Together 6.0.1 with this Java version.)

Needed additional Libraries:
	antlr.jar Version >= 2.7.1: 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.70KeY: a transformation framework for java
			             patched by KeY
	junit.jar version 3.8.1: test framework

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_vxx.install: this file

   * KeYSrc_vxx.tgz: the source code version of KeY-system
   * KeYExtLib_vxx.tgz: contains the external libraries
     (see above) without the JavaCC. You have to download the javacc.jar
     separately
     e.g. http://www.experimentalstuff.com/Technologies/JavaCC/

   * quicktour_vxx.ps.gz: a short tutorial
   * KeYDemo_vxx.tgz: example for KeY used in the tutorial


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

	1) Untar the tar-gzipped file:

		tar -xvzf KeYSrc_vxx.tgz
		(if your tar do not support the 'z'-option,
		alternatively:
			mv KeYSrc_vxx.tgz KeYSrc_vxx.tar.gz
			gunzip KeYSrc_vxx.tar.gz
			tar -xvf KeYSrc_vxx.tar
		)

	2) Change to the created directory key-release09

		cd key-release09

	3) Install the needed libraries. Please choose ONE of these
	variants:

			a) 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


			b) Place the libraries into the key-ext-jars
                           directory already created in the current
			   system. You can simply use the
			   KeYExtLib_vxx.tgz archive, copy it to
			   ./key-ext-jars directory and
			   untar it:

				cp KeYExtLib_vxx.tgz ./key-ext-jars
				cd key-ext-jars
				tar -xzvf KeYExtLib_vxx.tgz
				cd ..

			   Do not forget to copy the JavaCC library
			   (that is not included in the archive) into
			   this directory:

				cp javacc.jar ./key-ext-jars

			c) Use symbolic links to point to the
			   libraries you have already at a different
			   place. You have to do this for all the
			   libraries listed in (1). For example, to
			   provide access to antlr.jar that is in the
			   directory ~/antlr use this:

				cd key-ext-jars
				ln -s ~/antlr/antlr.jar antlr.jar
				cd ..


	4) 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.0.1/linux) by
	
			setenv TOGETHER_HOME ~togetherj/vers6.0.1/linux

	   If you have chosen variant (5b) or (5c) you can instead use
	   symbolic links to point to the directory of TogetherCC, (e.g.)
				
			cd key-ext-jars
			ln -s ~togetherj/vers6.0.1/linux TOGETHER
			cd .. 


	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
	

(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

		key@mail.informatik.kit.edu