*********************************
		* KeY Source Code Installation  * 
		*        Version 1.6.0         *
		********************************

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

Operating System: Linux/Unix, MacOSX, Windows (untested) 

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

Needed additional Libraries:
	antlr.jar Version >= 2.7.2: parser generator
	javacc.jar Version >= 3.0 : parser generator
	recoderKey.jar 
                 a transformation framework for java patched by the KeY group
	junit.jar version 3.8.1: test framework

Optionally, KeY can make use of the following binaries:
	SMT Solvers: bindings exist currently for Z3, Simplify, Yices and CVC3
              (export to SMT input file possible)        


(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
                     or (bash)     export KEY_LIB=~/key_lib                  
                     or (Windows)  set KEY_LIB=<path to libraries>

	4) Optional: Install Simplify and/or other SMT solvers.

           If you download Simplify not from the KeY-website but
           elsewhere (e.g. 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 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

          (analog procedure for other solvers)

	5) Change to the subdirectory ./system

		cd system

	6) Compile KeY:

		 make all (or gmake all)
             or 
                 export ANT_OPTS="-Xmx512m"
                 ant

           (compilation via 'ant' should work under Windows too, but you need to set the ANT_OPTS
            environment variable most likely via
                           set ANT_OPTS = "-Xmx512m"
            )                   

	

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

		../bin/runProver


(5) Alternatively to (4): Start KeY in Test Generation Mode
-------------------------------------

	Run 'startProver unit' or if you wish a simpler GUI run 'startProver testing'
	  (Windows: 'startProver.bat unit' or 'startProver.bat testing')
	
	The library objenesis.jar may be required to run the generated tests.


-------------------------------

If you encounter problems, please send a message to

		support@key-project.org