Skip to content

dschoepe/spacemacs-boogie-friends

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

2 Commits
 
 
 
 

Repository files navigation

boogie-friends layer for spacemacs

Table of Contents

Description

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.

Install

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-friends

You then need to add boogie-friends to the existing dotspacemacs-configuration-layers list in ~/.spacemacs.

Key bindings

The following keybindings work in all modes (dafny-mode, boogie-mode, z3-smt2-mode)

Key BindingDescription
SPC m vRerun file verification (boogie-friends-verify)

dafny-mode and boogie-mode only:

Key BindingDescription
SPC m tShow verification trace (boogie-friends-trace)
SPC m pGenerate tracing profile for function and run profile analyzer (boogie-friends-trace)

dafny-mode only:

Key BindingDescription
SPC m dShow verification trace (dafny-docs-open)
SPC m aShow translation to boogie (boogie-friends-translate)
SPC m jJump to corresponding line in boogie file (dafny-jump-to-boogie)

About

Spacemacs layer for working with Dafny, Boogie, and Z3

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published