Adds support to the Emacs IDE for Gobra.
This package is under heavy development. Thus, it is not published in any package archives.
To install it, one must clone the repository:
git clone git@github.com:Dspil/gobra-mode.git
Then, add the following lines in your init.el.
(add-to-list 'load-path "<gobra-mode repo path>")
(use-package gobra-mode)
(setq gobra-jar-path "<gobra jar file path>")
(setq gobra-z3-path "<Z3 executable path>")
Default keybindings:
C-c C-v
: Verifies the file corresponding to the current buffer.C-c C-g
: Goifies the current buffer.C-c C-c
: Opens the generated Viper code in a new buffer.C-c C-a
: Spawns a construction buffer through which the arguments passed to gobra are manipulated.