Dafny Workbench provides users with an environment in which they can easily write and verify Dafny programs.
Atom → File → Settings → Install →
$ apm install dafny-workbench
pkillis used to terminate Dafny and its descendants (e.g. Z3), make sure it can be resolved against the
By default, the Dafny executable is resolved against the
PATH variable. If the location of the tool's binary is added to the path, there's no need to change its
Additionally, one may change the
dafnyExecutableArguments (options) passed to Dafny. By default, the first line (banner) is excluded and compilation is turned off.
It is possible to change these settings in the Settings View:
Atom → File → Settings → Packages →
Alternatively, change them via Atom's
config.json, for example:
"dafny-workbench":executableSettings:# The location of the Dafny binary. By default it is resolved against the PATH variable.dafnyExecutablePath: "/path/to/dafny"# Comma separated list of options to pass to the Dafny binary. Execute `dafny /help` in your terminal to see which options are allowed.dafnyExecutableArguments: ["/nologo""/compile:0"]
The following commands are available via the Command Palette if a Dafny file is open in the active editor:
By default, no keybindings are setup. They can be added to your
keymap.cson, for example:
'atom-text-editor[data-grammar~="source"][data-grammar~="dafny"]':'ctrl-shift-B': 'dafny-workbench:start-dafny''ctrl-shift-alt-B': 'dafny-workbench:stop-dafny'
When you open a file that is associated with the language grammar of the desired verification tool (e.g.
language-dafny), the verification tool will be run on the editor's content. Since the verification tools do not accept input from
stdin, the package writes a copy of the file buffer to the OS's temporary folder each time a change is made to provide continuous verification, without the need to save a file.
Q: I am having trouble getting Dafny to run. What should I do?
A: A few tips:
dafnyExecutablePathpoints directly (and only) to the Dafny executable, so no wrapper script and no options (define those in
If you are on a Unix system and have to use a wrapper script, make sure the
dafny-workbench package can pass the options, as well as the file path to the script. The following example has been confirmed to work on a Mac (note the absence of quotes around
$*, this is important):
#!/usr/bin/env bashmono /path/to/Dafny.exe $*
Good catch. Let us know what about this package looks wrong to you, and we'll investigate right away.