IDE Import

This document gives instructions on how to configure a development environment for VerCors, using either ⌄Intellij IDEA or ⌄Visual Studio Code. Most VerCors developers use Intellij IDEA. Although VerCors supports Windows, MacOs and other unixen, most developers use a Linux distribution, so the development experience is tested more thoroughly on Linux.

Basic setup

This section describes how to install the prerequisites in more detail and how to build and run VerCors from a terminal. The instructions after the basic setup were however tested only under these conditions:

• A fresh installation of Ubuntu 22.04
• IntelliJ IDEA Community Edition 2023.1.1

Ubuntu

Install required dependencies:

apt install curl git openjdk-17-jdk-headless

Note that VerCors will also work with later jdks – it is not necessary to install an older one. openjdk-17-jdk includes openjdk-17-jdk-headless.

Clone the VerCors repository (~500MB):

git clone ssh://[email protected]/utwente-fmt/vercors.git

If you get an error about access rights, please ensure:

• ~/.ssh/id_rsa.pub or another public key exists. If not, run ssh-keygen;
• The key in ~/.ssh/id_rsa.pub is associated to your github account. If not, visit https://github.com/settings/keys;
• You have push access to the VerCors repository. If not, contact a member of the team.

You can also simply clone VerCors as read-only:

git clone https://github.com/utwente-fmt/vercors.git

Move into the repository:

cd vercors

Compile VerCors:

./mill -j 0 vercors.main.compile

Run an example to verify your setup works:

./bin/vct examples/concepts/arrays/array.pvl

That's it! 🥳

MacOs

Yet to be written...

Windows

Install required dependencies(Git and OpenJDK17)

Skip this step if you already have them installed:

Run a command prompt with administrator privileges:

winget install Git.git
winget install ms-openjdk-17

Note that VerCors will also work with later jdks – it is not necessary to install an older one.

Restart the command prompt, navigate to the directory where you want to install VerCors and clone the VerCors repository (~500MB):

git clone ssh://[email protected]/utwente-fmt/vercors.git

If you get an error about access rights, please ensure:

• ~/.ssh/id_rsa.pub or another public key exists. If not, run ssh-keygen;
• The key in ~/.ssh/id_rsa.pub is associated to your github account. If not, visit https://github.com/settings/keys;
• You have push access to the VerCors repository. If not, contact a member of the team.

You can also simply clone VerCors as read-only:

git clone https://github.com/utwente-fmt/vercors.git

Move into the repository:

cd vercors

To be able to properly view the compilation messages hereafter, it is useful to enable colors for the terminal. To do this, first type "regedit" in the windows search bar and open the application. Then navigate to Computer\HKEY_CURRENT_USER\Console. Right-click the folder "Console" and click on New > Create DWORD (32-bit) Value and name it VirtualTerminalLevel. Click on the new DWORD value and set its value to 1.

Compile VerCors:

mill.bat -j 0 vercors.main.compile

Run an example to verify your setup works:

.\bin\vct examples\concepts\arrays\array.pvl

That's it! 🥳

IntelliJ IDEA

Requires ⌃Basic Setup

Install IntelliJ IDEA if you do not have it yet:

snap install --classic intellij-idea-community

Note: intellij-idea-ultimate is free for educational use. See e.g. here. It includes features that are useful to us, such as a profiler.

Install the Scala plugin, e.g. from the splash screen:

Open or import the VerCors project from the root of the repository (i.e. the vercors directory).

If you have not yet compiled VerCors at this point, importing may take approximately 5 minutes. It is also possible that importing fails with an error. In that case, let the synchronization finish fully, then go to Build > Reload BSP project (the ⟲ symbol).

Important: VerCors requires more stack memory than normal applications. It is recommended to increase it before adding any configurations

• Go to Run > Edit Configurations > Edit Configuration Templates
• Edit the Application template
• Go to Modidify options > Add VM options
• Enter -Xss20m in the VM options field
• Edit the ScalaTest template
• Enter -Xss20m in the VM options field

Set the JDK to version 17 or later in File > Project Structure > Project Settings > Project > SDK.

Running and Debugging VerCors

• Go to Run > Edit Configurations and add an Application configuration
• Set the classpath -cp to vercors
• Set the Main class to vct.main.Main (and not vct.main.Main$)
• If IntelliJ complains that it cannot find BuildInfo.buildinfo.properties, you may have to go to Modify Options > Add before launch task and activate Use BSP Environment. In the pop-up, you can just click ok (the target can be blank or filled, doesn't matter).
• Specifically for the IntelliJ Console you need to force enable progress messages with the program argument -p
• You can be asked to specify a file every time by adding $Prompt$ to the program arguments, or just append a file path relative to the vercors root directory.

In the end your configuration should look something like this:

Running the test suite

The test suite takes approximately 45 minutes to run on a modern machine. You may wish to push your changes to your branch at the main repository instead, so that the CI can run chunks of the test suite in parallel. This currently takes approximately 15 minutes instead.

You can create a ScalaTest run configuration automatically by right-clicking a directory or file containing tests, and then clicking Run 'ScalaTests in <directory or file>'. We currently do not have a way of running a single test in a file that contains multiple tests from within IntelliJ IDEA.

Unclear build errors

If the build error is not clear, it may be helpful to run mill directly from a terminal, e.g.:

./mill -j 0 vercors.compile

Running the IntelliJ build from a terminal

IntelliJ communicates with the mill build system to build VerCors. The scripts at ./bin/vct and bin\vct.cmd will ask mill how to run VerCors. Consequently, you can always run the most recent VerCors build from a terminal with this script.

VSCode

The author does not use VSCode, so apologies for any awkward instructions. Corrections are appreciated.

Requires ⌃Basic Setup

Install VSCode if you do not have it yet:

snap install --classic code

Install the Metals plugin by going to Ctrl+Shift+X > Scala (Metals) > Install

This will add a Metals symbol in the left tray.

Open the VerCors project from the root of the repository (i.e. the vercors directory) at File > Open Folder. When prompted by the Metals extension, click Import build.

If you hid the notification, it may be in your notifications on the bottom right. Alternatively you can click Import build from the Metals pane on the left.

To build VerCors, click Metals > Cascade compile.

Running and Debugging VerCors

Go to Run and Debug > Create a launch.json file. Then:

• Type "Scala" in the configurations array, and select Scala: run main class from the suggestions;
• Set mainClass to vct.main.Main;
• Specifically for the Debug Console you need to force enable progress messages with the program argument -p;
• Set the arguments, for example ["-p", "examples/concepts/arrays/array.pvl"];
• Set the JVM options to ["-Xss20m"].

Your launch configuration should look something like this:

{
    "version": "0.2.0",
    "configurations": [{
        "type": "scala",
        "request": "launch",
        "name": "VerCors",
        "mainClass": "vct.main.Main",
        "args": ["-p", "examples/concepts/arrays/array.pvl"],
        "jvmOptions": ["-Xss20m"],
        "env": {}
    }]
}

Running the test suite

The test suite takes approximately 45 minutes to run on a modern machine. You may wish to push your changes to your branch at the main repository instead, so that the CI can run chunks of the test suite in parallel. This currently takes approximately 15 minutes instead.

You can simply run tests yourself from the Test pane on the left (the ⚗ symbol).

Running the Metals build from a terminal

VSCode communicates with the mill build system to build VerCors. The scripts at ./bin/vct and bin\vct.cmd will ask mill how to run VerCors. Consequently, you can always run the most recent VerCors build from a terminal with this script.