IDE Import ‐ old unsupported instructions for sbt

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. The setup for IntelliJ IDEA is considerably easier, so we recommend using that.

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.

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. (For older IDEA versions: in the dialog "Import Project from sbt", you should tick "Use sbt shell: for imports" and "for builds")
2. Wait for the running process to complete, which configures the whole project.
3. Open File > Settings, go to Build, Execution, Deployment > Build Tools > sbt, select the "vercors" sbt project (likely the only one) and tick use for [x] project reload and [x] builds. (Not needed in old versions of IDEA)

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: -Xss16m (increases the stack size to 16MB; as of IDEA 2020.3 you need to click Modify options > Add VM options first)
• Program arguments: $Prompt$ (asks for parameters every time)
• Working directory: the root of the git repository
• Use classpath of module: Vercors (as of IDEA 2020.3: -cp 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.

Configure SonarLint for VerCors in IntelliJ

SonarCloud runs code quality checks e.g. when you merge a branch. SonarLint gives you the same warnings as SonarCloud but now inside IntelliJ, while you work on the code. SonarLint also supports Eclipse, Visual Studio and VS code. While this instruction focusses on IntelliJ, the installation steps for other IDEs will likely be similar.

1. Install the SonarLint Plugin by following the installation instructions.
   • E.g. in IntelliJ via File > Settings > Plugins.
2. Add a connection which synchronises the rules of SonarLint with those of SonarCloud.
   • Go to Settings > Tools > SonarLint > Settings. Add a SonarQube / SonarCloud connection.
   • Pick a name. Select SonarCloud. Click Next.
   • Create a token. This requires you to be logged in to SonarCloud. Click Next.
     • Clicking "Generate Token" will direct you to the SonarCloud website. Log in with your GitHub account to connect to the VerCors project.
     • When generating a token on the SonarCloud web interface, the token will only be displayed once. Make sure to copy it, and paste it into the respective field in IntelliJ.
   • Select "University of Twente". Click Next.
   • Deselect "Receive notifications" (except if you would like to have notifications). Click Next.
   • Click Finish
3. Select a Sonarcloud project for SonarLint.
   • Go to Settings > Tools > SonarLint > Project Settings > Bind to SonarQube / SonarCloud.
   • In the dropdown menu of Project binding > Connections:, select the connection you set up in Step 2.
   • In the dropdown menu of Project binding > Project:, select the VerCors project.
   • Click Apply (to save the settings but keep the window open) or OK (to save the settings and close the dialogue).

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 (in MB) 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". I only encountered this on initial setup of the project and sometimes "accidentally" fixed it, so please let me know if you did set these options, but got this result anyway.
• The run configuration says: "Warning: Main method not found in class vct.main.Main". You might not have compiled vercors for the first time yet, or forgot to tick "use sbt shell for project reload, builds".