8. Customizing Proof General

There are two ways of customizing Proof General: it can be customized for a user’s preferences using a particular proof assistant, or it can be customized by a developer to add support for a new proof assistant. The latter kind of customization we call instantiation, or adapting. See the Adapting Proof General manual for how to do this. Here we cover the user-level customization for Proof General.

There are two kinds of user-level settings in Proof General:

Settings that apply globally to all proof assistants.
those that can be adjusted for each proof assistant individually.

The first sort have names beginning with proof-. The second sort have names which begin with a symbol corresponding to the proof assistant: for example, isa-, coq-, etc. The symbol is the root of the mode name. See section Quick start guide, for a table of the supported modes. To stand for an arbitrary proof assistant, we write PA- for these names.

In this chapter we only consider the generic settings: ones which apply to all proof assistants (globally or individually). The support for a particular proof assistant may provide extra individual customization settings not available in other proof assistants. See the chapters covering each assistant for details of those settings.

8.1 Basic options

Proof General has some common options which you can toggle directly from the menu:

   Proof-General -> Quick Options

The effect of changing one of these options will be seen immediately (or in the next proof step). The window-control options on this menu are described shortly. See section Display customization.

To save the current settings for these options (only), use the Save Options command in the submenu:

   Proof-General -> Quick Options -> Save Options

or M-x customize-save-customized.

The options on this sub-menu are also available in the complete user customization options group for Proof General. For this you need to know a little bit about how to customize in Emacs.

8.2 How to customize

Proof General uses the Emacs customization library to provide a friendly interface. You can access all the customization settings for Proof General via the menu:

   Proof-General -> Advanced -> Customize

Using the customize facility is straightforward. You can select the setting to customize via the menus, or with M-x customize-variable. When you have selected a setting, you are shown a buffer with its current value, and facility to edit it. Once you have edited it, you can use the special buttons set, save and done. You must use one of set or save to get any effect. The save button stores the setting in your ‘.emacs’ file. The command M-x customize-save-customized or Emacs menubar item Options -> Save Options saves all settings you have edited.

A technical note. In the customize menus, the variable names mentioned later in this chapter may be abbreviated — the "proof-" or similar prefixes are omitted. Also, some of the option settings may have more descriptive names (for example, on and off) than the low-level lisp values (non-nil, nil) which are mentioned in this chapter. These features make customize rather more friendly than raw lisp.

You can also access the customize settings for Proof General from other (non-script) buffers. Use the menu:

   Options -> Customize Emacs -> Top-level Customization Group

and select the External and then Proof-General groups.

The complete set of customization settings will only be available after Proof General has been fully loaded. Proof General is fully loaded when you visit a script file for the first time, or if you type M-x load-library RET proof RET.

For more help with customize, see (emacs)Customization.

8.3 Display customization

By default, Proof General displays two buffers during scripting, in a split window on the display. One buffer is the script buffer. The other buffer is either the goals buffer (*goals*) or the response buffer (*response*). Proof General raises and switches between these last two automatically.

Proof General allows several ways to customize this default display model, by splitting the Emacs frames in different ways and maximising the amount of information shown, or by using multiple frames. The customization options are explained below; they are also available on the menu:

  Proof-General -> Quick Options -> Display

and you can save your preferred default.

If your screen is large enough, you may prefer to display all three of the interaction buffers at once. This is useful, for example, to see output from the proof-find-theorems command at the same time as the subgoal list. Set the user option proof-three-window-enable to make Proof General keep both the goals and response buffer displayed.

If you prefer to switch windows and buffers manually when you want to see the prover output, you can customize the user option proof-auto-raise-buffers to prevent the automatic behaviour. You can browse interaction output by hovering the mouse over the command regions in the proof script.

User Option: proof-auto-raise-buffers

If non-nil, automatically raise buffers to display latest output.
If this is not set, buffers and windows will not be managed by Proof General.

The default value is t.

User Option: proof-three-window-enable

Whether response and goals buffers have dedicated windows.
If non-nil, Emacs windows displaying messages from the prover will not be switchable to display other windows.

This option can help manage your display.

Setting this option triggers a three-buffer mode of interaction where the goals buffer and response buffer are both displayed, rather than the two-buffer mode where they are switched between. It also prevents Emacs automatically resizing windows between proof steps.

If you use several frames (the same Emacs in several windows on the screen), you can force a frame to stick to showing the goals or response buffer.

This option only takes effect if the frame height is bigger than 4 times ‘window-min-height’ (i.e., bigger than 16 with default values) because there must be enough space to create 3 windows.

The default value is t.

Sometimes during script management, there is no response from the proof assistant to some command. In this case you might like the empty response window to be hidden so you have more room to see the proof script. The setting proof-delete-empty-windows helps you do this.

User Option: proof-delete-empty-windows

If non-nil, automatically remove windows when they are cleaned.
For example, at the end of a proof the goals buffer window will be cleared; if this flag is set it will automatically be removed. If you want to fix the sizes of your windows you may want to set this variable to 'nil' to avoid windows being deleted automatically. If you use multiple frames, only the windows in the currently selected frame will be automatically deleted.

The default value is nil.

This option only has an effect when you have set proof-three-window-mode.

If you are working on a machine with a window system, you can use Emacs to manage several frames on the display, to keep the goals buffer displayed in a fixed place on your screen and in a certain font, for example. A convenient way to do this is via the user option

User Option: proof-multiple-frames-enable

Whether response and goals buffers have separate frames.
If non-nil, Emacs will make separate frames (screen windows) for the goals and response buffers, by altering the Emacs variable ‘special-display-regexps’.

The default value is nil.

Multiple frames work best when proof-delete-empty-windows is off and proof-three-window-mode is on.

Finally, there are two commands available which help to switch between buffers or refresh the window layout. These are on the menu:

  Proof-General -> Buffers

Command: proof-display-some-buffers: Display the response, trace, goals, or shell buffer, rotating.
A fixed number of repetitions of this command switches back to the same buffer. Also move point to the end of the response buffer if it’s selected. If in three window or multiple frame mode, display two buffers. The idea of this function is to change the window->buffer mapping without adjusting window layout.

Command: proof-layout-windows

Refresh the display of windows according to current display mode.

For multiple frame mode, this function obeys the setting of ‘pg-response-eagerly-raise’, which see.

For single frame mode:

- In two panes mode, this uses a canonical layout made by splitting Emacs windows in equal proportions. The splitting is vertical if Emacs width is smaller than ‘split-width-threshold’ and horizontal otherwise. You can then adjust the proportions by dragging the separating bars.

- In three pane mode, there are three display modes, depending

  where the three useful buffers are displayed: scripting
  buffer, goals buffer and response buffer.

  Here are the three modes:

  - vertical: the 3 buffers are displayed in one column.
  - hybrid: 2 columns mode, left column displays scripting buffer
    and right column displays the 2 others.
  - horizontal: 3 columns mode, one for each buffer (script, goals,
    response).

  By default, the display mode is automatically chosen by
  considering the current Emacs frame width: if it is smaller
  than ‘split-width-threshold’ then vertical mode is chosen,
  otherwise if it is smaller than 1.5 * ‘split-width-threshold’
  then hybrid mode is chosen, finally if the frame is larger than
  1.5 * ‘split-width-threshold’ then the horizontal mode is chosen.

  You can change the value of ‘split-width-threshold’ at your
  will.

  If you want to force one of the layouts, you can set variable
  ‘proof-three-window-mode-policy’ to 'vertical, 'horizontal or
  'hybrid.  The default value is 'smart which sets the automatic
  behaviour described above.

User Option: proof-shrink-windows-tofit

If non-nil, automatically shrink output windows to fit contents.
In single-frame mode, this option will reduce the size of the goals and response windows to fit their contents.

The default value is nil.

User Option: proof-colour-locked

If non-nil, colour the locked region with ‘proof-locked-face’.
If this is not set, buffers will have no special face set on locked regions.

The default value is t.

User Option: proof-output-tooltips

Non-nil causes Proof General to add tooltips for prover output.
Hovers will be added when this option is non-nil. Prover outputs can be displayed when the mouse hovers over the region that produced it and output is available (see ‘proof-full-annotation’). If output is not available, the type of the output region is displayed. Changes of this option will not be reflected in already-processed regions of the script.

The default value is nil.

8.4 User options

Here is a list of the important user options for Proof General, apart from the display options mentioned above.

User options can be set via the customization system already mentioned, via the old-fashioned M-x edit-options mechanism, or simply by adding setq’s to your ‘.emacs’ file. The first approach is strongly recommended.

Unless mentioned, all of these settings can be changed dynamically, without needing to restart Emacs to see the effect. But you must use customize to be sure that Proof General reconfigures itself properly.

User Option: proof-splash-enable

If non-nil, display a splash screen when Proof General is loaded.

The default value is t.

User Option: proof-electric-terminator-enable

If non-nil, use electric terminator mode.
If electric terminator mode is enabled, pressing a terminator will automatically issue ‘proof-assert-next-command’ for convenience, to send the command straight to the proof process. If the command you want to send already has a terminator character, you don’t need to delete the terminator character first. Just press the terminator somewhere nearby. Electric!

The default value is nil.

User Option: proof-next-command-insert-space

If non-nil, PG will use heuristics to insert newlines or spaces in scripts.
In particular, if electric terminator is switched on, spaces or newlines will be inserted as the user types commands to the prover.

The default value is t.

User Option: proof-toolbar-enable

If non-nil, display Proof General toolbar for script buffers.

The default value is t.

User Option: proof-query-file-save-when-activating-scripting

If non-nil, query user to save files when activating scripting.

Often, activating scripting or executing the first scripting command of a proof script will cause the proof assistant to load some files needed by the current proof script. If this option is non-nil, the user will be prompted to save some unsaved buffers in case any of them corresponds to a file which may be loaded by the proof assistant.

You can turn this option off if the save queries are annoying, but be warned that with some proof assistants this may risk processing files which are out of date with respect to the loaded buffers!

The default value is t.

User Option: PA-script-indent

If non-nil, enable indentation code for proof scripts.

The default value is t.

User Option: PA-one-command-per-line

If non-nil, format for newlines after each command in a script.

The default value is t.

Variable: proof-omit-proofs-option

Set to t to omit complete opaque proofs for speed reasons.
When t, complete opaque proofs in the asserted region are not sent to the proof assistant (and thus not checked). For files with big proofs this can drastically reduce the processing time for the asserted region at the cost of not checking the proofs. For partial and non-opaque proofs in the asserted region all proof commands are sent to the proof assistant.

Using a prefix argument for ‘proof-goto-point’ (M-x proof-goto-point) or ‘proof-process-buffer’ (M-x proof-process-buffer) temporarily disables omitting proofs.

User Option: proof-prog-name-ask

If non-nil, query user which program to run for the inferior process.

The default value is nil.

Variable: PA-prog-args

Arguments to be passed to ‘proof-prog-name’ to run the proof assistant.
If non-nil, will be treated as a list of arguments for ‘proof-prog-name’. Otherwise ‘proof-prog-name’ will be split on spaces to form arguments.

Remark: Arguments are interpreted strictly: each one must contain only one word, with no space (unless it is the same word). For example if the arguments are -x foo -y bar, then the list should be ’("-x" "foo" "-y" "bar"), notice that ’("-x foo" "-y bar") is wrong.

Variable: PA-prog-env: Modifications to ‘process-environment’ made before running ‘proof-prog-name’.
Each element should be a string of the form ENVVARNAME=value. They will be added to the environment before launching the prover (but not pervasively). For example for coq on Windows you might need something like: (setq coq-prog-env ’("HOME=C:\Program Files\Coq\"))

User Option: proof-prog-name-guess

If non-nil, use ‘proof-guess-command-line’ to guess ‘proof-prog-name’.
This option is compatible with ‘proof-prog-name-ask’. No effect if ‘proof-guess-command-line’ is nil.

The default value is nil.

User Option: proof-tidy-response

Non-nil indicates that the response buffer should be cleared often.
The response buffer can be set either to accumulate output, or to clear frequently.

With this variable non-nil, the response buffer is kept tidy by clearing it often, typically between successive commands (just like the goals buffer).

Otherwise the response buffer will accumulate output from the prover.

The default value is t.

User Option: proof-keep-response-history

Whether to keep a browsable history of responses.
With this feature enabled, the buffers used for prover responses will have a history that can be browsed without processing/undoing in the prover. (Changes to this variable take effect after restarting the prover).

The default value is nil.

User Option: pg-input-ring-size

Size of history ring of previous successfully processed commands.

The default value is 32.

User Option: proof-general-debug

Non-nil to run Proof General in debug mode.
This changes some behaviour (e.g. markup stripping) and displays debugging messages in the response buffer. To avoid erasing messages shortly after they’re printed, set ‘proof-tidy-response’ to nil. This is only useful for PG developers.

The default value is nil.

User Option: proof-follow-mode

Choice of how point moves with script processing commands.
One of the symbols: 'locked, 'follow, 'followdown, 'ignore.

If 'locked, point sticks to the end of the locked region. If 'follow, point moves just when needed to display the locked region end. If 'followdown, point if necessary to stay in writeable region If 'ignore, point is never moved after movement commands or on errors.

If you choose 'ignore, you can find the end of the locked using M-x proof-goto-end-of-locked

The default value is locked.

User Option: proof-auto-action-when-deactivating-scripting

If 'retract or 'process, do that when deactivating scripting.

With this option set to 'retract or 'process, when scripting is turned off in a partly processed buffer, the buffer will be retracted or processed automatically.

With this option unset (nil), the user is questioned instead.

Proof General insists that only one script buffer can be partly processed: all others have to be completely processed or completely unprocessed. This is to make sure that handling of multiple files makes sense within the proof assistant.

NB: A buffer is completely processed when all non-whitespace is locked (coloured blue); a buffer is completely unprocessed when there is no locked region.

For some proof assistants (such as Coq) fully processed buffers make no sense. Setting this option to 'process has then the same effect as leaving it unset (nil). (This behaviour is controlled by ‘proof-no-fully-processed-buffer’.)

The default value is nil.

User Option: proof-rsh-command

Shell command prefix to run a command on a remote host.
For example,

   ssh bigjobs

Would cause Proof General to issue the command ‘ssh bigjobs coqtop’ to start Coq remotely on our large compute server called ‘bigjobs’.

The protocol used should be configured so that no user interaction (passwords, or whatever) is required to get going. For proper behaviour with interrupts, the program should also communicate signals to the remote host.

The default value is nil.

8.5 Changing faces

The numerous fonts and colours that Proof General uses are configurable. If you alter faces through the customize menus (or the command M-x customize-face), only the particular kind of display in use (colour window system, monochrome window system, console, …) will be affected. This means you can keep separate default settings for each different display environment where you use Proof General.

As well as the faces listed below, Proof General may use the regular font-lock- faces (eg font-lock-keyword-face, font-lock-variable-name-face, etc) for fontifying the proof script or proof assistant output. These can be altered to your taste just as easily, but note that changes will affect all other modes which use them!

8.5.1 Script buffer faces

Face: proof-queue-face: Face for commands in proof script waiting to be processed.

Face: proof-locked-face: Face for locked region of proof script (processed commands).

Face: proof-script-sticky-error-face: Proof General face for marking an error in the proof script.

Face: proof-script-highlight-error-face: Proof General face for highlighting an error in the proof script.

Face: proof-mouse-highlight-face: General mouse highlighting face used in script buffer.

Face: proof-highlight-dependent-face: Face for showing (backwards) dependent parts.

Face: proof-highlight-dependency-face: Face for showing (forwards) dependencies.

Face: proof-declaration-name-face: Face for declaration names in proof scripts.
Exactly what uses this face depends on the proof assistant.

Face: proof-tacticals-name-face: Face for names of tacticals in proof scripts.
Exactly what uses this face depends on the proof assistant.

8.5.2 Goals and response faces

Face: proof-error-face: Face for error messages from proof assistant.

Face: proof-warning-face: Face for warning messages.
Warning messages can come from proof assistant or from Proof General itself.

Face: proof-debug-message-face: Face for debugging messages from Proof General.

Face: proof-boring-face: Face for boring text in proof assistant output.

Face: proof-active-area-face: Face for showing active areas (clickable regions), outside of subterm markup.

Face: proof-eager-annotation-face: Face for important messages from proof assistant.

The slightly bizarre name of the last face comes from the idea that while large amounts of output are being sent from the prover, some messages should be displayed to the user while the bulk of the output is hidden. The messages which are displayed may have a special annotation to help Proof General recognize them, and this is an "eager" annotation in the sense that it should be processed as soon as it is observed by Proof General.

8.6 Tweaking configuration settings

This section is a note for advanced users.

Configuration settings are the per-prover customizations of Proof General. These are not intended to be adjusted by the user. But occasionally you may like to test changes to these settings to improve the way Proof General works. You may want to do this when a proof assistant has a flexible proof script language in which one can define new tactics or even operations, and you want Proof General to recognize some of these which the default settings don’t mention. So please feel free to try adjusting the configuration settings and report to us if you find better default values than the ones we have provided.

The configuration settings appear in the customization group prover-config, or via the menu

    Proof-General -> Internals ->  Prover Config

One basic example of a setting you may like to tweak is:

Variable: proof-assistant-home-page: Web address for information on proof assistant.
Used for Proof General’s help menu.

Most of the others are more complicated. For more details of the settings, see Adapting Proof General for full details. To browse the settings, you can look through the customization groups prover-config, proof-script and proof-shell. The group proof-script contains the configuration variables for scripting, and the group proof-shell contains those for interacting with the proof assistant.

Unfortunately, although you can use the customization mechanism to set and save these variables, saving them may have no practical effect because the default settings are mostly hard-wired into the proof assistant code. Ones we expect may need changing appear as proof assistant specific configurations. For example, proof-assistant-home-page is set in the Coq code from the value of the customization setting coq-www-home-page. At present there is no easy way to save changes to other configuration variables across sessions, other than by editing the source code. (In future versions of Proof General, we plan to make all configuration settings editable in Customize, by shadowing the settings as prover specific ones using the PA- mechanism).

This document was generated on November 21, 2024 using texi2html 1.82.