SARL Installation Instructions

===================== Installing Theorem Provers =====================

SARL can be used without any external theorem provers
but it is unlikely to be able to resolve complex queries.
For SARL to perform more precise analysis, it needs access
to one or more high-quality automated theorem provers.
You should install at least one of the theorem provers below.
The more you install, the more precise SARL analysis will
be.

Note that SARL only requires the binary executable
version of each prover; you can ignore the libraries, various
API bindings, etc.   You just need to ensure that
each binary executable is in your PATH when you run
"civl config".   The currently supported provers are:
  
   - CVC3, http://www.cs.nyu.edu/acsys/cvc3/download.html
     download the latest, optimized build with static library
     and executable for your OS.  Place the executable file
     "cvc3" in your PATH.  You can discard everything else.
     Alternatively, on some linux systems, CVC3 can be installed
     using the package manager via "sudo apt-get install cvc3".
     This will place cvc3 in /usr/bin.
     
   - CVC4,  http://cvc4.cs.nyu.edu/downloads/
   
   - Z3, http://z3.codeplex.com/SourceControl/latest

======================= Installing for Users ========================

SARL is distributed as JAR file.  It is written in Java 8.

===================== Installation from Source ====================== 

1. Install a Java 8 SDK if you have not already.  Go to

  http://www.oracle.com/technetwork/java/javase/downloads/

for the latest from Oracle.  On linux, you can instead use
the package manager:

  sudo apt-get install openjdk-8-jdk

2. Install Apache ant, if you don't already have it
(http://ant.apache.org).

3. Download the tgz archive of VSL dependencies from 
   http://vsl.cis.udel.edu/lib/tools/vsl_depend
   Unzip the .tgz file and you will have the folder vsl.
   Move vsl to /opt (you might need to use "sudo" for this.
   Also, if you don't already have a directory called /opt, 
   you will have to create it with mkdir /opt).

   Suppose that you put the .tgz file (or .tar file if your browser
   unzipped it automatically to a .tar file) in the directory DOWNLOAD.
   You can use the following commands:

   		$ cd DOWNLOAD
   		$ tar xzf YourTgzOrTarFile vsl
   		$ sudo mv vsl /opt

   Now you can type "ls /opt/vsl", and the output should be

   		README.txt    lib        licenses    src
   		
4. svn checkout svn://vsl.cis.udel.edu/sarl/trunk sarl

5. cd sarl

6. If your VSL dependencies path is not in /opt/vsl, then you need
to create a build.properties file by copying the content from
build_default.properties and modifying the value of entry "root"
to be the path to your VSL dependencies folder. The newly created file
build.properties will automatically be used by ant to to build the
.jar file.

7. Type "ant" and everything should build without warnings or errors
and produce sarl.jar.

8.  Type "ant test" to run a JUnit test suite.  If you do not already
have a SARL configuration file (.sarl) in your home directory, SARL
will try to create one by looking for the theorem provers in your PATH.
After this, all  tests should pass.

If there are any problems, email siegel at udel dot edu.

============= Installation from source using Eclipse ================

1. Start with the latest Eclipse IDE for Java/EE developers,
http://www.eclipse.org/downloads/

2. Do steps 1-3 from above if you have not already.

3. Install an SVN plugin in Eclipse (such as Subversive) if you have
not already.

4. From within Eclipse, select New Project...from SVN.  The archive is
svn://vsl.cis.udel.edu/sarl.  After entering that, open it up and
select the "trunk". (It is simplest to just check out the trunk for
the Eclipse project.)

5. Check out the trunk, and create the project using the New Java
Project Wizard as usual, naming it "SARL". The .project, .classpath,
and other Eclipse meta-data are already in the SVN archive, saving you
a bunch of work.

6. If your VSL dependencies path is not in /opt/vsl, then you need
to create a build.properties file by copying the content from
build_default.properties and modifying the value of entry "root"
to be the path to your VSL dependencies folder. The newly created file
build.properties will automatically be used by ant to to build
the .jar file.

7. Do a clean build.  Everything should compile.  Generate the sarl.jar
by right-clicking (or ctrl-click on OS X) the build.xml file and
Run As->Ant Build.  

8. Go to Run->Run Configurations.... Create a new JUnit configuration.
Name it SARL Tests. Select "Run all tests in the selected project..."
and navigate to the folder "test" in the SARL project.
The Test runner should be JUnit 4. Under the Arguments tab, type
"-ea" (without the quotes) in the VM arguments area (to enable
assertion checking).

9. You may also use the command line to run the test suite, build
the documentation, etc.  "ant test" will run all of the tests
and generate the JUnit report.