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

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.

1. Make a directory called ‘myassistant/’ under the Proof General home directory proof-home-directory, to put the specific customization and associated files in.
2. Add a file ‘myassistant.el’ to the new directory.
3. Edit ‘proof-site.el’ to add a new entry to the 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.

4. Define the new Proof General modes in ‘myassistant.el’, by setting configuration variables to customize the behaviour of the generic modes.

Variable: 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 ‘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.

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 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 section 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).

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: 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 section 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.

This document was generated on October 4, 2024 using texi2html 1.82.