Dafny Workbench provides users with an environment in which they can easily write and verify Dafny programs.
Atom → File → Settings → Install → dafny-workbench
, or:
$ apm install dafny-workbench
Note:
pkill
is used to terminate Dafny and its descendants (e.g. Z3), make sure it can be resolved against the PATH
variable.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 dafnyExecutablePath
setting.
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 → dafny-workbench
.
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:
dafny-workbench:start-dafny
dafny-workbench:stop-dafny
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. .dfy
for 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:
dafnyExecutablePath
points directly (and only) to the Dafny executable, so no wrapper script and no options (define those in dafnyExecutableArguments
).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.