4. Proof Shell Settings

The variables in this chapter concern the proof shell mode, and are the largest group. They are split into several subgroups. The first subgroup are commands invoked at various points. The second subgroup of variables are concerned with matching the output from the proof assistant. The final subgroup contains various hooks which you can set to add lisp customization to Proof General in various points (some of them are also used internally for behaviour you may wish to adjust).

Variables for configuring the proof shell are put into the customize group proof-shell.

These should be set in the shell mode configuration, before proof-shell-config-done is called.

To understand the way the proof assistant runs inside Emacs, you may want to refer to the comint.el (Command interpreter) package distributed with Emacs. This package controls several shell-like modes available in Emacs, including the proof-shell-mode and all specific shell modes derived from it.

4.1 Commands

Settings in this section configure Proof General with commands to send to the prover to activate certain actions.

Variable: proof-prog-name

System command to run the proof assistant in the proof shell.
May contain arguments separated by spaces, but see also the prover specific settings ‘<PA>-prog-args’ and ‘<PA>-prog-env’.

Remark: if ‘<PA>-prog-args’ is non-nil, then ‘proof-prog-name’ is considered strictly: it must contain only the program name with no option, spaces are interpreted literally as part of the program name.

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\"))

Variable: proof-shell-auto-terminate-commands: Non-nil if Proof General should try to add terminator to every command.
If non-nil, whenever a command is sent to the prover using ‘proof-shell-invisible-command’, Proof General will check to see if it ends with ‘proof-terminal-string’, and add it if not. If ‘proof-terminal-string’ is nil, this has no effect.

Variable: proof-shell-pre-sync-init-cmd

The command for configuring the proof process to gain synchronization.
This command is sent before Proof General’s synchronization mechanism is engaged, to allow customization inside the process to help gain syncrhonization (e.g. engaging special markup).

It is better to configure the proof assistant for this purpose via command line options if possible, in which case this variable does not need to be set.

4.2 Script input to the shell

Generally, commands from the proof script are sent verbatim to the proof process running in the proof shell. For historical reasons, carriage returns are stripped by default. You can set proof-shell-strip-crs-from-input to adjust that. For more sophisticated pre-processing of the sent string, you may like to set proof-shell-insert-hook.

Variable: proof-shell-strip-crs-from-input

If non-nil, replace carriage returns in every input with spaces.
This is enabled by default: it is appropriate for many systems based on human input, because several CR’s can result in several prompts, which may mess up the display (or even worse, the synchronization).

If the prover can be set to output only one prompt for every chunk of input, then newlines can be retained in the input.

Variable: proof-shell-insert-hook

Hook run by ‘proof-shell-insert’ before inserting a command.
Can be used to configure the proof assistant to the interface in various ways – for example, to observe or alter the commands sent to the prover, or to sneak in extra commands to configure the prover.

This hook is called inside a ‘save-excursion’ with the ‘proof-shell-buffer’ current, just before inserting and sending the text in the variable ‘string’. The hook can massage ‘string’ or insert additional text directly into the ‘proof-shell-buffer’. Before sending ‘string’, it will be stripped of carriage returns.

Additionally, the hook can examine the variable ‘action’. It will be a symbol, set to the callback command which is executed in the proof shell filter once ‘string’ has been processed. The ‘action’ variable suggests what class of command is about to be inserted, the first two are normally the ones of interest:

 'proof-done-advancing       A "forward" scripting command
 'proof-done-retracting      A "backward" scripting command
 'proof-done-invisible       A non-scripting command
 'proof-shell-set-silent     Indicates prover output has been surpressed
 'proof-shell-clear-silent   Indicates prover output has been restored
 'init-cmd                   Early initialization command sent to prover

Caveats: You should be very careful about setting this hook. Proof General relies on a careful synchronization with the process between inputs and outputs. It expects to see a prompt for each input it sends from the queue. If you add extra input here and it causes more prompts than expected, things will break! Extending the variable ‘string’ may be safer than inserting text directly, since it is stripped of carriage returns before being sent.

Example uses: Lego used this hook for setting the pretty printer width if the window width has changed; Plastic used it to remove literate-style markup from ‘string’.

See also ‘proof-script-preprocess’ which can munge text when it is added to the queue of commands.

4.3 Settings for matching various output from proof process

These settings control the way Proof General reacts to process output. The single most important setting is proof-shell-annotated-prompt-regexp, which must be set as part of the prover configuraton. This is used to configure the communication with the prover process.

Variable: pg-subterm-first-special-char: First special character.
Codes above this character can have special meaning to Proof General, and are stripped from the prover’s output strings. Leave unset if no special characters are being used.

Variable: proof-shell-annotated-prompt-regexp

Regexp matching a (possibly annotated) prompt pattern.

this IS THE most important setting TO configure!!

Output is grabbed between pairs of lines matching this regexp, and the appearance of this regexp is used by Proof General to recognize when the prover has finished processing a command.

To help speed up matching you may be able to annotate the proof assistant prompt with a special character not appearing in ordinary output, which should appear in this regexp.

Variable: proof-shell-error-regexp

Regexp matching an error report from the proof assistant.

We assume that an error message corresponds to a failure in the last proof command executed. So don’t match mere warning messages with this regexp. Moreover, an error message should not be matched as an eager annotation (see ‘proof-shell-eager-annotation-start’) otherwise it will be lost.

Error messages are considered to begin from ‘proof-shell-error-regexp’ and continue until the next prompt. The variable ‘proof-shell-truncate-before-error’ controls whether text before the error message is displayed.

The engine matches interrupts before errors, see ‘proof-shell-interrupt-regexp’.

It is safe to leave this variable unset (as nil).

Variable: proof-shell-interrupt-regexp

Regexp matching output indicating the assistant was interrupted.
We assume that an interrupt message corresponds to a failure in the last proof command executed. So don’t match mere warning messages with this regexp. Moreover, an interrupt message should not be matched as an eager annotation (see ‘proof-shell-eager-annotation-start’) otherwise it will be lost.

The engine matches interrupts before errors, see ‘proof-shell-error-regexp’.

It is safe to leave this variable unset (as nil).

Variable: proof-shell-truncate-before-error

Non-nil means truncate output that appears before error messages.
If nil, the whole output that the prover generated before the last error message will be shown.

NB: the default setting for this is t to be compatible with behaviour in Proof General before version 3.4. The more obvious setting for new instances is probably nil.

Interrupt messages are treated in the same way. See ‘proof-shell-error-regexp’ and ‘proof-shell-interrupt-regexp’.

Variable: proof-shell-proof-completed-regexp

Regexp matching output indicating a finished proof.

When output which matches this regexp is seen, we clear the goals buffer in case this is not also marked up as a ‘goals’ type of message.

We also enable the QED function (save a proof) and we may automatically close off the proof region if another goal appears before a save command, depending on whether the prover supports nested proofs or not.

Variable: proof-shell-start-goals-regexp

Regexp matching the start of the proof state output.
This is an important setting. Output between ‘proof-shell-start-goals-regexp’ and ‘proof-shell-end-goals-regexp’ will be pasted into the goals buffer and possibly analysed further for proof-by-pointing markup. If it is left as nil, the goals buffer will not be used.

The goals display starts at the beginning of the match on this regexp, unless it has a match group, in which case it starts at (match-end 1).

Variable: proof-shell-end-goals-regexp

Regexp matching the end of the proof state output, or nil.
This allows a shorter form of the proof state output to be displayed, in case several messages are combined in a command output.

The portion treated as the goals output will be that between the match on ‘proof-shell-start-goals-regexp’ (which see) and the start of the match on ‘proof-shell-end-goals-regexp’.

If nil, use the whole of the output from the match on ‘proof-shell-start-goals-regexp’ up to the next prompt.

Variable: proof-shell-assumption-regexp

A regular expression matching the name of assumptions.

At the moment, this setting is not used in the generic Proof General.

Future use may provide a generic implementation for ‘pg-topterm-goalhyplit-fn’, used to help parse the goals buffer to annotate it for proof by pointing.

4.4 Settings for matching urgent messages from proof process

Among the various dialogue messages that the proof assistant outputs during proof, Proof General can consider certain messages to be "urgent". When processing many lines of a proof, Proof General will normally supress the output, waiting until the final message appears before displaying anything to the user. Urgent messages escape this: typically they include messages that the prover wants the user to notice, for example, perhaps, file loading messages, timing statistics or dedicated tracing messages which can be sent to the *trace* buffer.

So that Proof General notices, these urgent messages should be marked-up with "eager" annotations.

Variable: proof-shell-eager-annotation-start

Eager annotation field start. A regular expression or nil.
An "eager annotation indicates" to Proof General that some following output should be displayed (or processed) immediately and not accumulated for parsing later. Note that this affects processing of output which is ordinarily accumulated: output which appears before the eager annotation start will be discarded.

The start/end annotations can be used to hilight the output, but are stripped from display of the message in the minibuffer.

It is useful to recognize (starts of) warnings or file-reading messages with this regexp. You must also recognize any special messages from the prover to PG with this regexp (e.g. ‘proof-shell-clear-goals-regexp’, ‘proof-shell-retract-files-regexp’, etc.)

See also ‘proof-shell-eager-annotation-start-length’, ‘proof-shell-eager-annotation-end’.

Set to nil to disable this feature.

Variable: proof-shell-eager-annotation-start-length

Maximum length of an eager annotation start.
Must be set to the maximum length of the text that may match ‘proof-shell-eager-annotation-start’ (at least 1). If this value is too low, eager annotations may be lost!

This value is used internally by Proof General to optimize the process filter to avoid unnecessary searching.

Variable: proof-shell-eager-annotation-end

Eager annotation field end. A regular expression or nil.
An eager annotation indicates to Emacs that some following output should be displayed or processed immediately.

See also ‘proof-shell-eager-annotation-start’.

It is nice to recognize (ends of) warnings or file-reading messages with this regexp. You must also recognize (ends of) any special messages from the prover to PG with this regexp (e.g. ‘proof-shell-clear-goals-regexp’, ‘proof-shell-retract-files-regexp’, etc.)

The default value is "\n" to match up to the end of the line.

The default action for urgent messages is to display them in the response buffer, highlighted. But we also allow for some control messages, issued from the proof assistant to Proof General and not intended for the user to see. These are recognized in the same way as urgent messages (marked with eager annotations), so they will be acted on as soon as they are issued by the prover.

Variable: proof-shell-clear-response-regexp

Regexp matching output telling Proof General to clear the response buffer.

More precisely, this should match a string which is bounded by matches on ‘proof-shell-eager-annotation-start’ and ‘proof-shell-eager-annotation-end’.

This feature is useful to give the prover more control over what output is shown to the user. Set to nil to disable.

Variable: proof-shell-clear-goals-regexp

Regexp matching output telling Proof General to clear the goals buffer.

More precisely, this should match a string which is bounded by matches on ‘proof-shell-eager-annotation-start’ and ‘proof-shell-eager-annotation-end’.

This feature is useful to give the prover more control over what output is shown to the user. Set to nil to disable.

Variable: proof-shell-interactive-prompt-regexp

Matches output from the prover which indicates an interactive prompt.
If we match this, we suppose that the prover has switched to an interactive diagnostic mode which requires direct interaction with the shell rather than via script management. In this case, the shell buffer will be displayed and the user left to their own devices.

Note: this should match a string which is bounded by matches on ‘proof-shell-eager-annotation-start’ and ‘proof-shell-eager-annotation-end’.

Variable: proof-shell-trace-output-regexp

Matches tracing output which should be displayed in trace buffer.
Each line which matches this regexp but would otherwise be treated as an ordinary response, is sent to the trace buffer instead of the response buffer.

This is intended for unusual debugging output from the prover, rather than ordinary output from final proofs.

This should match a string which is bounded by matches on ‘proof-shell-eager-annotation-start’ and ‘proof-shell-eager-annotation-end’.

Set to nil to disable.

Variable: proof-shell-theorem-dependency-list-regexp

Matches output telling Proof General about dependencies.
This is to allow navigation and display of dependency information. The output from the prover should be a message with the form

   dependencies OF  X Y Z   ARE  A B C

with X Y Z, A B C separated by whitespace or somehow else (see ‘proof-shell-theorem-dependency-list-split’. This variable should be set to a regexp to match the overall message (which should be an urgent message), with two sub-matches for X Y Z and A B C.

This is an experimental feature, currently work-in-progress.

Two important control messages are recognized by proof-shell-process-file and proof-shell-retract-files-regexp, used for synchronizing Proof General with a file loading mechanism built into the proof assistant. See section Handling Multiple Files, for more details about how to use the final four settings described here.

Variable: proof-shell-process-file

A pair (regexp . function) to match a processed file name.

If regexp matches output, then the function function is invoked. It must return the name of a script file (with complete path) that the system has successfully processed. In practice, function is likely to inspect the match data. If it returns the empty string, the file name of the scripting buffer is used instead. If it returns nil, no action is taken.

More precisely, regexp should match a string which is bounded by matches on ‘proof-shell-eager-annotation-start’ and ‘proof-shell-eager-annotation-end’.

Care has to be taken in case the prover only reports on compiled versions of files it is processing. In this case, function needs to reconstruct the corresponding script file name. The new (true) file name is added to the front of ‘proof-included-files-list’.

Variable: proof-shell-retract-files-regexp

Matches a message that the prover has retracted a file.

More precisely, this should match a string which is bounded by matches on ‘proof-shell-eager-annotation-start’ and ‘proof-shell-eager-annotation-end’.

At this stage, Proof General’s view of the processed files is out of date and needs to be updated with the help of the function ‘proof-shell-compute-new-files-list’.

Variable: proof-shell-compute-new-files-list

Function to update ‘proof-included-files list’.

It needs to return an up-to-date list of all processed files. The result will be stored in ‘proof-included-files-list’.

This function is called when ‘proof-shell-retract-files-regexp’ has been matched in the prover output.

In practice, this function is likely to inspect the previous (global) variable ‘proof-included-files-list’ and the match data triggered by ‘proof-shell-retract-files-regexp’.

Variable: proof-cannot-reopen-processed-files

Non-nil if the prover allows re-opening of already processed files.

If the user has used Proof General to process a file incrementally, then PG will retain the spans recording undo history in the buffer corresponding to that file (provided it remains visited in Emacs).

If the prover allows, it will be possible to undo to a position within this file. If the prover does not allow this, this variable should be set non-nil, so that when a completed file is activated for scripting (to do undo operations), the whole history is discarded.

4.5 Hooks and other settings

Variable: proof-shell-filename-escapes

A list of escapes that are applied to %s for filenames.
A list of cons cells, car of which is string to be replaced by the cdr. For example, when directories are sent to Isabelle, HOL, and Coq, they appear inside ML strings and the backslash character and quote characters must be escaped. The setting

  '(("\\\\" . "\\\\")
    ("\"" . "\\\""))

achieves this.

This setting is used inside the function ‘proof-format-filename’.

Variable: proof-shell-process-connection-type

The value of ‘process-connection-type’ for the proof shell.
Set non-nil for ptys, nil for pipes.

note: In Emacs >= 24 (checked for 24 and 25.0.50.1), t is not a good choice: input is cut after 4095 chars, which hangs pg.

Variable: proof-shell-handle-error-or-interrupt-hook

Run after an error or interrupt has been reported in the response buffer.
Hook functions may inspect ‘proof-shell-last-output-kind’ to determine whether the cause was an error or interrupt. Possible values for this hook include:

 ‘proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window’
 ‘proof-goto-end-of-locked-if-pos-not-visible-in-window’

which move the cursor in the scripting buffer on an error or error/interrupt.

Remark: This hook is called from shell buffer. If you want to do something in scripting buffer, ‘save-excursion’ and/or ‘set-buffer’.

Variable: proof-shell-pre-interrupt-hook: Run immediately after ‘comint-interrupt-subjob’ is called.
This hook is added to allow customization for systems that query the user before returning to the top level.

Variable: proof-shell-handle-output-system-specific

Set this variable to handle system specific output.
Errors and interrupts are recognised in the function ‘proof-shell-handle-immediate-output’. Later output is handled by ‘proof-shell-handle-delayed-output’, which displays messages to the user in goals and response buffers.

This hook can run between the two stages to take some effect.

It should be a function which is passed (cmd string) as arguments, where ‘cmd’ is a string containing the currently processed command and ‘string’ is the response from the proof system. If action is taken and goals/response display should be prevented, the function should update the variable ‘proof-shell-last-output-kind’ to some non-nil symbol.

The symbol will be compared against standard ones, see documentation of ‘proof-shell-last-output-kind’. A suggested canonical non-standard symbol is 'systemspecific.

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