dafny-vscode

Dafny support for Visual Studio Code. This project was forked into Dafny-VSCode, where development continued - use that instead. Development of this branch stopped in 2016 and there is only rudimentary integratiion of Dafny.

Features

• Provides .dfy language id to vscode.
• Spawns a DafnyServer in the background and sends veification requests upon opening and saving Dafny files.
• Errors, warnings and hints are shown through the vscode interface. When there are no errors, you get a thumbup on the status bar.
• Syntax highlighting thanks to sublime-dafny. See file LICENSE_sublime-dafny.rst for license.
• Left hand side status bar item provides information about the current file.
• Right hand size status bar item relates to the state of the DafnyServer.

Requirements - Installation guide

• A C# runtime to run DafnyServer. Mono should be supported on all platforms that vscode runs on. On windows, you may also use .net - see config below.
• Binary dafny distribution, which contains DafnyServer.exe and its dependencies - path must be specified in config.
• The path to the DafnyServer.exe set in the user configuration as dafny.dafnyServerPath (see the File menu on Windows and GNU+Linux, Code menu on OSX).

Extension Settings

The following are necessary:

• dafny.dafnyServerPath: absolute DafnyServer.exe path.

The following are optional:

• dafny.monoPath: Absolute path to mono binary. Only required if mono isn't found in PATH (you'll get an error if that's the case).
• dafny.useMono: Only applicable to Windows; requires .net 4.0 or higher when false. Attempts to launch dafny process directly when set to false

Release Notes

• 0.1.2: Refactored/tweaked UI code, Added dafny.restartDafnyServer ("Restart Dafny Server") command.
• 0.1.0: Added syntax highlighting, tested on Ubuntu and OSX.
• 0.0.3: Getting mono from PATH when monoPath isn't set.
• 0.0.2: Fixed readme and license, added use animation.
• 0.0.1: Initial release, some half baked features turned off.

TODO

• add restart server action.
• atomatic verification as one types (with 'deboucing' waiting period).
• syntax highlighting (see if you can adapt sublime-dafny).
• context aware suggestiions.
• full context awareness, code completion.