dev

Setup

To setup the extension for first time use, run the following command:

./configure.sh

This will install Z3, Kind, the language server for Kind, the interpreter, and other dependencies. There are several development workflows depending on which component of the extension should be modified. The steps to follow after modifying each tool is mentioned below.

Update Z3

1. Manually download and unzip the glibc and osx assets from the releases page of Z3.
2. Copy glibc z3 executable to linux/z3 and osx z3 executable to macos/z3.
3. Remove the downloaded and unzipped assets.
4. Follow the Package and Publish instructions to publish a new release of the extension.

Update Kind 2

1. Manually download and extract the linux and macos assets from the releases page of Kind 2.
2. Copy linux kind2 executable to linux/kind2 and macos kind2 executable to macos/kind2.
3. Remove the downloaded and extracted assets.
4. Follow the Package and Publish instructions to publish a new release of the extension.

Debugging errors/crashes after updating Kind 2

The most likely reasons for the extension to crash after updating kind2 are:

• A bug in the JSON printer of kind.
• A modification in the JSON printer that breaks the Java API JSON parser.

In either case, the following steps can help debug the error:

1. Run both the VS Code client and server in debugging mode (TODO: add instructions link).
2. Follow the steps that recreate the error/crash up until before the last step in the Extension Development Host instance of VS Code.
3. Put a breakpoint in line 179 in Result.java. The breakpoint should be in kind2-language-server VS Code workspace and not kind2-java-api. To access the file from kind2-language-server VS Code workspace, click on any instance of Result in Kind2LanguageServer.java and press F12.
4. Execute the last step that reproduces the error/crash in the Extension Development Host instance of VS Code.
5. The last step should trigger the breakpoint and cause debugger for kind2-language-server to pause execution in line 179 in Results.java. The variable json should contain the JSON output of Kind.
6. Continue execution step-by-step until you find the line causing the problem or press continue button to let the program continue execution until an exception triggers the debugger to stop.
7. Fix the error and follow the steps in the section below to update the extension (if the Java API is modified).

Update the Java API for Kind 2

1. Publish a new release of the API to Maven Central. Wait for the new release to appear in Maven Central website.
2. Update the server's build.gradle file to use the new verion of the API.
3. Release a new version of the server on GitHub.
4. Extract the new release to kind-language-server. The executable should be in kind2-language-server/bin/kind2-language-server.
5. Follow the Package and Publish instructions to publish a new release of the extension.

Update the LSP server

1. Release a new version of the server.
2. Extract the new release to kind-language-server. The executable should be in kind2-language-server/bin/kind2-language-server.
3. Follow the Package and Publish instructions to publish a new release of the extension.

Debugging errors/crashes after updating API or server

1. Run both the VS Code client and server in debugging mode.
2. If the error is logical (i.e., not a crash/exception), put a breakpoint in the relevent line(s).
3. Follow the steps that reproduces the error/crash in the Extension Development Host instance of VS Code.
4. The breakpoint/exception should trigger the debugger to stop.
5. Fix the error.

Update the VS Code Client

1. Follow the Package and Publish instructions to publish a new release of the extension.

Debugging errors/crashes after updating client

1. Run only the VS Code client in debugging mode.
2. If the error is logical (i.e., not a crash/exception), put a breakpoint in the relevent line(s).
3. Follow the steps that reproduces the error/crash in the Extension Development Host instance of VS Code.
4. The breakpoint/exception should trigger the debugger to stop.
5. Fix the error.