Changes between Version 65 and Version 66 of Be a CIVL developer


Ignore:
Timestamp:
03/10/23 07:51:45 (3 years ago)
Author:
Alex Wilton
Comment:

Another update to instructions to reflect the fact that several files in dev.civl.com have moved out to the root directory.

Legend:

Unmodified
Added
Removed
Modified

  • Be a CIVL developer

    v65 v66  
    7979  1. Click the three vertical dots at the top right of the Project Explorer window and select "Projects Presentation > Hierarchical".
    8080  1. Again, click the three vertical dots again and this time select "Package Presentation > Hierarchical". \\\\
    81 1. Open up the file `dev.civl.com/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:
    82   1. 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.
     811. 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:
     82  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.
    8383  1. Open up `build.properties` and replace the value of `root` with the absolute path to `vsl-X.XX`, replacing `X.XX` with `${civlversion}`.
    8484  1. Save and close the file. \\\\
    … …  
    101101    {{{
    102102#!/bin/sh
    103 java -cp $ECLIPSE_WORKSPACE/CIVL/mods/dev.civl.com -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 $@
     103java -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 $@
    104104    }}}
    105105  1. You must make it executable. You can use the command `chmod ugo+x civl`.
    106106  1. Move this file to somewhere on your `PATH`.
    107107  1. 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. \\\\
    108 1. 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 `dev.civl.com/examples` and try running `civl verify` on some of them!
     1081. 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!
    109109
    110110== Running CIVL from within Eclipse ==
    … …  
    114114  1. 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.
    115115  1. 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.
    116     * Example: "Program arguments:" `verify algebra.cvl`, "Working directory:" `${workspace_loc:dev.civl.com/examples/arithmetic}`. This will run `civl verify` on the `algebra.cvl` example in the folder `dev.civl.com/examples/arithmetic`.
     116    * 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.
    117117  1. Press "Apply". If you wish to run this configuration, select "Run" with the configuration selected.
    118118
    119119Now 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".
    120120
    121 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. 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.
     121To 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.
     122
     123Most 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`.
    122124
    123125== Using Subversion from the command-line ==