Gobra-mode for Emacs

Adds support to Emacs for Gobra. Features include:

Syntax highlighting for Gobra keywords.
Interface to the Gobra executable.
Error highlighting after running Gobra.
Jump to error functionality.
Interface for manipulating Gobra arguments.
Folding and unfolding ghost code blocks in .go files.

Installation

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 file.

(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>")

Usage

Default keybindings provided by the gobra minor mode:

C-c g v: Verifies the file corresponding to the current buffer.
C-c g c: Opens the generated Viper code in a new buffer.
C-c g a: Spawns a construction buffer through which the arguments passed to gobra are manipulated.
C-c g s: Gobra mode creates the command that Gobra should run serializing the arguments and copying it to the kill-ring. Useful if working with the sbt shell of Gobra directly.
C-c g f: Verify the function under the cursor only. This assumes the arguments explicitly have the current file for verification (not its directory or package).
C-c g h: Fold or unfold ghost code chunk under cursor (works for .go files where the comment syntax (// @) is used.
C-c g j: Unfold every folded piece of ghost code in the current buffer.

The construction buffer for the arguments can be used to set, unset or modify the existing arguments of Gobra. It contains a checklist of possible Gobra arguments for which the following operations are defined:

c: Set or unset the current argument. If the argument has itself arguments, the user is prompted to fill them.
a: Add arguments to an already set argument.
e: Spawn a buffer to edit the arguments of this argument by hand.
d: Print documentation about the current argument.
s: Save the current set of arguments (and their arguments) to a file.
l: Load a configuration from a file.
q: Exit and return to the Gobra buffer.
n - p: Move up and down.

When the verifier is running, it lives in an async command in a buffer by default called *Gobra Command Output*. That buffer also supports some extra functionality, namely:

n: Go to the next reported error.
p: Go to the previous reported error.
RET: Go to the location of the error reported under the cursor at the corresponding file. If the file is not open, it is opened. If the cursor is over an error of the Gobra implementation, RET opens the corresponding file where the exception was raised. This only works if gobra-development-path is set to point to the src directory of Gobra.

When the Gobra command terminates, the errors are highlighted in the already open buffers that are getting verified.

Minor mode

The minor mode can be enabled automatically when a .go file is opened with:

(add-hook 'go-mode-hook 'gobra-minor-mode)

Overriding Go mode hooks

gobra-mode is a derived mode from go-mode. This means that when opening a .gobra file the go-mode-hook functions will be invoked. This creates a problem for example with the use of LSP mode if it is configured to start automatically for go files because there is no LSP backend for Gobra. To override that hook, a local variable gobra-actions-before-go-mode is defined which holds a function with stuff to do before the go-mode hooked functions run. The following hack is then possible to stop LSP from starting in a Gobra buffer:

First define a buffer-local variable:

(defvar-local my/conditional-lsp-flag t)

Then define a function starting LSP when that variable is true:

(defun my/conditional-lsp ()
  (when my/conditional-lsp-flag
    (lsp)))

Hook this to go-mode instead of just LSP:

(add-hook go-mode-hook 'my/conditional-lsp)

Use the gobra-actions-before-go-mode variable to turn the local variable to nil:

(setq gobra-actions-before-go-mode
      (lambda ()
        (setq-local my/conditional-lsp-flag nil)))

Now whenever a .gobra file is opened, lsp won’t be invoked.