| 1 | SARL Installation Instructions
|
|---|
| 2 |
|
|---|
| 3 | ===================== Installing Theorem Provers =====================
|
|---|
| 4 |
|
|---|
| 5 | SARL can be used without any external theorem provers
|
|---|
| 6 | but it is unlikely to be able to resolve complex queries.
|
|---|
| 7 | For SARL to perform more precise analysis, it needs access
|
|---|
| 8 | to one or more high-quality automated theorem provers.
|
|---|
| 9 | You should install at least one of the theorem provers below.
|
|---|
| 10 | The more you install, the more precise SARL analysis will
|
|---|
| 11 | be.
|
|---|
| 12 |
|
|---|
| 13 | Note that SARL only requires the binary executable
|
|---|
| 14 | version of each prover; you can ignore the libraries, various
|
|---|
| 15 | API bindings, etc. You just need to ensure that
|
|---|
| 16 | each binary executable is in your PATH when you run
|
|---|
| 17 | "civl config". The currently supported provers are:
|
|---|
| 18 |
|
|---|
| 19 | - CVC3, http://www.cs.nyu.edu/acsys/cvc3/download.html
|
|---|
| 20 | download the latest, optimized build with static library
|
|---|
| 21 | and executable for your OS. Place the executable file
|
|---|
| 22 | "cvc3" in your PATH. You can discard everything else.
|
|---|
| 23 | Alternatively, on some linux systems, CVC3 can be installed
|
|---|
| 24 | using the package manager via "sudo apt-get install cvc3".
|
|---|
| 25 | This will place cvc3 in /usr/bin.
|
|---|
| 26 |
|
|---|
| 27 | - CVC4, http://cvc4.cs.nyu.edu/downloads/
|
|---|
| 28 |
|
|---|
| 29 | - Z3, http://z3.codeplex.com/SourceControl/latest
|
|---|
| 30 |
|
|---|
| 31 | ======================= Installing for Users ========================
|
|---|
| 32 |
|
|---|
| 33 | SARL is distributed as JAR file. It is written in Java 8.
|
|---|
| 34 |
|
|---|
| 35 | ===================== Installation from Source ======================
|
|---|
| 36 |
|
|---|
| 37 | 1. Install a Java 8 SDK if you have not already. Go to
|
|---|
| 38 |
|
|---|
| 39 | http://www.oracle.com/technetwork/java/javase/downloads/
|
|---|
| 40 |
|
|---|
| 41 | for the latest from Oracle. On linux, you can instead use
|
|---|
| 42 | the package manager:
|
|---|
| 43 |
|
|---|
| 44 | sudo apt-get install openjdk-8-jdk
|
|---|
| 45 |
|
|---|
| 46 | 2. Install Apache ant, if you don't already have it
|
|---|
| 47 | (http://ant.apache.org).
|
|---|
| 48 |
|
|---|
| 49 | 3. Download the tgz archive of VSL dependencies from
|
|---|
| 50 | http://vsl.cis.udel.edu/lib/tools/vsl_depend
|
|---|
| 51 | Unzip the .tgz file and you will have the folder vsl.
|
|---|
| 52 | Move vsl to /opt (you might need to use "sudo" for this.
|
|---|
| 53 | Also, if you don't already have a directory called /opt,
|
|---|
| 54 | you will have to create it with mkdir /opt).
|
|---|
| 55 |
|
|---|
| 56 | Suppose that you put the .tgz file (or .tar file if your browser
|
|---|
| 57 | unzipped it automatically to a .tar file) in the directory DOWNLOAD.
|
|---|
| 58 | You can use the following commands:
|
|---|
| 59 |
|
|---|
| 60 | $ cd DOWNLOAD
|
|---|
| 61 | $ tar xzf YourTgzOrTarFile vsl
|
|---|
| 62 | $ sudo mv vsl /opt
|
|---|
| 63 |
|
|---|
| 64 | Now you can type "ls /opt/vsl", and the output should be
|
|---|
| 65 |
|
|---|
| 66 | README.txt lib licenses src
|
|---|
| 67 |
|
|---|
| 68 | 4. svn checkout svn://vsl.cis.udel.edu/sarl/trunk sarl
|
|---|
| 69 |
|
|---|
| 70 | 5. cd sarl
|
|---|
| 71 |
|
|---|
| 72 | 6. If your VSL dependencies path is not in /opt/vsl, then you need
|
|---|
| 73 | to create a build.properties file by copying the content from
|
|---|
| 74 | build_default.properties and modifying the value of entry "root"
|
|---|
| 75 | to be the path to your VSL dependencies folder. The newly created file
|
|---|
| 76 | build.properties will automatically be used by ant to to build the
|
|---|
| 77 | .jar file.
|
|---|
| 78 |
|
|---|
| 79 | 7. Type "ant" and everything should build without warnings or errors
|
|---|
| 80 | and produce sarl.jar.
|
|---|
| 81 |
|
|---|
| 82 | 8. Type "ant test" to run a JUnit test suite. If you do not already
|
|---|
| 83 | have a SARL configuration file (.sarl) in your home directory, SARL
|
|---|
| 84 | will try to create one by looking for the theorem provers in your PATH.
|
|---|
| 85 | After this, all tests should pass.
|
|---|
| 86 |
|
|---|
| 87 | If there are any problems, email siegel at udel dot edu.
|
|---|
| 88 |
|
|---|
| 89 | ============= Installation from source using Eclipse ================
|
|---|
| 90 |
|
|---|
| 91 | 1. Start with the latest Eclipse IDE for Java/EE developers,
|
|---|
| 92 | http://www.eclipse.org/downloads/
|
|---|
| 93 |
|
|---|
| 94 | 2. Do steps 1-3 from above if you have not already.
|
|---|
| 95 |
|
|---|
| 96 | 3. Install an SVN plugin in Eclipse (such as Subversive) if you have
|
|---|
| 97 | not already.
|
|---|
| 98 |
|
|---|
| 99 | 4. From within Eclipse, select New Project...from SVN. The archive is
|
|---|
| 100 | svn://vsl.cis.udel.edu/sarl. After entering that, open it up and
|
|---|
| 101 | select the "trunk". (It is simplest to just check out the trunk for
|
|---|
| 102 | the Eclipse project.)
|
|---|
| 103 |
|
|---|
| 104 | 5. Check out the trunk, and create the project using the New Java
|
|---|
| 105 | Project Wizard as usual, naming it "SARL". The .project, .classpath,
|
|---|
| 106 | and other Eclipse meta-data are already in the SVN archive, saving you
|
|---|
| 107 | a bunch of work.
|
|---|
| 108 |
|
|---|
| 109 | 6. If your VSL dependencies path is not in /opt/vsl, then you need
|
|---|
| 110 | to create a build.properties file by copying the content from
|
|---|
| 111 | build_default.properties and modifying the value of entry "root"
|
|---|
| 112 | to be the path to your VSL dependencies folder. The newly created file
|
|---|
| 113 | build.properties will automatically be used by ant to to build
|
|---|
| 114 | the .jar file.
|
|---|
| 115 |
|
|---|
| 116 | 7. Do a clean build. Everything should compile. Generate the sarl.jar
|
|---|
| 117 | by right-clicking (or ctrl-click on OS X) the build.xml file and
|
|---|
| 118 | Run As->Ant Build.
|
|---|
| 119 |
|
|---|
| 120 | 8. Go to Run->Run Configurations.... Create a new JUnit configuration.
|
|---|
| 121 | Name it SARL Tests. Select "Run all tests in the selected project..."
|
|---|
| 122 | and navigate to the folder "test" in the SARL project.
|
|---|
| 123 | The Test runner should be JUnit 4. Under the Arguments tab, type
|
|---|
| 124 | "-ea" (without the quotes) in the VM arguments area (to enable
|
|---|
| 125 | assertion checking).
|
|---|
| 126 |
|
|---|
| 127 | 9. You may also use the command line to run the test suite, build
|
|---|
| 128 | the documentation, etc. "ant test" will run all of the tests
|
|---|
| 129 | and generate the JUnit report.
|
|---|