Configuration

• Introduction
• Manual Installation
• ~package.el~ installation via MELPA
  • Install ~z3-mode~

Introduction

z3-mode provides an interactive development environment for checking the satisfiability of logical formula written in SMTLIBv2 with backends such as Z3.

Manual Installation

To install manually, check out this repository and add the following to your .emacs

(add-to-list 'load-path "/path/to/z3-mode/")
(autoload 'z3-mode "z3-mode" nil t)
(add-to-list 'auto-mode-alist '("\\.rs\\'" . z3-mode))

package.el installation via MELPA

It can be more convenient to use Emacs’s package manager to handle installation for you if you use many elisp libraries. If you have package.el but haven’t added MELPA, the community package source, yet, add this to ~/.emacs.d/init.el:

(require 'package)
(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)

Then do this to load the package listing:

M-x eval-buffer

M-x package-refresh-contents

If you use a version of Emacs prior to 24 that doesn’t include package.el, you can get it from here.

If you have an older ELPA package.el installed from tromey.com, you should upgrade in order to support installation from multiple sources. The ELPA archive is deprecated and no longer accepting new packages, so the version there (1.7.1) is very outdated.

Install z3-mode

One you have package.el, you can install z3-mode or any other modes by choosing them from a list:

M-x package-list-packages Now, to install packages, move your cursor to them and press i. This will mark the packages for installation. When you’re done with marking, press x, and ELPA will install the packages for you (under ~/.emacs.d/elpa/ ).

or using M-x package-install z3-mode