13. Writing More Lisp Code

You may want to add some extra features to your instance of Proof General which are not supported in the generic core. To do this, you can use the settings described above, plus a small number of fundamental functions in Proof General which you can consider as exported in the generic interface. Be careful using more functions than are mentioned here because the internals of Proof General may change between versions.

13.1 Default values for generic settings

Several generic settings are defined using defpgcustom in ‘proof-config.el’. This introduces settings of the form <PA>-name for each proof assistant PA.

To set the default value for these settings in prover-specific cases, you should use the special defpgdefault macro:

Macro: defpgdefault

Set default for the proof assistant specific variable <PA>-sym to value.
This should be used in prover-specific code to alter the default values for prover specific settings.

Usage: (defpgdefault SYM value)

In your prover-specific code you can simply use the setting <PA>-sym directly, i.e., write myprover-home-page.

In the generic code, you can use a macro, writing (proof-ass home-page) to refer to the <PA>-home-page setting for the currently running instance of Proof General.

See section Configuration variable mechanisms, for more details on this mechanism.

13.2 Adding prover-specific configurations

Apart from the generic settings, your prover instance will probably need some specific customizable settings.

Defining new prover-specific settings using customize is pretty easy. You should do it at least for your prover-specific user options.

The code in ‘proof-site.el’ provides each prover with two customization groups automatically (based on the name of the assistant): <PA> for user options for prover PA and <PA>-config for configuration of prover PA. Typically <PA>-config holds settings which are constants but which may be nice to tweak.

The first group appears in the menu

  ProofGeneral -> Advanced -> Customize -> <PA> 

The second group appears in the menu:

  ProofGeneral -> Internals -> <PA> config

A typical use of defcustom looks like this:

(defcustom myprover-search-page
  "http://findtheorem.myprover.org"
  "URL of search web page for myprover."
  :type 'string
  :group 'myprover-config)

This introduces a new customizable setting, which you might use to make a menu entry, for example. The default value is the string "http://findtheorem.myprover.org".

13.3 Useful variables

In ‘proof-site’, some architecture flags are defined. These can be used to write conditional pieces of code for different Emacs and operating systems. They are referred to mainly in ‘proof-compat’ (which helps to keep the architecture and version dependent code in one place).

13.4 Useful functions and macros

The recommended functions you may invoke are these:

• Any of the interactive commands (i.e. anything you can invoke with M-x, including all key-bindings)
• Any of the internal functions and macros mentioned below

To insert text into the current (usually script) buffer, the function proof-insert is useful. There’s also a handy macro proof-defshortcut for defining shortcut functions using it.

Function: proof-insert text

Insert text into the current buffer.
text may include these special characters:

%p - place the point here after input

Any other %-prefixed character inserts itself.

Macro: proof-defshortcut

Define shortcut function FN to insert string, optional keydef KEY.
This is intended for defining proof assistant specific functions. string is inserted using ‘proof-insert’, which see. KEY is added onto proof assistant map.

The function proof-shell-invisible-command is a useful utility for sending a single command to the process. You should use this to implement user-level or internal functions rather than attempting to directly manipulate the proof action list, or insert into the shell buffer.

Function: proof-shell-invisible-command cmd &optional wait invisiblecallback &rest flags

Send cmd to the proof process.
The cmd is ‘invisible’ in the sense that it is not recorded in buffer. cmd may be a string or a string-yielding expression.

Automatically add ‘proof-terminal-string’ if necessary, examining ‘proof-shell-no-auto-terminate-commands’.

By default, let the command be processed asynchronously. But if optional wait command is non-nil, wait for processing to finish before and after sending the command.

In case cmd is (or yields) nil, do nothing.

invisiblecallback will be invoked after the command has finished, if it is set. It should probably run the hook variables ‘proof-state-change-hook’.

flags are additional flags to put onto the ‘proof-action-list’. The flag 'invisible is always added to flags.

There are several handy macros to help you define functions which invoke proof-shell-invisible-command.

Macro: proof-definvisible

Define function FN to send string to proof assistant, optional keydef KEY.
This is intended for defining proof assistant specific functions. string is sent using ‘proof-shell-invisible-command’, which see. string may be a string or a function which returns a string. KEY is added onto proof assistant map.

Macro: proof-define-assistant-command

Define FN (docstring DOC): check if cmdvar is set, then send body to prover.
body defaults to cmdvar, a variable.

Macro: proof-define-assistant-command-witharg

Define FN (arg) with DOC: check cmdvar is set, prompt a string and eval body.
The body can contain occurrences of arg. cmdvar is a variable holding a function or string. Automatically has history.

Function: proof-format-filename string filename

Format string by replacing quoted chars by escaped version of filename.

%e uses the canonicalized expanded version of filename (including directory, using ‘default-directory’ – see ‘expand-file-name’).

%r uses the unadjusted (possibly relative) version of filename.

%m (’module’) uses the basename of the file, without directory or extension.

%s means the same as %e.

Using %e can avoid problems with dumb proof assistants who don’t understand ~, for example.

For all these cases, the escapes in ‘proof-shell-filename-escapes’ are processed.

If string is in fact a function, instead invoke it on filename and return the resulting (string) value.

This document was generated on April 20, 2024 using texi2html 1.82.