1. Beginning with a New Prover
Proof General has about 100 configuration variables which are set on a per-prover basis to configure the various features. It may sound like a lot but don’t worry! Many of the variables occur in pairs (typically regular expressions matching the start and end of some text), and you can begin by setting just a fraction of the variables to get the basic features of script management working. The bare minimum for a working prototype is about 25 simple settings.
For more advanced features you may need (or want) to write some Emacs Lisp. If you’re adding new functionality please consider making it generic for different proof assistants, if appropriate. When writing your modes, please follow the Emacs Lisp conventions, See (Elisp)Tips.
The configuration variables are declared in the file ‘generic/proof-config.el’. The details in the central part of this manual are based on the contents of that file, beginning in Menus, toolbar, and user-level commands, and continuing until Global Constants. Other chapters cover the details of configuring for multiple files and for supporting the other Emacs packages mentioned in the user manual (Support for other Packages). If you write additional Elisp code interfacing to Proof General, you can find out about some useful functions by reading Writing More Lisp Code. The last chapter of this manual describes some of the internals of Proof General, in case you are interested, maybe because you need to extend the generic core to do something new.
In the rest of this chapter we describe the general mechanisms for instantiating Proof General. We assume some knowledge of the content of the main Proof General manual.
|1.1 Overview of adding a new prover|
|1.2 Demonstration instance and easy configuration|
|1.3 Major modes used by Proof General|
1.1 Overview of adding a new prover
Each proof assistant supported has its own subdirectory under
proof-home-directory, used to store a root elisp file and any
other files needed to adapt the proof assistant for Proof General.
Here is how to go about adding support for a new prover.
- Make a directory called ‘myassistant/’ under the Proof General home
proof-home-directory, to put the specific customization and associated files in.
- Add a file ‘myassistant.el’ to the new directory.
- Edit ‘proof-site.el’ to add a new entry to the
proof-assistants-tablevariable. The new entry should look like this:
(myassistant "My Proof Assistant" "\\.myasst$")
The first item is used to form the name of the internal variables for the new mode as well as the directory and file where it loads from. The second is a string, naming the proof assistant. The third item is a regular expression to match names of proof script files for this assistant. See the documentation of
proof-assistant-tablefor more details.
- Define the new Proof General modes in ‘myassistant.el’, by setting configuration variables to customize the behaviour of the generic modes.
- User Option: proof-assistant-table
Proof General’s table of supported proof assistants.
This is copied from ‘
proof-assistant-table-default’ at load time, removing any entries that do not have a corresponding directory under ‘
Each entry is a list of the form
(symbol name file-extension [AUTOMODE-REGEXP] [IGNORED-EXTENSIONS-LIST])
The name is a string, naming the proof assistant. The symbol is used to form the name of the mode for the assistant, ‘SYMBOL-mode’, run when files with automode-regexp (or with extension file-extension) are visited. If present, ignored-extensions-list is a list of file-name extensions to be ignored when doing file-name completion (ignored-extensions-list is added to
symbol is also used to form the name of the directory and elisp file for the mode, which will be
where proof-home-directory is the value of the variable ‘
The default value is
((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (easycrypt "EasyCrypt" "ec" ".*\\.eca?") (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci")).
The final step of the description above is where the work lies. There
are two basic methods. You can write some Emacs lisp functions and
define the modes using the macro
define-derived-mode. Or you can
use the new easy configuration mechanism of Proof General 3.0 described
in the next section, which calls
define-derived-mode for you.
You still need to know which configuration variables should be set, and
how to set them.
The documentation below (and inside Emacs) should help with that, but the best way to begin might be to use an existing Proof General instance as an example.
1.2 Demonstration instance and easy configuration
Proof General is supplied with a demonstration instance for Isabelle which configures the basic features. This is a whittled down version of Isabelle Proof General, which you can use as a template to get support for a new assistant going. Check the directory ‘demoisa’ for the two files ‘demoisa.el’ and ‘demoisa-easy.el’.
The file ‘demoisa.el’ follows the scheme described in Major modes used by Proof General. It uses the Emacs Lisp macro
define-derived-mode to define the four modes for a Proof General
instance, by inheriting from the generic code. Settings which configure
Proof General are made by functions called from within each mode, as
The file ‘demoisa-easy.el’ uses a new simplified mechanism to
achieve (virtually) the same result. It uses the macro
proof-easy-config defined in ‘proof-easy-configl.el’ to make
all of the settings for the Proof General instance in one go, defining
the derived modes automatically using a regular naming scheme. No lisp
code is used in this file except the call to this macro. The minor
difference in the end result is that all the variables are set at once,
rather than inside each mode. But since the configuration variables are
all global variables anyway, this makes no real difference.
proof-easy-config is called like this:
(proof-easy-config myprover "MyProver" config_1 val_1 ... config_n val_n)
The main body of the macro call is like the body of a
contains pairs of variables and value settings. The first argument to
the macro is a symbol defining the mode root, the second argument is a
string defining the mode name. These should be the same as the first
part of the entry in
proof-assistant-table for your prover.
See section Overview of adding a new prover. After the call to
proof-easy-config, the new modes
myprover-goals-mode will be defined. The configuration
variables in the body will be set immediately.
This mechanism is in fact recommended for new instantiations of Proof General since it follows a regular pattern, and we can more easily adapt it in the future to new versions of Proof General.
Even Emacs Lisp experts should prefer the simplified mechanism. If you
want to set some buffer-local variables in your Proof General modes, or
invoke supporting lisp code, this can easily be done by adding functions
to the appropriate mode hooks after the
For example, to add extra settings for the shell mode for
demoisa, we could do this:
(defun demoisa-shell-extra-config () extra configuration ... ) (add-hook 'demoisa-shell-mode-hook 'demoisa-shell-extra-config)
The function to do extra configuration
is then called as the final step when
entered (be wary, this will be after the generic
proof-shell-config-done is called, so it will be too late to set
normal configuration variables which may be examined by
1.3 Major modes used by Proof General
There are four major modes used by Proof General, one for each type of
buffer it handles. The buffer types are: script, shell, response and
goals. Each of these has a generic mode, respectively:
The pattern for defining the major mode for an instance of Proof General
is to use
define-derived-mode to define a specific mode to inherit from
each generic one, like this:
(define-derived-mode myass-shell-mode proof-shell-mode "MyAss shell" nil (myass-shell-config) (proof-shell-config-done))
myass-shell-config is a function which sets the
configuration variables for the shell (see section Proof Shell Settings).
It’s important that each of your modes invokes one of the functions
once it has set its configuration variables. These functions
finalize the configuration of the mode.
The modes must be named standardly, replacing
proof- with the
prover’s symbol name,
PA-. In other words, you must define
See the file ‘demoisa.el’ for an example of the four calls to
Aside: notice that the modes are selected using stub functions
proof-site.el, which set the variables
that actually select the right mode. These variables
are declared in
This document was generated by Erik Martin-Dorel on June 2, 2019 using texi2html 1.82.