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.
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.
proof-home-directory
, to put the specific customization
and associated files in.
proof-assistants-table
variable. 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-table
for
more details.
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 ‘proof-home-directory
’.
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 ‘completion-ignored-extensions
’).
symbol is also used to form the name of the directory and elisp file for the mode, which will be
proof-home-directory/symbol/symbol.el
where proof-home-directory is the value of the
variable ‘proof-home-directory
’.
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.
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
appropriate.
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.
The macro 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 setq
. It
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 Overview of adding a new prover. After the call to
proof-easy-config
, the new modes myprover-mode
,
myprover-shell-mode
, myprover-response-mode
,
and 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 proof-easy-config
call.
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 demoisa-shell-extra-config
is then called as the final step when demoisa-shell-mode
is
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
proof-shell-config-done
).
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:
proof-mode
, proof-shell-mode
, proof-response-mode
,
and proof-goals-mode
.
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))
Where myass-shell-config
is a function which sets the
configuration variables for the shell (see Proof Shell Settings).
It’s important that each of your modes invokes one of the functions
proof-config-done
,
proof-shell-config-done
,
proof-response-config-done
, or
proof-goals-config-done
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
PA-mode
, PA-shell-mode
, etc.
See the file demoisa.el for an example of the four calls to
define-derived-mode
.
Aside: notice that the modes are selected using stub functions
inside proof-site.el
, which set the variables
proof-mode-for-script
, proof-mode-for-shell
, etc,
that actually select the right mode. These variables
are declared in pg-vars.el
.