Kind 2 Extension for VS Code

This extension provides basic support for the Lustre programming language with Kind 2 Model Checker annotations.

Requirements

Java 8+ run-time.

• Debian-based Linux: sudo apt install openjdk-17-jdk
• RHEL-based Linux: sudo yum install java-17-openjdk
• MacOS: brew install --cask temurin
• Windows: install a JDK from Adoptium, or run winget install EclipseAdoptium.Temurin.17.JDK.

Since pre-release 0.15.0, Windows is supported natively; running the extension through WSL2 is no longer required or supported.

Windows through WSL2 (version 0.13.0 and earlier)

Running the extension inside WSL2 is required for version 0.13.0 and earlier, and uses the Linux build. WSL1 is not supported. Follow these steps to run the extension on WSL2 (Windows 10 version 1903+ or Windows 11):

1. Install WSL
   • Windows 10 version 2004+ and Windows 11: Run wsl --install in PowerShell or Windows Command Prompt and restart your machine.
   • Windows 10 version 1903+: follow the manual steps in this page.
2. Follow the instructions on this page to finish setting up your WSL2 Linux environment.
3. Install the Remote - WSL extension for VS Code.
4. Click on the green rectangle in the bottom-left corner of the VS Code window. A prompt will appear on the top. click on new WSL window.
5. Press Ctrl+Shift+` to open a Linux terminal on the new VS Code window. Use the terminal to install the Java run-time.
6. In the same VS Code window, go to the extension view in the activity bar to the left and lookup the Kind 2 extension. Click Install in WSL: <distro name>. Refer to this page to learn more about using WSL with VS Code.

Options

The extension supports modular and compositional analysis modes of Kind 2. Those modes are disabled by default. Follow the steps below to enable them (and other Kind 2 configurations):

1. Go to VS Code settings.
2. Click on Kind 2 under the Extensions section.
3. Enable modular, compositional, and/or other options.
4. If you prefer an editor interface, click on icon at the top-right corner of the settings page to switch the JSON view:
5. Type kind2. VS Code will provide an autocompletion menu with available Kind 2 options. Select the options you want to configure and save your changes.

You can also enable/disable modular and compositional analysis modes from Kind's view. Click on their icons to enable them.

Main Features

• Syntax highlighting for Lustre and Kind 2 constructs.
• Go-to-definition for top level declarations.
• Document symbol outline.
• Syntax and type error reports.
• Model checking.
• Simulations.
• Counter-examples for falsified properties.
• Raw output of calling Kind 2 through the terminal.