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 parameters.
• Various manipulations of ghost code blocks in .go files.

Installation

This package is under development (many changes may be non backwards compatible). Thus, it is not published in any package archives.

To install it, one must clone the repository:

git clone [email protected]:viperproject/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 parameters passed to gobra are manipulated.
• C-c g s: Gobra mode creates the command that Gobra should run serializing the parameters and copying it to the kill-ring. Useful if working with the sbt shell of Gobra directly.
• C-c g b: Gobra mode defines a hook called gobra-verification-hook. Anything added to that will be called when verification finishes if the variable gobra-enable-verification-hook is non-nil. Useful if you want to be notified after a large verification task finishes. This command toggles the variable gobra-enable-verification-hook.
• C-c g k: Toggles the popping up of the verification buffer when verifying something. Useful if you need the verification buffer on a frame on a different monitor.
• C-c g l: Verify the function under the cursor only. This assumes the parameters 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.
• C-c g f: Format the ghost code chunk under cursor. This currently converts //@ annotations to // @ annotations and aligns the arguments of the keywords preserves, requires and ensures in function contracts.
• C-c g C-f: Format ghost code in the whole buffer.
• C-c g p: Jump to previous ghost code chunk.
• C-c g n: Jump to next ghost code chunk.

If Hydra is installed, pressing C-c g will spawn a hydra menu with all these commands available.

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

• c: Set or unset the current parameter. If the parameter has itself arguments, the user is prompted to fill them.
• a: Add arguments to an already set parameter.
• d: Delete the current argument of a parameter.
• ?: Print documentation about the current parameter.
• s: Save the current set of parameters (and their arguments) to a file.
• l: Load a configuration from a file.
• q: Exit and return to the Gobra buffer.
• j: Jump to a specific parameter.
• 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)

Note that the minor mode is responsible for almost everything so it should be enabled for .gobra files as well. gobra-mode however is a major mode deriving from go-mode so hooking the minor mode to go-mode will enable it for Gobra buffers as well.

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.

Who do I talk to?

This project is maintained by Dionisios Spiliopoulos