| 24 | | 1. Install theorem provers [https://github.com/CVC4/CVC4 cvc4] and [https://github.com/Z3Prover/z3/releases z3] following the instructions provided with those tools. CIVL uses only the command line interface for these tools, so you don't have to worry about installing libraries or anything other than the executable binary. Make sure the executable is somewhere in your PATH. |
| 25 | | 1. Install Eclipse IDE for Java/EE developers if you have not already done so. |
| 26 | | 1. Install an SVN plugin in Eclipse (such as Subversive) if you have not already done so. To install Subversive follow the instructions found at [https://www.eclipse.org/subversive/installation-instructions.php]. |
| 27 | | 1. If you already have the VSL dependencies library, you may skip this step. Otherwise, download the tgz archive of VSL dependencies from [http://vsl.cis.udel.edu/lib/tools/vsl_depend http://vsl.cis.udel.edu/lib/tools/vsl_depend]. Unzip the .tgz file and you will have the folder named `vsl`. Move `vsl` directly under `/opt` (this might require `sudo`). |
| 28 | | 1. Install prerequisite projects ABC, SARL and GMC. Make sure that the three projects are put in the workspace directory where CIVL will be created. Specifically:\\ \\ |
| 29 | | * Install the symbolic algebra and reasoning library SARL. In Eclipse, select New Project...from SVN, and use the archive svn://vsl.cis.udel.edu/sarl. After entering that, open it up and select the "trunk" (or the appropriate branch if you are working on a branch). The project by default will be named "SARL" and there is no reason to change this unless you want to have two different branches of SARL existing simultaneously in the same workspace. Then follow the instructions in SARL's INSTALL file for Eclipse installation. As those instructions explain, if the default settings in `build_default.properties` are not appropriate for you, then create a copy called `build.properties` in the same directory and edit it as you will. (This copy will be ignored by version control.) Build `sarl.jar` from within Eclipse by right-clicking (or ctrl-clicking) on the `build.xml` file and selecting Run As->Ant Build. \\ |
| 30 | | \\ |
| 31 | | * Install the C front-end ABC. In Eclipse, select New Project...from SVN, use the archive svn://vsl.cis.udel.edu/abc. The process is exactly like the one for SARL described above. \\ \\ |
| 32 | | * Install the generic model checking utilities package GMC. In Eclipse, select New Project...from SVN, use the archive svn://vsl.cis.udel.edu/gmc. Same process. \\ \\ |
| 33 | | 1. From within Eclipse, select New Project...from SVN. The archive is svn://vsl.cis.udel.edu/civl. Follow the same process as with the other 3 projects to install CIVL. |
| 34 | | 1. Navigate to Preferences -> Java -> Build Path -> !ClassPath Variables, and then select New to create a classpath variable `VSL`, and specify its value to be `/opt/vsl`. |
| 35 | | 1. Do a clean build. Everything should compile. Generate `civl.jar` by right-clicking (or ctrl-click on OS X) the `build.xml` file and Run As->Ant Build. |
| | 24 | 1. If your version of Java is older than 17 (the version number in the first line printed by the command `java --version` is what version you have) then install the latest version of Java here: [https://www.oracle.com/java/technologies/downloads/] \\\\ |
| | 25 | 1. Install theorem provers [https://github.com/CVC4/CVC4 cvc4] and [https://github.com/Z3Prover/z3/releases z3] following the instructions provided with those tools. CIVL uses only the command line interface for these tools, so you don't have to worry about installing libraries or anything other than the executable binary. Make sure the executable is somewhere in your `PATH`. \\\\ |
| | 26 | 1. Set up the VSL dependencies folder: |
| | 27 | 1. Download the file found at [http://vsl.cis.udel.edu/lib/tools/vsl_depend]. |
| | 28 | 1. Unzip the `.tgz` so that you end up with a folder with a name of the form `vsl-X.XX`. |
| | 29 | 1. Pick somewhere in your filesystem to move this folder. On Unix systems a good choice is `/opt`. On Windows a good choice is `C:\Program Files`. Note that you may need to use `sudo` on Unix or use Administrator permissions on Windows to perform this move depending on where you choose to place this folder. \\\\ |
| | 30 | 1. Install Eclipse IDE for Java Developers from here: [https://www.eclipse.org/downloads/packages/installer] \\\\ |
| | 31 | 1. Install Subversive for Eclipse using these instructions (paying attention to our notes below): [https://www.eclipse.org/subversive/installation-instructions.php] |
| | 32 | * ''Phase 1 notes:'' |
| | 33 | * When selecting which components to install only "Subversvie > Subversive SVN Team Provider" is required. |
| | 34 | * ''Phase 2 notes:'' |
| | 35 | * There is a comment that a dialog automatically displays after rebooting but it is not our experience that this actually happens. So if it doesn't for you then just follow the instructions they have just below that comment for manually installing the SVN connectors. It will be a near identical process to the installation done in Phase 1. |
| | 36 | * Unless you know how to set up your own SVN Connector with Subversive, you should check all the boxes in this phase (i.e. check the parent level box "Subversive SVN Connectors"). This will include the supposedly "optional" component "SVNKit 1.10.x Implementation" which is an implementation of a SVN Connector using SVNKit. \\\\ |
| | 37 | 1. Now we checkout the CIVL projects in Eclipse with Subversive. |
| | 38 | 1. "File > New > Project...". A Wizard Selector window should appear. |
| | 39 | 1. Pick "SVN > Project from SVN" and press "Next". A SVN Checkout window should appear. |
| | 40 | 1. Under the "General" tab, set the URL to be `svn://vsl.cis.udel.edu/civl` |
| | 41 | 1. Set "User" and "Password" to be the username and password you have for the CIVL repo. |
| | 42 | 1. Check "Save authentication" if you don't want to have to enter that information when performing future SVN commands on this repo in Eclipse. |
| | 43 | 1. Press "Next". |
| | 44 | 1. Press the "Browse..." button next to the URL. In the window that pops up, expand the "civl" folder and select "trunk". Press OK. The pop-up window should disappear and the URL should now say `svn://vsl.cis.udel.edu/civl/trunk`. |
| | 45 | 1. Press "Finish". A "Check Out As" window should appear. |
| | 46 | 1. Select the option "Find projects in the children of the selected resource". |
| | 47 | 1. Press "Finish". The window should change (after about 5 seconds) and display a list of 5 items. Ensure the option "Check out as a projects into workspace" at the top is selected. Also ensure that each of the 5 items in the list are checked. |
| | 48 | 1. Press "Finish". The window should disappear and you should see a small progress bar in the bottom left corner of Eclipse. This shows its progress in checking out each of the 5 new projects that Eclipse is creating. Eventually the progress bar should be complete and you should see 5 new projects in your workspace (probably marked with warnings and errors) titled: |
| | 49 | * `dev.civl.abc` |
| | 50 | * `dev.civl.com` |
| | 51 | * `dev.civl.gmc` |
| | 52 | * `dev.civl.mc` |
| | 53 | * `dev.civl.sarl` \\\\ |
| | 54 | 1. You probably will want to change the package presentation to the hierarchical view since it makes navigating the code much easier. Click the three vertical dots at the top right of the Package Explorer window (where your projects are) and then press "Package Presentation > Hierarchical". \\\\ |
| | 55 | 1. Open up the file `dev.civl.com/build_default.properties`. If the value of `root.parent` does not match the absolute path to the containing folder of the VSL dependencies folder, `vsl-X.XX`, that you downloaded earlier then perform the following nested instructions: |
| | 56 | a. Close `build_default.properties` and then make a copy of it (still in `dev.civl.com`) called `build.properties`. Do not delete `build_default.properties` since this is tracked by SVN. |
| | 57 | a. Open up `build.properties` and replace the value of `root.parent` with the absolute path to the containing folder of `vsl-X.XX`. If you are on Windows, you must replace backslashes `\` with forward slashes `/`. For example, if you are on Windows and your path to `vsl-X.XX` looks like `C:\Program Files\vsl-X.XX`, then the value of `root.parent` will be `C:/Program Files`. |
| | 58 | a. Save and close the file. \\\\ |
| | 59 | 1. Next we will point Eclipse to where the dependencies for CIVL are. |
| | 60 | a. Open up the Eclipse Preferences and then navigate to "Java > Build Path > Classpath Variables". |
| | 61 | a. Press "New...". A new popup window will appear. |
| | 62 | a. Enter `VSL` for the "Name:" field and then for the "Path:" field, enter the path to `vsl-X.XX`. |
| | 63 | a. Press "Ok". Then press "Apply and Close". Eclipse will ask you if you want to do a full rebuild. Press "Yes". \\\\ |
| | 64 | 1. Now we will run our ant scripts to perform our one-time task of running ANTLR. |
| | 65 | a. Right-click on `dev.civl.abc/build.xml`. Press "Run As > 1 Ant Build". After about 20 seconds, the console should have displayed BUILD SUCCESSFUL. |
| | 66 | a. Right-click on `dev.civl.abc` and press "Refresh". |
| | 67 | a. Perform the previous two steps for the project `dev.civl.mc`. |
| | 68 | |
| | 69 | == Running CIVL == |
