== How to become a CIVL developer == * If you are interested in contributing to the development of CIVL, send an email to civl-users@googlegroups.com expressing your interest, and we'll get back to you. We can use help in many areas, including testing and creating new examples, and we are very open to new ideas on all aspects of the project. * The lead developer will perform the following tasks: * Add you to the civl-dev@googlegroups.com email list. You will be able to read and post messages to this group. Use it to discuss any development issues. * Create a Subversion account for you in the appropriate projects (CIVL, ABC, SARL, GMC). You will then be able to commit to the `branches` directories in those repositories. (All of the repositories are already world-readable.) * Create a Trac account for you. You will then be able to create and modify bug/issue tickets, and write to the Wiki. (The tickets and Wiki are already world-readable.) == How to make changes or additions to CIVL == 1. To make any changes or additions to CIVL, you must first become a CIVL developer. See above. 1. Before embarking on any major changes or additions, talk to the other developers. This is best done using the email list civl-dev@googlegroups.com. Explain what you want to do, and listen to the feedback. 1. Create a new branch for the new features you want to add into CIVL. Name your branch anything you like and create it in the branches directory of the repository. See "Using Subversion from the command line" for instructions on creating the branch. 1. There are two different ways to work on your branch in Eclipse. The first way is appropriate for relatively small changes that do not involve a lot of components. In this approach you check out your branch into the current workspace, giving the project a different name from existing projects, e.g., `CIVL_mybranch`. In the second approach, you create a whole new workspace with all four projects. In this approach you can stick with the standard names for all projects (`CIVL`, `GMC`, `SARL`, `ABC`). This approach is appropriate when you have bigger changes affecting multiple components. 1. Proceed with development of your branch, committing as often as you like. Periodically, merge changes from the trunk into your branch, and resolve any conflicts that result. This will make it much easier to integrate your branch into the trunk later on. Be sure to follow the CIVL [wiki:"Coding Standards"] and the [wiki:"Coding Standards for CIVL models"]. 1. Create unit tests and system tests for your new code, making sure they provide 100% statement coverage of your code, at a minimum. You may also need to make changes to existing tests. 1. Have at least one other CIVL developer review your code. Your reviewer will make suggestions for improvements. Iterate until both of you are satisfied. 1. When you feel your branch is complete, send an email to civl-dev@googlegroups.com. In the email, give the name of your branch and summarize the changes/additions you have made. We will then schedule a CIVL meeting where your contribution will be discussed. All developers will be given some time to review your branch before the meeting. 1. At the meeting, your branch will either be accepted or it will be rejected with suggestions for further changes. If accepted, it will be merged into the trunk. Only the lead developers have permission to do this merge. If further changes are suggested, a future meeting will be scheduled to discuss again. We recommend using the Eclipse IDE to write CIVL code. Remember to set your Java code formatter as "built-in 2.1" in your Eclipse. == How to set up CIVL in Eclipse == 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/] \\\\ 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`. \\\\ 1. Set up the VSL dependencies folder: 1. Download the file found at [http://vsl.cis.udel.edu/lib/tools/vsl_depend]. 1. Unzip the `.tgz` so that you end up with a folder with a name of the form `vsl-X.XX`. 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. \\\\ 1. Install Eclipse IDE for Java Developers from here: [https://www.eclipse.org/downloads/packages/installer] \\\\ 1. Install Subversive for Eclipse using these instructions (paying attention to our notes below): [https://www.eclipse.org/subversive/installation-instructions.php] * ''Phase 1 notes:'' * When selecting which components to install only "Subversvie > Subversive SVN Team Provider" is required. * ''Phase 2 notes:'' * 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. * 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. \\\\ 1. Now we checkout the CIVL projects in Eclipse with Subversive. 1. "File > New > Project...". A Wizard Selector window should appear. 1. Pick "SVN > Project from SVN" and press "Next". A SVN Checkout window should appear. 1. Under the "General" tab, set the URL to be `svn://vsl.cis.udel.edu/civl` 1. Set "User" and "Password" to be the username and password you have for the CIVL repo. 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. 1. Press "Next". 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`. 1. Press "Finish". A "Check Out As" window should appear. 1. Select the option "Find projects in the children of the selected resource". 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. 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: * `dev.civl.abc` * `dev.civl.com` * `dev.civl.gmc` * `dev.civl.mc` * `dev.civl.sarl` \\\\ 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". \\\\ 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: 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. 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`. a. Save and close the file. \\\\ 1. Next we will point Eclipse to where the dependencies for CIVL are. a. Open up the Eclipse Preferences and then navigate to "Java > Build Path > Classpath Variables". a. Press "New...". A new popup window will appear. a. Enter `VSL` for the "Name:" field and then for the "Path:" field, enter the path to `vsl-X.XX`. a. Press "Ok". Then press "Apply and Close". Eclipse will ask you if you want to do a full rebuild. Press "Yes". \\\\ 1. Now we will run our ant scripts to perform our one-time task of running ANTLR. 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. a. Right-click on `dev.civl.abc` and press "Refresh". a. Perform the previous two steps for the project `dev.civl.mc`. == Running CIVL == 1. Somewhere on your system, create a plain text file containing exactly the following two lines: {{{ #!/bin/sh java -jar /Path/To/Your/workspace/CIVL/civl.jar $@ }}} where {{{/Path/To/Your/workspace}}} is replaced with the path to your Eclipse workspace directory. Name this file `civl`, put it in your `PATH`, and make it executable (`chmod ugo+x civl`). Alternatively, you can define an alias in your `.profile`, `.bash_profile`, `.bashrc`, or equivalent: {{{ alias civl='java -jar /Path/To/Your/workspace/CIVL/civl.jar' }}} 1. From the shell (terminal window), execute `civl config`. This should find the theorem provers in your `PATH` and create a file `.sarl` in your home directory. 1. In Eclipse, navigate to "Run->Run Configurations... Create a new JUnit configuration." Name it "CIVL Regression Tests". Select "Run all tests in the selected project..." and navigate to the folder `test/regress` in the CIVL project. The Test runner should be JUnit 4. Under the Arguments tab, type `-ea` in the VM arguments area (to enable assertion checking). 1. An example of how to set up a single test from within Eclipse: \\ create a new Run Configuration via the Run->Run Configurations... menu. Create a new "Java Application" configuration. Call it `CIVLbarrier2`. The Project is CIVL. The main class is `edu.udel.cis.vsl.civl.CIVL`. Under the Arguments tab, set the Program arguments to `verify examples/concurrency/barrier2.cvl`. Modify the VM arguments as in the step above. You should now be able to run the test by clicking "Run". == Using Subversion from the command-line == * CIVL uses Subversion to manage source code. The CIVL Subversion repository is structured in the typical way. In particular, the repository contains directories named `trunk`, `branches` and `tags`. * To create a new branch named `branch_name` from the current trunk, type {{{ svn copy svn://vsl.cis.udel.edu/civl/trunk svn://vsl.cis.udel.edu/civl/branches/branch_name }}} * Once a new branch has been created, you can check out your new branch with the command {{{ svn co svn://vsl.cis.udel.edu/civl/branches/branch_name }}} You can also create a new Eclipse project from that branch, in the usual way. * Within your own branch, you can change anything you want to implement your changes or additions, and you can commit your changes to the svn server so that you won't lose your work. * To merge changes made to the trunk into your branch, change into your local branch directory and type {{{ svn merge ^/trunk . }}} Resolve any conflicts and when you are satisfied with the state of your local copy, commit it as usual. Do this regularly (or whenever changes are committed to the trunk) in order to reduce the work of resolving conflicts when you decide to merge your branch back to the trunk. * To see a summary of the merge history from the trunk to your branch, go into your branch directory and type {{{ svn mergeinfo ^/trunk }}} * Lead developers only: to merge a branch back to the trunk, change into your local copy of the trunk directory and type {{{ svn merge ^/branches/branch_name . }}} Resolve conflicts as needed and make sure all tests pass. Then commit the trunk. At this point the branch may be deleted (`svn remove ^/branches/branch_name`) or it can be kept around if the developer wants to continue to use it.