This is a layer for working with Dafny, Boogie, and Z3 files using the boogie-friends package. It doesn’t do much other than installing that package and setting up vim-friendly keybindings.
To use this configuration layer, first clone the repository to
~/.emacs.d/private:
cd $HOME/.emacs.d/private
git clone https://github.com/dschoepe/spacemacs-boogie-friends ~/.emacs.d/private/boogie-friendsYou then need to add boogie-friends to the existing
dotspacemacs-configuration-layers list in ~/.spacemacs.
The following keybindings work in all modes (dafny-mode, boogie-mode, z3-smt2-mode)
| Key Binding | Description |
|---|---|
SPC m v | Rerun file verification (boogie-friends-verify) |
dafny-mode and boogie-mode only:
| Key Binding | Description |
|---|---|
SPC m t | Show verification trace (boogie-friends-trace) |
SPC m p | Generate tracing profile for function and run profile analyzer (boogie-friends-trace) |
dafny-mode only:
| Key Binding | Description |
|---|---|
SPC m d | Show verification trace (dafny-docs-open) |
SPC m a | Show translation to boogie (boogie-friends-translate) |
SPC m j | Jump to corresponding line in boogie file (dafny-jump-to-boogie) |