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.

Shared setup

This section describes how to install the prerequisites in more detail. The instructions after the shared setup were however tested only under these conditions:

• A fresh installation of Ubuntu 22.04

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.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

Yet to be written...

IntelliJ IDEA

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$)
• 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