Dafny for Visual Studio Code
This extension adds Dafny 3 support to Visual Studio Code. If you require Dafny 2 support, consider using the legacy extension. This VSCode plugin requires the Dafny language server (shipped with the Dafny release since v3.1.0). The plugin will install it automatically upon first use.
You can find examples below.
The plugin requires at least .NET Core 5.0 (the ASP.NET Core 5.0 runtime to be more specific) to run the Dafny Language Server. Please download a distribution from Microsoft. When you first open a Dafny file, the extension will prompt you to install .NET Core manually. The language server gets installed automatically.
Please note that in this new plugin version "automatic verification" is always on and a language server side feature.
Here are a few impressions of the features.
On the first start, the plugin will install the Dafny language server automatically.
Whenever a syntax, semantic, or verification error is present, the plugin will inform the user.
Compile and Run
Show Counter Example
Hover a symbol to get information about that symbol.
Type a dot to get a list of possible members of the accessed symbol.
If VSCode appears unresponsive, you may lower the verification frequency or disable it entirely.
Stuck at Verifying...
Under certain circumstances, the extension appears to be stuck at Verifying.... Until now, this has only been observed for Mac OSX and occurs due to a stack overflow in the language server.
To overcome this issue, set the environment variable
Dafny for Visual Studio Code is an MIT licensed open-source project that lives from code contributions.
We welcome your help! For a description of how you can contribute, as well as a list of issues you can work on, please visit the Dafny-VSCode GitHub repository.
To build Dafny VSCode locally, first clone this repository.
Change into the root directory of the previously cloned repository and install the node modules.
To build and debug using Visual Studio Code, install the TypeScript + Webpack Problem Matchers extension.
After the installation, open the root folder within VSCode and hit
Because the latest version of the plugin requires recent changes to the Dafny language server, you will then need to change the
To create a VSIX package of the previously built sources, install the VSCode Extension Manager globally:
Now create the package through the CLI:
We use ESLint with the TypeScript plugin to ensure code consistency across the whole source. Install the ESLint extension in VSCode to have live feedback. Alternatively, you can check your code from the command line by running