This extension provides commands and related editor context-menu items to execute Dafny command-line executable in the terminal window.
Commands and Editor Context-Menu Items
Command and Context Menu Item
Description
Key Binding
Dafny CLI: Verify Current Symbol
Execute the Dafny verifier in the terminal with the parameter /proc set to the innermost function/method/lemma/constructor symbol enclosing the current cursor position. If no symbol is detected, then /proc is set to the word where the cursor is positioned.
Ctrl + Shift + v
Dafny CLI: Verify Current Symbol with Trace
As Dafny CLI: Verify Current Symbol, except that the /trace option is added when running the Dafny command-line executable
Ctrl + Shift + t
Dafny CLI: Verify File
Execute the Dafny verifier in the terminal window on the current file
Ctrl + Shift + Alt + v
Dafny CLI: Verify File With Trace
As Dafny CLI: Verify File, except that the /trace option is added when running the Dafny
Ctrl + Shift + Alt + t
Dafny CLI: Repeat Last
Runs the Dafny command-lin executable with the same options used during the last execution
Ctrl + Shift + r
Extension Settings
Setting
Description
dafny-cli.dafny-path
Path to the folder containing the Dafny executable
dafny-cli.extra-options
Command line options to use when running the Dafny executable
dafny-cli.dafny.commandPrefix
Prefix to the command to execute to run Dafny (useful for the environment where the Dafny executable is provided as parameter to mono)
dafny-cli.dafny.commandPostfix
Postfix to the command executed to run Dafny
dafny-cli.dafny.version_above_3_7_1
To be checked if the version of Dafny used is higher than 3.7.1
Known Issues
The plugin only works with workspaces created through the File -> Open Folder ... command.
If either the Dafny CLI: Verify Under Cursor or the Dafny CLI: Verify Under Cursor with Trace command is executed on a constructor method, then all the constructor methods in the current file will be verified, not only the one under the cursor.
