Changes between Version 49 and Version 50 of Be a CIVL developer


Ignore:
Timestamp:
02/24/17 10:36:49 (9 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Be a CIVL developer

    v49 v50  
    2020 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.
    2121
    22 == Set up CIVL in Eclipse ==
    23 1. Install  theorem provers [http://www.cs.nyu.edu/acsys/cvc3/ cvc3], [https://github.com/CVC4/CVC4 cvc4] and [https://github.com/Z3Prover/z3/releases z3]. Install Eclipse IDE for Java/EE developers if you have not already done so.
    24 1. Install an SVN plugin in Eclipse (such as Subversive) if you have not already.
    25 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 vsl. Move vsl to /opt.
     22== How to set up CIVL in Eclipse ==
     231. Install  theorem provers [http://www.cs.nyu.edu/acsys/cvc3/ cvc3], [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.
     241. Install Eclipse IDE for Java/EE developers if you have not already done so.
     251. Install an SVN plugin in Eclipse (such as Subversive) if you have not already done so.
     261. 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`). 
    26271. 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:\\ \\
    27    * Install the symbolic algebra and reasoning library SARL. In Eclipse, select New Project...from SVN, use the archive  svn://vsl.cis.udel.edu/sarl. After entering that, open it up and select the "trunk". After checking out trunk, name  the project "SARL". Then follow the instructions in the INSTALL file for Eclipse installation. Build the sarl.jar from within Eclipse by right-clicking (or ctrl-clicking) on the build.xml file and selecting Run As->Ant Build. \\
     28   * 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. \\
    2829 \\
    29    * Install the C front-end ABC. In Eclipse, select New Project...from SVN, use the archive svn://vsl.cis.udel.edu/abc. After entering that, open it up and select the "trunk". After checking out trunk, name the project "ABC". Then follow the instructions in the INSTALL file for Eclipse installation. Build the abc.jar from within Eclipse by right-clicking (or ctrl-clicking on OS X) on the build.xml file and selecting Run As->Ant Build. \\ \\
    30    * Install the generic model checking utilities package GMC. In Eclipse, select New Project...from SVN, use the archive svn://vsl.cis.udel.edu/gmc. After entering that, open it up and select the "trunk". After checking out !trunk, name the project "GMC". Build the gmc.jar from within Eclipse by right-clicking (or ctrl-clicking) on the build.xml file and selecting Run As->Ant Build. \\ \\
    31 1. From within Eclipse, select New Project...from SVN. The archive is svn://vsl.cis.udel.edu/civl.  After entering that, open it up and select the "trunk". (It is simplest to just check out the trunk for the Eclipse project.)
    32 1. Check out the trunk, and create the project using the New Java Project Wizard as usual, naming it "CIVL". The .project, .classpath, and other Eclipse meta-data are already in the SVN archive, saving you a bunch of work.
    33 1. If default_build.properties matches the configuration of your system, then you can skip this step. Otherwise, you may need to create a file build.properties in the directory containing build.xml. Copy and paste the content from any file under properties, edit each entry with the path configured in your system. The newly created file build.properties will automatically be used by ant to to build the .jar file.
    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 the civl.jar by right-clicking (or ctrl-click on OS X) the build.xml file and Run As->Ant Build.
     30   * 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. \\ \\
     31   * 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. \\ \\
     321. 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.
     331. 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`.
     341. 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.
    36351. Somewhere on your system, create a plain text file containing exactly the following two lines:
    3736  {{{
    … …  
    3938java -jar /Path/To/Your/workspace/CIVL/civl.jar $@
    4039  }}}
    41   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:
     40  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:
    4241{{{
    4342alias civl='java -jar /Path/To/Your/workspace/CIVL/civl.jar'
    4443}}}
    45 1. From a terminal window, execute "civl config".  This should find the theorem provers in your PATH and create a file .sarl in your home directory.
    46 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" (without the quotes) in the VM arguments area (to enable assertion checking).
    47 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".
     441. 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.
     451. 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).
     461. 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".
    4847
    49 == Using Subversion in command-line ==
     48== Using Subversion from the command-line ==
    5049
    5150* 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`.