wiki:Be a CIVL developer

How to become a CIVL developer

  • If you are interested in contributing to the development of CIVL, send an email to civl-users@… 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@… 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.
  2. Before embarking on any major changes or additions, talk to the other developers. This is best done using the email list civl-dev@…. Explain what you want to do, and listen to the feedback.
  3. 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.
  4. 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.
  5. 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 Coding Standards and the Coding Standards for CIVL models.
  6. 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.
  7. Have at least one other CIVL developer review your code. Your reviewer will make suggestions for improvements. Iterate until both of you are satisfied.
  8. When you feel your branch is complete, send an email to civl-dev@…. 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.
  9. 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.

Notes for Windows Users

CIVL is not currently supported on Windows. However, it is easy to use CIVL and set up an Eclipse development environment on Windows using WSL. With Windows 11 or with Windows 10 21H2 (or newer), you can easily install WSL2 and run Linux GUI applications from it.

If you want to develop CIVL using a Windows machine, you should install WSL2 using the following instructions and then follow the remaining instructions of this page in the Linux partition managed by WSL.

  1. Open up powershell and execute the command wsl --install
  2. Restart your computer.
  3. Open up WSL (you can search for it now on the windows start menu). Pick a username and password to use when it asks.
  4. Execute sudo apt update
  5. Execute sudo apt upgrade
  6. Execute sudo apt install openjdk-17-jre-headless
  7. To get all packages required for displaying GUIs, it is easiest to install a simple GUI application like gedit which will obtain all of the necessary packages for you. Execute sudo apt install gedit -y.
  8. Test gedit out by running gedit. A separate GUI window for gedit should appear. This means you are now set up to run GUI Linux applications from WSL.

You can now follow the rest of the instructions on this page. Note that when downloading files, you may need to move them to somewhere on your Linux partition before running them (like the Eclipse installer for example). This can easily be done with the regular Windows file explorer.

As a reminder, all the instructions on this page are to be done with respect to your Linux partition created by WSL. So for example, if an instruction says that something needs to go on your PATH, this means that it should be on your Linux PATH not the Windows PATH.

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/

  2. Install theorem provers ​cvc4 and ​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.

  3. Set up the VSL dependencies folder:
    1. Download the file found at ​http://vsl.cis.udel.edu/lib/tools/vsl_depend.
    2. Unzip the .tgz so that you end up with a folder with a name of the form vsl-X.XX.
    3. Pick somewhere in your filesystem to move this folder. A good choice is /opt. Note that you may need to use sudo.

  4. Install Eclipse IDE for Java Developers using the install found here: ​https://www.eclipse.org/downloads/packages/installer

  5. 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 "Subversive > 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.

  6. Now we checkout the CIVL projects in Eclipse with Subversive.
    1. "File > New > Project...". A Wizard Selector window should appear.
    2. Pick "SVN > Project from SVN" and press "Next". A SVN Checkout window should appear.
    3. Under the "General" tab, set the URL to be svn://vsl.cis.udel.edu/civl
    4. Set "User" and "Password" to be the username and password you have for the CIVL repo.
    5. Check "Save authentication" if you don't want to have to enter that information when performing future SVN commands on this repo in Eclipse.
    6. Press "Next".
    7. 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.
    8. Press "Finish". A "Check Out As" window should appear.
    9. Select the option "Check out as a project with the name specified:" and set the name to be CIVL.
    10. 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 the repo into your workspace.
    11. Once completed, you should see a new project in your workspace titled CIVL. Right-click it and select "Import...". An Import window should appear.
    12. Select "General > Existing Projects into Workspace" and then press "Next".
    13. In the next window, select "Select root directory:" and set it to be the path to the CIVL directory in your workspace.
    14. Next, uncheck the option "Copy projects into workspace" and check the option "Search for nested projects". In the "Projects:" list of the window there should be 5 new projects that appear titled:
      • dev.civl.abc
      • dev.civl.com
      • dev.civl.gmc
      • dev.civl.mc
      • dev.civl.sarl
    15. Select these 5 projects and then press "Finish".
    16. The window should disappear and the 5 projects you selected should appear in the Package Explorer window.

  7. To properly work with these new projects, you must change to using the Project Explorer window rather than the Package Explorer window.
    1. Close out of the Package Explorer window and then select "Window > Show View > Project Explorer".
    2. Click the three vertical dots at the top right of the Project Explorer window and select "Projects Presentation > Hierarchical".
    3. Again, click the three vertical dots again and this time select "Package Presentation > Hierarchical".

  8. Open up the file build_default.properties. If the value of root does not match the absolute path to the VSL dependencies folder, vsl-X.XX, that you downloaded earlier then perform the following nested instructions:
    1. Close build_default.properties and then make a copy of it called build.properties. Do not delete build_default.properties since this is tracked by SVN.
    2. Open up build.properties and replace the value of root with the absolute path to vsl-X.XX, replacing X.XX with ${civlversion}.
    3. Save and close the file.

  9. Next we will point Eclipse to where the dependencies for CIVL are.
    1. Open up the Eclipse Preferences and then navigate to "Java > Build Path > Classpath Variables".
    2. Press "New...". A new popup window will appear.
    3. Enter VSL for the "Name:" field and then for the "Path:" field, enter the path to vsl-X.XX.
    4. Press "Ok". Then press "Apply and Close". Eclipse will ask you if you want to do a full rebuild. Press "Yes".

  10. Now we will run our ant scripts to perform our one-time task of running ANTLR.
    1. 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.
    2. Right-click on dev.civl.abc and press "Refresh".
    3. Perform the previous two steps for the project dev.civl.mc.

Running CIVL from command line

  1. We will create a script that will sit on your PATH that will allow you to conveniently run CIVL from the .class files built in Eclipse.
    1. Create two new environment variables:
      • ECLIPSE_WORKSPACE should be the absolute path to your Eclipse workspace.
      • VSL_DEPS should be the path to your vsl-X.XX dependencies folder.
    2. Somewhere on your system, create a plain text file named civl and copy-paste the following: 
      #!/bin/sh
java -cp $ECLIPSE_WORKSPACE/CIVL -p $ECLIPSE_WORKSPACE/CIVL/mods/dev.civl.abc:$ECLIPSE_WORKSPACE/CIVL/mods/dev.civl.gmc:$ECLIPSE_WORKSPACE/CIVL/mods/dev.civl.mc:$ECLIPSE_WORKSPACE/CIVL/mods/dev.civl.sarl:$VSL_DEPS/mods/antlr3:$VSL_DEPS/mods/antlr4 -m dev.civl.mc/dev.civl.mc.CIVL $@
    3. You must make it executable. You can use the command chmod ugo+x civl.
    4. Move this file to somewhere on your PATH.
    5. Run civl help from the command line to ensure that it worked. You should get a long list of command line options that CIVL accepts.

  2. Execute the command civl config. This should find the theorem provers in your PATH and create a file .sarl in your home directory. You can now run civl from the command line. Go to the example files found in the examples directory and try running civl verify on some of them!

Running CIVL from within Eclipse

To run CIVL from Eclipse, you need to create a run configuration that specifies where the "main class" is and then what arguments you want to pass CIVL and where you want to run CIVL from. After setting this up you can reuse this run configuration by simply altering the arguments you pass it and where it is executed from.

  1. In Eclipse, navigate to "Run > Run Configurations..." and select the "Java Application" item in the left column of the window.
  2. Press the "New Configuration" button and give it a name like "CIVL".
  3. Under the "Main" tab, enter dev.civl.mc as the "Project" and dev.civl.mc.CIVL as the "Main class". You can use the "Browse..." and "Search..." buttons for this.
  4. Under the "Arguments" tab, enter the program arguments you want to pass to CIVL in the "Program arguments" section. In the "Working directory" section at the bottom of the same tab select "Other:" and specify where you want CIVL to be executed from.
    • Example: "Program arguments:" `verify algebra.cvl`, "Working directory:" ${workspace_loc:CIVL/examples/arithmetic}. This will run civl verify on the algebra.cvl example in the folder CIVL/examples/arithmetic in your workspace.
  5. Press "Apply". If you wish to run this configuration, select "Run" with the configuration selected.

Now whenever you want to run CIVL, you can simply go to "Run > Run Configurations...", select the "CIVL" configuration you have made, and change the settings under the "Arguments" tab as needed and press "Run". If you want to run CIVL in debug mode then you will instead go to "Run > Debug Configurations...", select the "CIVL" configuration you made and press "Debug".

To run JUnit tests, you can set up a JUnit launch configuration in a similar way to above, but Eclipse is able to automatically set up appropriate launch configurations for you (except for tests found in dev.civl.mc). All you need to do is right-click on whatever test suite you want to run JUnit on (this can be folders containing tests, or even an individual test within a .java file) and then select "Run As > JUnit Test". If you want to run the JUnit test in debug mode then simply select "Debug As > JUnit Test" instead.

Most tests in dev.civl.mc rely on the files found in the root level examples folder. By default though, Eclipse will set up new JUnit configurations to run from the project folder containing the tests (so in this case dev.civl.mc). However we need these tests to be run from the root folder CIVL. So when setting up JUnit tests under dev.civl.mc, you must set the "Working directory" to be the root folder CIVL.

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.

Last modified 3 years ago Last modified on 03/10/23 07:51:45
Note: See TracWiki for help on using the wiki.