Skip to content
Dafny for Visual Studio Code
Branch: develop
Clone or download
Latest commit 755898d Apr 5, 2019
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.vscode
client
scripts Fix release script Apr 5, 2019
server Update changelog and bump version to 0.17.0 Apr 5, 2019
.dockerignore Run tests with docker Nov 29, 2018
.gitignore Remove flow graph Apr 4, 2019
.travis.yml Remove sonar-scanner from external travis builds (pull requests) Feb 18, 2019
.vscodeignore
LICENSE
README.md Move Sonarcloud batch to develop branch Apr 1, 2019
RELEASE.md Change publisher id to correctnessLab Jan 7, 2019
addnullcheck.gif Added new animations May 19, 2017
compileandrun.gif Added new animations May 19, 2017
counterexample.gif Added new animations May 19, 2017
installation.gif Added new animations May 19, 2017
simpleassert.gif
sonar-project.properties Run tslint during test-docker and in sonar Jan 7, 2019
tslint.json Ignore console outputs in tslint Jan 7, 2019

README.md

Dafny VSCode Marketplace Downloads Count

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.

master develop
Build Status
VSCode Marketplace
Build Status
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).

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:

  • Linux & macOS: scripts/dev-env.bash
  • Windows: scripts\dev-env.bat

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

You can’t perform that action at this time.