diff --git a/README b/README
index dd0228d692f848dfd5c949773a884c89135c3c76..26229521988cc34cd1692b7e263ffe2316560167 100644
--- a/README
+++ b/README
@@ -1,5 +1,12 @@
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 :(