Home

Awesome

Dafny 2 VSCode (Legacy) Marketplace Downloads Count

⚠ This plugin targets Dafny 2 and is deprecated. Consider switching to its successor that supports Dafny 3.0.0.

This repository contains the infrastructure necessary to support Dafny for Visual Studio Code.

To add Dafny to VSCode, please go to the Visual Studio Marketplace.

masterdevelop
Build Status<br>VSCode MarketplaceBuild Status<br>Sounarcloud

Architecture

The infrastructure consists of a Dafny language server, which can be found in the server directory, and a VS Code extension, which in turn can be found in the client directory. These components communicate with each other using the Language Server Protocol (LSP).

Dafny VSode Architecture

Contribute

We welcome all contributions! Please create a pull request and we will take care of releasing a new version when appropriate.

How-To

Setup

It is pretty simple to contribute to this plugin. All it takes is having Visual Studio Code and npm installed. Simply clone this repository and switch into the new folder. On the command line, execute one of the following scripts:

These scripts install node dependencies and start code for both the server and client.

If all the commands succeeded, the language server part and the client part of the plugin are opened in two different Visual Studio Code editors and installs all the dependencies.

🛈 It is necessary that the code command is available in your PATH. On the Mac, this is usually not given. If it is missing, have a look at this tutorial.

⚠️ Having the extension installed via the Visual Studio Marketplace (along with a Dafny installation via the extension), can lead to conflicts with your locally built extension. It is therefore recommended to uninstall all previous installations of the extension from Visual Studio Code.

Compile

In the server editor, press CTRL+Shift+b or ⇧+⌘+B to compile. The task that is started also watches file changes and recompiles automatically after saving.

To try out the changes, go to the client editor and press F5. A new instance of Visual Studio Code will be started that has the Dafny plugin running and ready for testing. Sometimes, Visual Studio Code does not recognize changes and does not apply them to the running test instance. If this is the case, simply close and restart the test instance, the changes should then be applied.

Tests and Linting

Make sure that your changes don't break the existing tests in the client/test folder. You can run the tests with npm test while in the client folder. For this to work, you have to set environment variable DAFNY_PATH on your system to your Dafny release (without a "/" at the end of the path).

Alternatively, you can execute tests with docker (Linux & macOS only) using scripts/test-docker.bash.

If you add new features, please make sure to include unit tests to cover as much code as possible.

To get some code-consistency, we check against tslint in all automated builds. Please check that your client and server complies: tslint --project ..

Release

To release a new version of Dafny VSCode, follow the description in RELEASE.md.

License

Dafny VSCode is released under the MIT License. Note that by submitting a Pull Request, you agree to release your changes under this license.

Contributors