Home

This document gives instructions on how to configure a development environment for VerCors, using either Eclipse or Intellij IDEA. Below the instructions there is a list of encountered errors, you might want to check there if you encounter one.

TODO home Readme.md:

• JDK 8 should not be required, now installed openjdk11 & works
• should not need to get apache commons
• why do we distribute vct-sbt if it is required anyway
• ant comes with eclipse on linux

Configuring VerCors for Eclipse

First make sure that Eclipse is installed. The installation instructions described below have been tested with Ubuntu 18.04 and Eclipse version 4.11.0 (March 2019) from snap, not apt. The version from the eclipse website should be equivalent. Also make sure that VerCors has been installed according to the instructions given on the main Git page.

Install the Scala IDE plugin for Eclipse. Download- and installation instructions can be found here. After providing the installation/update site in Eclipse, make sure that all the suggested options are selected for installation. After installation has completed, navigate to Help > Install new software > Manage, and go to Scala > Compiler. We have to give scalac more memory to compile VerCors than is available by default, so enter "-J-Xmx2048m" under "Additional command line options" to increase the limit to 2048MB.

Install the eclipse plugin for sbt, instructions for which can be found here. It is recommended that you install it in the global file, and not in the vercors file, as we do not want to add eclipse-specific configuration in the repository. Create a global settings file for SBT (e.g. in ~/.sbt/1.0/global.sbt) and add the setting EclipseKeys.skipParents in ThisBuild := false

Configuring the VerCors modules

1. Navigate to the vercors subdirectory using a terminal, and run sbt eclipse. This will generate all the eclipse projects necessary to build vercors within eclipse.
2. In eclipse, go to File > Import and select General > Existing Projects into Workspace. Select the vercors subdirectory, and tick Search for nested projects. If all went well, it should list all the vercors subprojects (vercors, hre, parsers, viper, silicon, etc.). Click finish.
3. Eclipse will automatically build vercors; wait for it to finish. If eclipse fails to build the projects in this stage, unfortunately the projects are left in a broken state. You should remove all the projects or clear the workspace, and try again.

Running VerCors from Eclipse

To run VerCors from Eclipse, and thereby allow debugging within Eclipse, a Run Configuration needs to be created and used. To create a run configuration, do the following. In the menu, navigate to "Run > Run Configurations...". Select "Java Application" in the left menu and press the "New" button/icon in the toolbar. From here you can assign a name to the new configuration, for example "VerCors". Under "Project" select the "Vercors" project. Under "Main class" select or type vct.main.Main. Under the "Arguments" tab, type ${string_prompt} in the "Program arguments" field, so that every time VerCors is run with this new configuration, a pop-up window will be given in which arguments to VerCors can be specified. Moreover, in the "VM arguments" field, type -Xss16m, which increases the stack size to 16MB for VerCors runs (the default stack size may not be enough). Set the working directory to the root directory of the git repository (so vercors, not vercors/vercors). Finally, move to the "Environment" tab, click on the button "New...", and add two new environment variables: VCT_HOME, set to "." and TOOL_HOME, set to "./deps".

After performing these steps, you should be able to run VerCors from Eclipse via the "Run" option (do not forget selecting the new run configuration). The output of VerCors is then printed in Eclipse console view. To validate the configuration, try for example "--silicon examples/manual/fibonacci.pvl". If you get an error like NoClassDefFoundError: scala/Product, perform the workaround listed under "I got an error!" below.

Configuring VerCors for IntelliJ IDEA

The steps below were testing with Ubuntu 18.04 and Intellij IDEA community edition, version 2019.1.1 retrieved via snap. Also make sure that VerCors has been installed according to the instructions given on the main Git page.

When first installed, go to Configure > Plugins, or when already installed go to File > Settings > Plugins. Install the Scala plugin, and restart the IDE as suggested.

Configuring the project

1. Go to Open when first installed, File > Open otherwise, and open vercors/build.sbt. Open it as a project as suggested. In the dialog "Import Project from sbt", you should tick "Use sbt shell: for builds" and untick "Allow overriding sbt version".
2. Wait for the running process to complete, which configures the whole project.

Running VerCors from IntelliJ IDEA

Go to Run > Edit configurations, and add a Java application with the following settings:

• Main class: vct.main.Main
• VM options: -Xss 16m (increases the stack size to 16MB)
• Program arguments: $Prompt$ (asks for parameters every time)
• Working directory: the root of the git repository (so vercors, not vercors/vercors)
• Environment variables: VCT_HOME = "."; TOOL_HOME = "./deps"
• Use classpath of module: Vercors

You should now be able to run and debug VerCors from within IntellJ IDEA! The first time the run configuration is used the project will be built in full, so that will take some time.

I encountered an error!

Here is a collection of errors we encountered, with a solution. Is your problem not here? Please file an issue!

• While eclipse is building the workspace, I get a StackOverflowException. The scala compiler has insufficient memory to compile the project, try increasing the limit at Help > Install New Software > Manage, then Scala > Compiler. Try adding -J-X____m at "Additional command line parameters", substituting ___ with the amount of memory you want to try.
• Silicon is not detected as a project when running sbt eclipse. By default, parent projects (SBT projects that aggregate other projects) are not included by this tool. Remember to add EclipseKeys.skipParents in ThisBuild := false to the global SBT settings file.
• Only VerCors is detected as a project by eclipse. Remember to tick "Search for nested projects".
• The run configuration only outputs NoClassDefFoundError: scala/Product. For whatever reason, the scala runtime environment is not included in the run configuration. You should add manual dependencies in the run configuration, at Dependencies > Classpath Entries > Add External JARs. Add scala-library.jar and scala-reflect.jar, which should be present in the sbt configuration directory, ~/.sbt/boot/scala-x.x.x/ or similar. It seems to me that these libraries should be included from the project classpath, so please let me know if I'm misunderstanding!
• While IntelliJ is building, it encounters import errors in package vct.antlr4.generated. When creating the project from vercors/build.sbt, do not forget to tick "Use sbt shell: for builds", do not tick imports, and untick "allow overriding sbt version".