14. Internals of Proof General

This chapter sketches some of the internal functions and variables of Proof General, to help developers who wish to understand or modify the code.

Most of the documentation below is generated automatically from the comments in the code. Because Emacs lisp is interpreted and self-documenting, the best way to find your way around the source is inside Emacs once Proof General is loaded. Read the source files, and use functions such as C-h v and C-h f.

The code is split into files. The following sections document the important files, kept in the ‘generic/’ subdirectory.

14.1 Spans

Spans are an abstraction of Emacs overlays originally used to help bridge the gulf between GNU Emacs and XEmacs. See the file ‘lib/span.el’. XEmacs calls these extents which is a name still used in some parts of the code.

14.2 Proof General site configuration

The file ‘proof-site.el’ contains the initial configuration for Proof General for the site (or user) and the choice of provers.

The first part of the configuration is to set proof-home-directory to the directory that ‘proof-site.el’ is located in, or to the variable of the environment variable PROOFGENERAL_HOME if that is set.

Variable: proof-home-directory: Directory where Proof General is installed.
Based on where the file ‘proof-site.el’ was loaded from. Falls back to consulting the environment variable ‘PROOFGENERAL_HOME’ if proof-site.el couldn’t know where it was executed from.

Further directory variables allow the files of Proof General to be split up and installed across a system if need be, rather than under the proof-home-directory root.

Variable: proof-images-directory: Where Proof General image files are installed. Ends with slash.

Variable: proof-info-directory: Where Proof General Info files are installed. Ends with slash.

After defining these settings, we define a mode stub for each proof assistant enabled. The mode stub will autoload Proof General for the right proof assistant when a file is visited with the corresponding extension. The proof assistants enabled are the ones listed in the proof-assistants setting.

Variable: proof-assistants

Choice of proof assistants to use with Proof General.
A list of symbols chosen from: ‘coq’ ‘easycrypt’ ‘phox’ ‘qrhl’ ‘pgshell’ ‘pgocaml’ ‘pghaskell’. If nil, the default will be ALL available proof assistants.

Each proof assistant defines its own instance of Proof General, providing session control, script management, etc. Proof General will be started automatically for the assistants chosen here. To avoid accidently invoking a proof assistant you don’t have, only select the proof assistants you (or your site) may need.

You can select which proof assistants you want by setting this variable before ‘proof-site.el’ is loaded, or by setting the environment variable ‘PROOFGENERAL_ASSISTANTS’ to the symbols you want, for example "coq easycrypt". Or you can edit the file ‘proof-site.el’ itself.

Note: to change proof assistant, you must start a new Emacs session.

The file ‘proof-site.el’ also defines a version variable.

Variable: proof-general-version: Version string identifying Proof General release.

14.3 Configuration variable mechanisms

The file ‘proof-config.el’ defines the configuration variables for Proof General, including instantiation parameters and user options. See previous chapters for details of its contents. Here we mention some conventions for declaring user options.

Global user options and instantiation parameters are declared using defcustom as usual. User options should have ‘*’ as the first character of their docstrings (standard Emacs convention) and live in the customize group proof-user-options. See ‘proof-config.el’ for the groups for instantiation parameters.

User options which are generic (having separate instances for each prover) and instantiation parameters (by definition generic) can be declared using the special macro defpgcustom. It is used in the same way as defcustom, except that the symbol declared will automatically be prefixed by the current proof assistant symbol.

Macro: defpgcustom

Define a new customization variable <PA>-sym for the current proof assistant.
This is intended for defining settings which are useful for any prover, but which the user may require different values of across provers.

The function proof-assistant-<SYM> is also defined, which can be used in the generic portion of Proof General to access the value for the current prover.

Arguments args are as for ‘defcustom’, which see. If a :group argument is not supplied, the setting will be added to the internal settings for the current prover (named <PA>-config).

In specific instances of Proof General, the macro defpgdefault can be used to give a default value for a generic setting.

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)

All new instantiation variables are best declared using the defpgcustom mechanism (old code may be converted gradually). Customizations which are liable to be different for different instances of Proof General are also best declared in this way. An example is the use of X Symbol, controlled by PA-x-symbol-enable, since it works poorly or not at all with some provers.

To access the generic settings, the following four functions and macros are useful.

Macro: proof-ass: Return the value for SYM for the current prover.
This macro should only be invoked once a specific prover is engaged.

Macro: proof-ass-sym: Return the symbol for SYM for the current prover. SYM not evaluated.
This macro should only be called once a specific prover is known.

Macro: proof-ass-symv: Return the symbol for SYM for the current prover. SYM evaluated.
This macro should only be invoked once a specific prover is engaged.

If changing a user option setting amounts to more than just setting a variable (it may have some dynamic effect), we can set the custom-set property for the variable to the function proof-set-value which does an ordinary set-default to set the variable, and then calls a function with the same name as the variable, to do whatever is necessary according to the new value for the variable.

There are several settings which can be switched on or off by the user, which use this proof-set-value mechanism. They are controlled by boolean variables with names like proof-foo-enable, and appear at the start of the customize group proof-user-options. They should be edited by the user through the customization mechanism, and set in the code using customize-set-variable.

In proof-utils.el there is a handy macro, proof-deftoggle, which constructs an interactive function for toggling boolean customize settings. We can use this to make an interactive function proof-foo-toggle to put on a menu or bind to a key, for example.

This general scheme is followed as far as possible, to give uniform behaviour and appearance for boolean user options, as well as interfacing properly with the customize mechanism.

Function: proof-set-value sym value

Set a customize variable using ‘set-default’ and a function.
We first call ‘set-default’ to set sym to value. Then if there is a function sym (i.e. with the same name as the variable sym), it is called to take some dynamic action for the new setting.

If there is no function sym, we try stripping ‘proof-assistant-symbol’ and adding "proof-" instead to get a function name. This extends proof-set-value to work with generic individual settings.

The dynamic action call only happens when values change: as an approximation we test whether proof-config is fully-loaded yet.

Macro: proof-deftoggle: Define a function VAR-toggle for toggling a boolean customize setting VAR.
The toggle function uses ‘customize-set-variable’ to change the variable. othername gives an alternative name than the default <VAR>-toggle. The name of the defined function is returned.

14.4 Global variables

Global variables are defined in ‘proof.el’. The same file defines a few utility functions and some triggers to load in the other files.

Variable: proof-script-buffer: The currently active scripting buffer or nil if none.

Variable: proof-shell-buffer: Process buffer where the proof assistant is run.

Variable: proof-response-buffer: The response buffer.

Variable: proof-goals-buffer: The goals buffer.

Variable: proof-buffer-type: Symbol for the type of this buffer: 'script, 'shell, 'goals, or 'response.

Variable: proof-included-files-list

List of files currently included in proof process.
This list contains files in canonical truename format (see ‘file-truename’).

Whenever a new file is being processed, it gets added to this list via the ‘proof-shell-process-file’ configuration settings. When the prover retracts a file, this list is resynchronised via the ‘proof-shell-retract-files-regexp’ and ‘proof-shell-compute-new-files-list’ configuration settings.

Only files which have been fully processed should be included here. Proof General itself will automatically add the filenames of a script buffer which has been completely read when scripting is deactivated. It will automatically remove the filename of a script buffer which is completely unread when scripting is deactivated.

NB: Currently there is no generic provision for removing files which are only partly read-in due to an error, so ideally the proof assistant should only output a processed message when a file has been successfully read.

Variable: proof-shell-proof-completed: Flag indicating that a completed proof has just been observed.
If non-nil, the value counts the commands from the last command of the proof (starting from 1).

Variable: proof-shell-error-or-interrupt-seen: Flag indicating that an error or interrupt has just occurred.
Set to 'error or 'interrupt if one was observed from the proof assistant during the last group of commands.

14.5 Proof script mode

The file ‘proof-script.el’ contains the main code for proof script mode, as well as definitions of menus, key-bindings, and user-level functions.

Proof scripts have two important variables for the locked and queue regions. These variables are local to each script buffer (although we only really need one queue span in total rather than one per buffer).

Variable: proof-locked-span: The locked span of the buffer.
Each script buffer has its own locked span, which may be detached from the buffer. Proof General allows buffers in other modes also to be locked; these also have a non-nil value for this variable.

Variable: proof-queue-span: The queue span of the buffer. May be detached if inactive or empty.
Each script buffer has its own queue span, although only the active scripting buffer may have an active queue span.

Various utility functions manipulate and examine the spans. An important one is proof-init-segmentation.

Function: proof-init-segmentation: Initialise the queue and locked spans in a proof script buffer.
Allocate spans if need be. The spans are detached from the buffer, so the regions are made empty by this function. Also clear list of script portions.

For locking files loaded by a proof assistant, we use the next function.

Function: proof-complete-buffer-atomic buffer

Ensure buffer marked completely processed, completing with a single step.

If buffer already contains a locked region, only the remainder of the buffer is closed off atomically (although undo for the initial portion is unlikely to work, the decoration may be worth retaining).

This works for buffers which are not in proof scripting mode too, to allow other files loaded by proof assistants to be marked read-only.

Atomic locking is instigated by the next function, which uses the variables proof-included-files-list documented earlier (see section Handling Multiple Files and see section Global variables).

Function: proof-register-possibly-new-processed-file file &optional informprover noquestions

If informprover is non-nil, the proof assistant will be told about this, to co-ordinate with its internal file-management. (Otherwise we assume that it is a message from the proof assistant which triggers this call). In this case, the user will be queried to save some buffers, unless noquestions is non-nil.

No action is taken if the file is already registered.

A warning message is issued if the register request came from the proof assistant and Emacs has a modified buffer visiting the file.

(Unlocking is done by proof-shell-process-urgent-message-retract together with proof-restart-buffers.)

An important pair of functions activate and deactivate scripting for the current buffer. A change in the state of active scripting can trigger various actions, such as starting up the proof assistant, or altering proof-included-files-list.

Command: proof-activate-scripting &optional nosaves queuemode

Ready prover and activate scripting for the current script buffer.

The current buffer is prepared for scripting. No changes are necessary if it is already in Scripting minor mode. Otherwise, it will become the new active scripting buffer, provided scripting can be switched off in the previous active scripting buffer with ‘proof-deactivate-scripting’.

Activating a new script buffer is a good time to ask if the user wants to save some buffers; this is done if the user option ‘proof-query-file-save-when-activating-scripting’ is set and provided the optional argument nosaves is non-nil.

The optional argument queuemode relaxes the test for a busy proof shell to allow one which has mode queuemode. In all other cases, a proof shell busy error is given.

Finally, the hooks ‘proof-activate-scripting-hook’ are run. This can be a useful place to configure the proof assistant for scripting in a particular file, for example, loading the correct theory, or whatever. If the hooks issue commands to the proof assistant (via ‘proof-shell-invisible-command’) which result in an error, the activation is considered to have failed and an error is given.

Command: proof-deactivate-scripting &optional forcedaction

Try to deactivate scripting for the active scripting buffer.

Aims to set ‘proof-script-buffer’ to nil and turn off the modeline indicator. No action is required there is no active scripting buffer.

We make sure that the active scripting buffer either has no locked region or a full locked region (everything in it has been processed). If this is not already the case, we question the user whether to retract or assert, or automatically take the action indicated in the user option ‘proof-auto-action-when-deactivating-scripting’.

If ‘proof-no-fully-processed-buffer’ is t there is only the choice to fully retract the active scripting buffer. In this case the active scripting buffer is retracted even if it was fully processed. Setting ‘proof-auto-action-when-deactivating-scripting’ to 'process is ignored in this case.

If the scripting buffer is (or has become) fully processed, and it is associated with a file, it is registered on ‘proof-included-files-list’. Conversely, if it is (or has become) empty, we make sure that it is not registered. This is to be certain that the included files list behaves as we might expect with respect to the active scripting buffer, in an attempt to harmonize mixed scripting and file reading in the prover.

This function either succeeds, fails because the user refused to process or retract a partly finished buffer, or gives an error message because retraction or processing failed. If this function succeeds, then ‘proof-script-buffer’ is nil afterwards.

The optional argument forcedaction overrides the user option ‘proof-auto-action-when-deactivating-scripting’ and prevents questioning the user. It is used to make a value for the ‘kill-buffer-hook’ for scripting buffers, so that when a scripting buffer is killed it is always retracted.

The function proof-segment-up-to is the main one used for parsing the proof script buffer. There are several variants of this function available corresponding to different parsing strategies; the appropriate one is aliased to proof-segment-up-to according to which configuration variables have been set.

If proof-script-sexp-commands is set, the choice is proof-script-generic-parse-sexp. item If only proof-script-command-end-regexp or proof-terminal-string are set, then the default is proof-script-generic-parse-cmdend.
If proof-script-command-start-regexp is set, the choice is proof-script-generic-parse-cmdstart.

The function proof-semis-to-vanillas uses proof-segment-up-to to convert a parsed region of the script into a series of commands to be sent to the proof assistant.

Function: proof-script-generic-parse-cmdend: For ‘proof-script-parse-function’ if ‘proof-script-command-end-regexp’ set.

Function: proof-script-generic-parse-cmdstart: For ‘proof-script-parse-function’ if ‘proof-script-command-start-regexp’ is set.

Function: proof-script-generic-parse-sexp: Used for ‘proof-script-parse-function’ if ‘proof-script-sexp-commands’ is set.

Function: proof-semis-to-vanillas semis &optional queueflags

Create vanilla spans for semis and a list for the queue.
Proof terminator positions semis has the form returned by the function ‘proof-segment-up-to’. The argument list is destroyed. The callback in each queue element is ‘proof-done-advancing’.

If the variable ‘proof-script-preprocess’ is set (to the name of a function), call that function to construct the first element of each queue item.

The optional queueflags are added to each queue item.

The function proof-assert-until-point is the main one used to process commands in the script buffer. It’s actually used to implement the assert-until-point, electric terminator keypress, and find-next-terminator behaviours. In different cases we want different things, but usually the information (i.e. are we inside a comment) isn’t available until we’ve actually run proof-segment-up-to (point), hence all the different options when we’ve done so.

Function: proof-assert-until-point &optional displayflags: Process the region from the end of the locked-region until point.

The main command for retracting parts of a script is proof-retract-until-point.

Function: proof-retract-until-point &optional undo-action displayflags

Set up the proof process for retracting until point.
This calculates the commands to undo to the current point within the locked region. If invoked outside the locked region, undo the last successfully processed command. See ‘proof-retract-target’.

After retraction has succeeded in the prover, the filter will call ‘proof-done-retracting’. If undo-action is non-nil, it will then be invoked on the region in the proof script corresponding to the proof command sequence. displayflags control output shown to user, see ‘proof-action-list’.

Before the retraction is calculated, we enforce the file-level protocol with ‘proof-activate-scripting’. This has a couple of effects:

1. If the file is completely processed, we have to re-open it for scripting again which may involve retracting other (dependent) files.

2. We may query the user whether to save some buffers.

Step 2 may seem odd – we’re undoing (in) the buffer, after all – but what may happen is that when scripting starts going forward again, we hit a command that loads other files, but the user hasn’t saved the latest edits. Therefore it is right to query saves here.

To clean up when scripting is stopped, a script buffer is killed, a file is retract (and thus must be unlocked), or the proof assistant exits, we use the functions proof-restart-buffers and proof-script-remove-all-spans-and-deactivate.

Function: proof-restart-buffers buffers: Remove all extents in buffers and maybe reset ‘proof-script-buffer’.
The high-level effect is that all members of buffers are completely unlocked, including all the necessary cleanup. No effect on a buffer which is nil or killed. If one of the buffers is the current scripting buffer, then ‘proof-script-buffer’ will deactivated.

Function: proof-script-remove-all-spans-and-deactivate: Remove all spans from scripting buffers via ‘proof-restart-buffers’.

14.6 Proof shell mode

The proof shell mode code is in the file ‘proof-shell.el’. Proof shell mode is defined to inherit from scomint-mode using define-derived-mode near the end of the file. The ‘scomint.el’ package stands for “simplified comint”, where comint-mode is the standard Emacs mode for running an embedded command interpreter. In scomint, many of the interactive commands have been removed to speed up the process handling, because it isn’t intended that the user interacts directly with the shell in Proof General.

The bulk of the code in the proof-shell package is concerned with sending code to and from the shell, and processing output for the associated buffers (goals and response).

Good process handling is a tricky issue. Proof General attempts to manage the process strictly, by maintaining a queue of commands to send to the process. Once a command has been processed, another one is popped off the queue and sent.

There are several important internal variables which control interaction with the process.

Variable: proof-shell-busy

A lock indicating that the proof shell is processing.

The lock notes that we are processing a queue of commands being sent to the prover, and indicates whether the commands correspond to script management from a buffer (rather than being ad-hoc query commands to the prover).

When processing commands from a buffer for script management, this will be set to the queue mode 'advancing or 'retracting to indicate the direction of movement.

When this is non-nil, ‘proof-shell-ready-prover’ will give an error if called with a different requested queue mode.

See also functions ‘proof-activate-scripting’ and ‘proof-shell-available-p’.

Variable: proof-marker: Marker in proof shell buffer pointing to previous command input.

Variable: proof-action-list

The main queue of things to do: spans, commands and actions.
The value is a list of lists of the form

   (span commands action [DISPLAYFLAGS])

which is the queue of things to do.

span is a region in the sources, where commands come from. Often, additional properties are recorded as properties of span.

commands is a list of strings, holding the text to be send to the prover. It might be the empty list if nothing needs to be sent to the prover, such as, for comments. Usually commands contains just 1 string, but it might also contains more elements. The text should be obtained with ‘(mapconcat ’identity commands " ")’, where the last argument is a space.

action is the callback to be invoked when this item has been processed by the prover. For normal scripting items it is ‘proof-done-advancing’, for retract items ‘proof-done-retracting’, but there are more possibilities (e.g. ‘proof-done-invisible’, ‘proof-shell-set-silent’, ‘proof-shell-clear-silent’ and ‘proof-tree-show-goal-callback’).

The displayflags are set for non-scripting commands or for when scripting should not bother the user. They may include

  'invisible                non-script command (‘proof-shell-invisible-command’)
  'no-response-display      do not display messages in response buffer
  'no-error-display         do not display errors/take error action
  'no-goals-display         do not goals in goals buffer
  'proof-tree-show-subgoal  item inserted by the proof-tree package
  'priority-action          item added via proof-add-to-priority-queue

Note that 'invisible does not imply any of the others. If flags are non-empty, interactive cues will be surpressed. (E.g., printing hints).

See the functions ‘proof-start-queue’ and ‘proof-shell-exec-loop’.

In Proof General 4.2 and earlier it was always the case that all items from the queue region were present in proof-action-list. Because of the new parallel background compilation for Coq, this is no longer the case. Prover specific code may now store items from the queue region somewhere else. To notify generic Proof General about this, it must set proof-second-action-list-active for the time where some queue items are missing from proof-action-list. In this case Proof General keeps the proof shell lock and the queue span even in case proof-action-list gets empty. Coq uses this feature to hold back Require commands and the following text until the asynchronous background compilation finishes.

Variable: proof-second-action-list-active

Signals that some items are waiting outside of ‘proof-action-list’.
If this is t it means that some items from the queue region are waiting for being processed in a place different from ‘proof-action-list’. In this case Proof General must behave as if ‘proof-action-list’ would be non-empty, when it is, in fact, empty.

This is used, for instance, for parallel background compilation for Coq: The Require command and the following items are not put into ‘proof-action-list’ and are stored somewhere else until the background compilation finishes. Then those items are put into ‘proof-action-list’ for getting processed.

Variable: pg-subterm-anns-use-stack

Choice of syntax tree encoding for terms.

If nil, prover is expected to make no optimisations. If non-nil, the pretty printer of the prover only reports local changes. For Coq 6.2, use t.

The function proof-shell-start is used to initialise a shell buffer and the associated buffers.

Command: proof-shell-start

Initialise a shell-like buffer for a proof assistant.
Does nothing if proof assistant is already running.

Also generates goal and response buffers.

If ‘proof-prog-name-ask’ is set, query the user for the process command.

The function proof-shell-kill-function performs the converse function of shutting things down; it is used as a hook function for kill-buffer-hook. Then no harm occurs if the user kills the shell directly, or if it is done more cautiously via proof-shell-exit. The function proof-shell-restart allows a less drastic way of restarting scripting, other than killing and restarting the process.

Function: proof-shell-kill-function: Function run when a proof-shell buffer is killed.
Try to shut down the proof process nicely and clear locked regions and state variables. Value for ‘kill-buffer-hook’ in shell buffer, called by ‘proof-shell-bail-out’ if process exits.

Command: proof-shell-exit &optional dont-ask

Query the user and exit the proof process.

This simply kills the ‘proof-shell-buffer’ relying on the hook function

‘proof-shell-kill-function’ to do the hard work. If optional argument dont-ask is non-nil, the proof process is terminated without confirmation.

The kill function uses ‘<PA>-quit-timeout’ as a timeout to wait after sending ‘proof-shell-quit-cmd’ before rudely killing the process.

This function should not be called if ‘proof-shell-exit-in-progress’ is t, because a recursive call of ‘proof-shell-kill-function’ will give strange errors.

Function: proof-shell-bail-out process event: Value for the process sentinel for the proof assistant process.
If the proof assistant dies, run ‘proof-shell-kill-function’ to cleanup and remove the associated buffers. The shell buffer is left around so the user may discover what killed the process. event is the string describing the change.

Command: proof-shell-restart

Clear script buffers and send ‘proof-shell-restart-cmd’.
All locked regions are cleared and the active scripting buffer deactivated.

If the proof shell is busy, an interrupt is sent with ‘proof-interrupt-process’ and we wait until the process is ready.

The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant process.

It is up to the proof assistant how much context is cleared: for example, theories already loaded may be "cached" in some way, so that loading them the next time round only performs a re-linking operation, not full re-processing. (One way of caching is via object files, used by Coq).

14.6.1 Input to the shell

Input to the proof shell via the queue region is managed by the functions proof-extend-queue and proof-shell-exec-loop.

Function: proof-extend-queue end queueitems: Extend the current queue with queueitems, queue end end.
To make sense, the commands should correspond to processing actions for processing a region from (buffer-queue-or-locked-end) to end. The queue mode is set to 'advancing

Function: proof-extend-queue end queueitems: Extend the current queue with queueitems, queue end end.
To make sense, the commands should correspond to processing actions for processing a region from (buffer-queue-or-locked-end) to end. The queue mode is set to 'advancing

Function: proof-shell-exec-loop

Main loop processing the ‘proof-action-list’, called from shell filter.

‘proof-action-list’ contains a list of (span command action [FLAGS]) lists.

If this function is called with a non-empty ‘proof-action-list’, the head of the list is the previously executed command which succeeded. We execute the callback (action span) on the first item, then (action span) on any following items which have null as their cmd components.

If a there is a next command after that, send it to the process.

If the action list becomes empty, unlock the process and remove the queue region.

The return value is non-nil if the action list is now empty or contains only invisible elements for Prooftree synchronization.

Input is actually inserted into the shell buffer and sent to the process by the low-level function proof-shell-insert.

Function: proof-shell-insert strings action &optional scriptspan

Insert strings at the end of the proof shell, call ‘scomint-send-input’.

strings is a list of strings (which will be concatenated), or a single string.

The action argument is a symbol which is typically the name of a callback for when each string has been processed.

This calls ‘proof-shell-insert-hook’. The arguments action and scriptspan may be examined by the hook to determine how to modify the string variable (exploiting dynamic scoping) which will be the command actually sent to the shell.

Note that the hook is not called for the empty (null) string or a carriage return.

We strip the string of carriage returns before inserting it and updating ‘proof-marker’ to point to the end of the newly inserted text.

Do not use this function directly, or output will be lost. It is only used in ‘proof-add-to-queue’ when we start processing a queue, and in ‘proof-shell-exec-loop’, to process the next item.

When Proof General is processing a queue of commands, the lock is managed using a couple of utility functions. You should not need to use these directly.

Function: proof-grab-lock &optional queuemode: Grab the proof shell lock, starting the proof assistant if need be.
Runs ‘proof-state-change-hook’ to notify state change. If queuemode is supplied, set the lock to that value.

Function: proof-release-lock: Release the proof shell lock. Clear ‘proof-shell-busy’.

14.6.2 Output from the shell

Two main functions deal with output, proof-shell-classify-output and proof-shell-process-urgent-message. In effect we consider the output to be two streams intermingled: the "urgent" messages which have "eager" annotations, as well as the ordinary ruminations from the prover.

The idea is to conceal as much irrelevant information from the user as possible; only the remaining output between prompts and after the last urgent message will be a candidate for the goal or response buffer. The internal variable proof-shell-urgent-message-marker tracks the last urgent message seen.

When output is grabbed from the prover process, the first action is to strip spurious carriage return characters from the end of lines, if proof-shell-strip-crs-from-output requires it. Then the output is stored into proof-shell-last-output, and its type is stored in proof-shell-last-output-kind. Output which is deferred or possibly discarded until the queue is empty is copied into proof-shell-delayed-output, with type proof-shell-delayed-output-kind. A record of the last prompt seen from the prover process is also kept, in proof-shell-last-prompt.

Variable: proof-shell-strip-crs-from-output: If non-nil, remove carriage returns (^M) at the end of lines from output.
This is enabled for cygwin32 systems by default. You should turn it off if you don’t need it (slight speed penalty).

Variable: proof-shell-last-prompt: A raw record of the last prompt seen from the proof system.
This is the string matched by ‘proof-shell-annotated-prompt-regexp’.

Variable: proof-shell-last-output: A record of the last string seen from the proof system.
This is raw string, for internal use only.

Variable: proof-shell-last-output-kind

A symbol denoting the type of the last output string from the proof system.
Specifically:

 'interrupt      An interrupt message
 'error          An error message
 'loopback       A command sent from the PA to be inserted into the script
 'response       A response message
 'goals          A goals (proof state) display
 'systemspecific Something specific to a particular system,
                  -- see ‘proof-shell-handle-output-system-specific’

The output corresponding to this will be in ‘proof-shell-last-output’.

See also ‘proof-shell-proof-completed’ for further information about the proof process output, when ends of proofs are spotted.

This variable can be used for instance specific functions which want to examine ‘proof-shell-last-output’.

Variable: proof-shell-last-output-kind

A symbol denoting the type of the last output string from the proof system.
Specifically:

 'interrupt      An interrupt message
 'error          An error message
 'loopback       A command sent from the PA to be inserted into the script
 'response       A response message
 'goals          A goals (proof state) display
 'systemspecific Something specific to a particular system,
                  -- see ‘proof-shell-handle-output-system-specific’

The output corresponding to this will be in ‘proof-shell-last-output’.

See also ‘proof-shell-proof-completed’ for further information about the proof process output, when ends of proofs are spotted.

This variable can be used for instance specific functions which want to examine ‘proof-shell-last-output’.

Variable: proof-shell-delayed-output-start: A record of the start of the previous output in the shell buffer.
The previous output is held back for processing at end of queue.

Variable: proof-shell-delayed-output-end: A record of the start of the previous output in the shell buffer.
The previous output is held back for processing at end of queue.

Variable: proof-shell-delayed-output-flags: A copy of the ‘proof-action-list’ flags for ‘proof-shell-delayed-output’.

Function: proof-shell-handle-immediate-output cmd start end flags

See if the output between start and end must be dealt with immediately.
To speed up processing, PG tries to avoid displaying output that the user will not have a chance to see. Some output must be handled immediately, however: these are errors, interrupts, goals and loopbacks (proof step hints/proof by pointing results).

In this function we check, in turn:

  ‘proof-shell-interrupt-regexp’
  ‘proof-shell-error-regexp’
  ‘proof-shell-proof-completed-regexp’
  ‘proof-shell-result-start’

Other kinds of output are essentially display only, so only dealt with if necessary.

To extend this, set ‘proof-shell-handle-output-system-specific’, which is a hook to take particular additional actions.

This function sets variables: ‘proof-shell-last-output-kind’, and the counter ‘proof-shell-proof-completed’ which counts commands after a completed proof.

Function: proof-shell-handle-delayed-output

Display delayed goals/responses, when queue is stopped or completed.
This function handles the cases of ‘proof-shell-output-kind’ which are not dealt with eagerly during script processing, namely 'response and 'goals types.

This is useful even with empty delayed output as it will empty the buffers.

The delayed output is in the region [proof-shell-delayed-output-start,proof-shell-delayed-output-end].

If no goals classified output is found, the whole output is displayed in the response buffer.

If goals output is found, the last matching instance, possibly bounded by ‘proof-shell-end-goals-regexp’, will be displayed in the goals buffer (and may be further analysed by Proof General).

Any output that appears before the last goals output (but after messages classified as urgent, see ‘proof-shell-filter’) will also be displayed in the response buffer.

For example, if output has this form:

  messsage-1
  goals-1
  message-2
  goals-2
  junk

then goals-2 will be displayed in the goals buffer, and message-2 in the response buffer. junk will be ignored.

Notice that the above alternation (and separation of junk) can only be distinguished if both ‘proof-shell-start-goals-regexp’ and ‘proof-shell-end-goals-regexp’ are set. With just the start goals regexp set, goals-2 junk will appear in the goals buffer and no response output would occur.

The goals and response outputs are copied into ‘proof-shell-last-goals-output’ and ‘proof-shell-last-response-output’ respectively.

The value returned is the value for ‘proof-shell-last-output-kind’, i.e., 'goals or 'response.

Variable: proof-shell-urgent-message-marker: Marker in proof shell buffer pointing to end of last urgent message.

Function: proof-shell-process-urgent-message start end

Analyse urgent message between start and end for various cases.

Cases are: trace output, included/retracted files, cleared goals/response buffer, variable setting, xml-encoded pgip response, theorem dependency message or interactive output indicator.

If none of these apply, display the text between start and end.

The text between start and end should be a string that starts with text matching ‘proof-shell-eager-annotation-start’ and ends with text matching ‘proof-shell-eager-annotation-end’.

The main processing point which triggers other actions is proof-shell-filter. It is called from proof-shell-filter-wrapper, which itself is called from an ordinary Emacs process filter inside the simplified comint library that is distributed with Proof General (in lib/scomint.el).

Function: proof-shell-filter

Master filter for the proof assistant shell-process.
A function for ‘scomint-output-filter-functions’.

Deal with output and issue new input from the queue. This is an important internal function. The output must be collected from ‘proof-shell-buffer’ for the following reason. This function might block inside ‘process-send-string’ when sending input to the proof assistant or to prooftree. In this case Emacs might call the process filter again while the previous instance is still running. ‘proof-shell-filter-wrapper’ detects and delays such calls but does not buffer the output.

Handle urgent messages first. As many as possible are processed, using the function ‘proof-shell-process-urgent-messages’.

If a prompt is seen, run ‘proof-shell-filter-manage-output’ on the output between the new prompt and the last input (position of ‘proof-marker’) or the last urgent message (position of ‘proof-shell-urgent-message-marker’), whichever is later. For example, in this case:

 PROMPT> input
 output-1
 urgent-message-1
 output-2
 urgent-message-2
 output-3
 PROMPT>

‘proof-marker’ points after input.

‘proof-shell-urgent-message-marker’ points after urgent-message-2, after both urgent messages have been processed by ‘proof-shell-process-urgent-messages’. Urgent messages always processed; they are intended to correspond to informational notes that the prover makes to inform the user or interface on progress.

In this case, the ordinary outputs output-1 and output-2 are ignored; only output-3 will be processed by ‘proof-shell-filter-manage-output’.

Error or interrupt messages are expected to terminate an interactive output and appear last before a prompt and will always be processed. Error messages and interrupt messages are therefore not considered as urgent messages.

The first time that a prompt is seen, ‘proof-marker’ is initialised to the end of the prompt. This should correspond with initializing the process. After that, ‘proof-marker’ is only changed when input is sent in ‘proof-shell-insert’.

Function: proof-shell-filter-manage-output start end

Subroutine of ‘proof-shell-filter’ for output between start and end.

First, we invoke ‘proof-shell-handle-immediate-output’ which classifies and handles output that must be dealt with immediately.

Other output (user display) is only displayed when the proof action list becomes empty, to avoid a confusing rapidly changing output that slows down processing.

After processing the current output, the last step undertaken by the filter is to send the next command from the queue.

Function: proof-shell-filter-wrapper str-do-not-use

Wrapper for ‘proof-shell-filter’, protecting against parallel calls.
In Emacs a process filter function can be called while the same filter is currently running for the same process, for instance, when the filter blocks on I/O. This wrapper protects the main entry point, ‘proof-shell-filter’ against such parallel, overlapping calls.

The argument str-do-not-use contains the most recent output, but is discarded. ‘proof-shell-filter’ collects the output from ‘proof-shell-buffer’ (where it is inserted by ‘scomint-output-filter’), relieving this function from the task to buffer the output that arrives during parallel, overlapping calls.

14.7 Debugging

To debug Proof General, it may be helpful to set the configuration variable proof-general-debug.

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.

For more information about debugging Emacs lisp, consult the Emacs Lisp Reference Manual. I recommend using the source-level debugger edebug.

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