Linter package with support for the program verification tools Dafny, Chalice and Boogie, provided that for each desired tool its grammar (language package) is installed (and, of course, the tool itself).
An example of successful verification:
An example of unsuccessful verification:
Atom → File → Settings → Install →
$ apm install linter-verification
By default, each supported verification tool 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
executableArguments (options) passed to the verification tool. By default, the first line (banner) is excluded as this adds needless overhead. For Dafny, compilations are turned off for similar reasons.
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:
"linter-verification":executableSettings:# By default the `dafny` binary is resolved from the path variable.dafnyExecutablePath: "/path/to/dafny"# Execute `dafny /help` for all possible options.dafnyExecutableArguments: ["/nologo""/compile:0"]
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.
Experimental support for the Owicki-Gries method of verification of parallel programs is provided by
dafny-transpiler. When a Dafny file is opened and the first line contains
// Use Owicki-Gries., the transpiler will be invoked before the file is passed to Dafny, so that Dafny verifies the transpiled output. Since it can be beneficial to inspect the transpiled output, this file is written to the same directory as the original file.
The FAQ assumes Dafny is the intended verification tool, but typically the questions and answers are also applicable to Chalice and Boogie.
Q: When I open a Dafny file I briefly see 'pending', but after that nothing is shown in the linter panel. No success message and no errors. What gives?
A: This likely means that the Dafny executable is not being called correctly or returns unexpected output.
dafnyExecutablePathpoints directly (and only) to the Dafny executable, so no wrapper script and no options (define those in
linter-verificationpackage 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 $*
Q: When I open a Dafny file with the experimental Owicki-Gries annotations I do not see linter messages, but when I open a normal Dafny file I do. How come?
A: Make sure the linter error panel's scope is set to project in the settings of the
linter package. When the transpiler is invoked the linter message points to the transpiled file to provide the ability to click on error messages and jump to the correct line in the transpiled file.
Q: When I open or create a new Dafny file and add
// Use Owicki-Gries. as first line of the file, the transpiler does not run. Why not?
A: Currently the first line is only checked upon opening a file. Reopen the file and the transpiler should be invoked.
Good catch. Let us know what about this package looks wrong to you, and we'll investigate right away.