extended README

README

 This is Leon 0.2.0
 
+===============
+Getting Started
+===============
+
+This section gives a very quick overview of how to build and use Leon, refer to
+the following sections if you wish (or need) more detailed information.
+
 To build it, you will need, for example, the following:
   * Java Runtime Environment, from Oracle, e.g. Version 7 Update 5 
     (to run xsbt and scala)
@@ -10,6 +17,11 @@ To build it, you will need, for example, the following:
     (for Z3)
   * GNU Multiprecision library, e.g. gmp3, works with e.g. apt-get
     (for Z3)
+The followin can be obtained from the web, but for convenience they are contained in the
+repository and are actually automatically handled by the default build configuration.
+  * ScalaZ3 from https://github.com/psuter/ScalaZ3/
+  * The libz3 library from microsoft:
+    http://research.microsoft.com/en-us/um/redmond/projects/z3/
 
 To build, type this:
 
@@ -19,7 +31,7 @@ xsbt script
 
 Then you can try e.g.
 
-./run-demo demo/RedBlackTree.scala
+./leon testcases/sas2011-testcases/RedBlackTree.scala
 
 and get something like this:
 
@@ -43,16 +55,122 @@ and get something like this:
           ║ redNodesHaveBlackChildren match.      (35,56) valid               Z3-f+t    0.003 ║
           ║ size                      postcond.           valid               Z3-f+t    0.012 ║
           ╚═══════════════════════════════════════════════════════════════════════════════════╝
+          
+
+=============
+Building Leon
+=============
+
+Leon requires quite a few dependencies, and you will need to make sure
+everything is correctly set up before being able to build it. Leon is probably
+much easier to build on Unix-like plattforms. Not to say it is impossible to
+build on Windows. But some scripts used to run and test the system are shell
+script and you will need to manually port them to Windows if you wish to use
+Windows.
+
+First you need a Java Runtime Environment. The most recent version should work.
+Simply follow the standard installation process (e.g. apt-get) for your system.
+
+Next, you need the Simple Build Tool (sbt) https://github.com/harrah/xsbt/wiki
+which seems to be (as of today) the standard way to build Scala program. Again
+you should follow the installation procedure. You can also find information
+about sbt here: http://typesafe.com/technology/sbt. Sbt is quite a complex
+tool, so I would suggest looking at the getting started guide on the wiki page.
+However, if you just want to quickly build Leon and never look back, then the
+information provided here should be sufficient.
+
+(This section is outdated for linux, but can be useful to adapt on Windows/Mac)
+Now you will have to build the ScalaZ3 project from
+https://github.com/psuter/ScalaZ3/. You should follow the instructions given in
+the ScalaZ3 project. The ScalaZ3 is a Scala wrapper on the Z3 native library
+from Microsoft. It is used in Leon to make native call to Z3. The generated
+.jar from ScalaZ3 will be dependent on your own z3 native library, which you
+can obtain from http://research.microsoft.com/en-us/um/redmond/projects/z3/.
+However, the ScalaZ3 repository comes with 32 and 64 bits version for Linux and
+you should probably use those ones to make sure the version is compatible. You
+can install the Z3 native library in some standard system library path such as
+/usr/lib. You need to install the scalaz3.jar file in the "unmanaged"
+directory. The build system is configured to use any jar file in the
+"unmanaged" directory. Finally be aware that the Z3 library will come with its
+own set of dependencies, in particular you will need to have GMP. You will
+probably have to fight with a few errors before everything can finally work
+together.
+
+Finally you can build Leon. Start sbt from a terminal to get an interactive
+sbt session. Then type:
+  clean
+This will make sure the build is clean, then:
+  package
+This will compile everything and create jar files. This could take a long time.
+Finally you need to generate a running script with the command:
+  script
+This will generate the leon script that can be used to run leon from command line
+with correct arguments and classpath. This script you should not need to re-generate
+another time, if you modify some code you just need to run 'compile' again. If anything
+goes wrong, you should carefully read the error message and try to fix it. You can
+refer to the troubleshooting section of this manual.
+
+Note that Leon is organised as a structure of two projects, with one main (or
+root) project and one sub-project. From a user point of view, this should most
+of the time be transparent and the build command should take care of
+everything. The subproject is in 'library' and contains required code to make
+Leon input programs valid Scala programs. The point of having this library
+sub-project, is that you can use the generated jar for the library sub-project
+on its own and you should be able to compile Leon testcases with the standard
+Scala compiler.
+
+Now we can make sure that the build went fine. There is a collection of
+testcase in 'regression' that are used to check the correctness of the system.
+We provide a shell script 'run-tests.sh' to run all of them and make sure Leon
+behaves as expected. You should run ./run-tests now to make sure everything is in
+order. Note that running all tests can take some time.
+
+==========
+Using Leon
+==========
+
+
+========================
+Layout of this directory
+========================
+
+Here is a quick overview of the conventions used in the layout of this directory.
+
+  -src
+    Contains all Scala sources for the Leon project. The layout of the sources follows the standard SBT (and Maven) convention.
+
+  -regression
+    Contains many small testcases. They are meant to be run automatically with a test script and Leon should behave correctly on
+    all of them (correctly could mean either proving validity, finding counter-example or refusing the input).
+
+  -testcases
+    Contains somewhat realistic testcases, that correspond to existing algorithms. Leon might not successfully handle all of them.
+
+  -README
+    This file.
+
+  -PERMISSION
+    You can safely ignore this file.
+    It is used to handle git PERMISSION for this repository.
+
+  -build.sbt
+  -project/Build.sbt
+    Configuration of SBT.
+
+  -library
+    Sub-project containing the Leon library. Needed if one wishes to run Leon testcases with standard Scala.
+
+  -unmanaged
+    This is the directory used by the build system to find unmanated dependencies. You usually need to manually
+    add files to this directory.
+
+  -lib-bin
+  -lib64-bin
+    Contains some binary dependencies for the system that have been build for different plattform/OS.
+
+  
+===============
+Troubleshooting 
+===============
 
-Additional information:
-=======================
-Sample output of 
-  ldd lib-bin/lib3.so
-is:
-	linux-gate.so.1 =>  (0x00b13000)
-	libgmp.so.3 => /usr/lib/libgmp.so.3 (0x00110000)
-	libstdc++.so.6 => /usr/lib/i386-linux-gnu/libstdc++.so.6 (0x0016f000)
-	libm.so.6 => /lib/i386-linux-gnu/libm.so.6 (0x0025a000)
-	libgcc_s.so.1 => /lib/i386-linux-gnu/libgcc_s.so.1 (0x00709000)
-	libc.so.6 => /lib/i386-linux-gnu/libc.so.6 (0x004d9000)
-	/lib/ld-linux.so.2 (0x002ab000)
+Sorry, not done yet :(