Dafny 2 for Visual Studio Code (Legacy)
⚠ This plugin targets Dafny 2 and is deprecated. Consider switching to its successor that supports Dafny 3.0.0.
This extension adds Dafny support to Visual Studio Code.
Features
- Compile and run
.dfy files.
- Automatic installation of the newest Dafny version.
- Automatic verification as one types.
- Errors, warnings and hints are shown through the VSCode interface.
- When there are no errors, you get a 👍 on the status bar.
- Syntax highlighting thanks to sublime-dafny. See file
LICENSE_sublime-dafny.rst for license.
- Display counter example for failing proof.
- IntelliSense for classes and CodeLens showing method references.
You can find more Examples below.
Shortcuts
| Shortcut |
Description |
Ctrl+Shift+B or ⇧+⌘+B |
Compile .dfy file to .dll or .exe, if there is a Main method |
F5 |
Compile and run, if the source file has a Main method |
F7 |
Show CounterExample |
F8 |
Hide CounterExample |
Tasks
Choose Tasks -> Run Task... to run one of the following:
| Task |
Description |
Install DafnyServer |
Downloads and installs the DafnyServer and sets the dafny.dafnyServerPath accordingly |
Uninstall DafnyServer |
Uninstalls the DafnyServer |
Restart DafnyServer |
Restarts the DafnyServer |
Requirements
- The plugin needs a .NET runtime to run the DafnyServer. If you are not on Windows, please download a distribution from Mono.
- Note: When you first open a Dafny file, the extension will prompt you to automatically install Dafny and Mono.
- In case you would like the plugin to use a different Dafny distribution, set the path to the
DafnyServer.exe file via the dafny.dafnyServerPath user setting.
Extension Settings
| Setting |
Description |
Default |
dafny.basePath |
Absolute path to the Dafny binary directory (which contains DafnyServer.exe). |
|
dafny.monoExecutable |
Mono executable with absolute path. Only necessary if mono is not in system PATH (you'll get an error if that's the case). Ignored on Windows when useMono is false. |
|
dafny.useMono |
Only applicable to Windows! Requires .NET 4.5 or higher when set to false. |
false |
dafny.automaticVerification |
Verify as soon as the document is changed. When false, only verify on save. |
true |
dafny.automaticVerificationDelayMS |
Delay in ms to wait after a document change before verifying document. This avoids syntax errors while typing. Only relevant if automaticVerification is true. |
700 |
dafny.automaticShowCounterModel |
Show CounterModel automatically if a proof fails. Might cause performance issues if true. |
false |
dafny.serverVerifyArguments |
Additional arguments to pass to the "verify" command of the Dafny Server. E.g.["/timeLimit:40", "/vcsLoad:1"] |
[] |
Examples
Installation
On the first start the plugin asks you to install Dafny automatically.
Add null check
Some diagnostics can be directly inserted with a quickfix at the beginning of a line.
Compile and Run
Pressed F5 to compile and run the program.
Show Counter Example
Pressed F7 to show counter examples.
Contribute
This is a MIT licensed open-source project that lives from code contributions. All contributors are listed in our project readme.
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.
