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.
Settings in this section configure Proof General with commands to send to the prover to activate certain actions.
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.
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.
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\"))
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.
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.
See also ‘proof-shell-init-cmd
’.
The command(s) for initially configuring the proof process.
This command is sent to the process as soon as synchronization is gained
(when an annotated prompt is first recognized). It can be used to configure
the proof assistant in some way, or print a welcome message
(since output before the first prompt is discarded).
See also ‘proof-shell-pre-sync-init-cmd
’.
A command for re-initialising the proof process.
A command to quit the proof process. If nil, send EOF instead.
Command to the proof assistant to change the working directory.
The format character ‘%s’ is replaced with the directory, and
the escape sequences in ‘proof-shell-filename-escapes
’ are
applied to the filename.
This setting is used to define the function ‘proof-cd
’ which
changes to the value of (default-directory
) for script buffers.
For files, the value of (default-directory
) is simply the
directory the file resides in.
NB: By default, ‘proof-cd
’ is called from ‘proof-activate-scripting-hook
’,
so that the prover switches to the directory of a proof
script every time scripting begins.
Command to turn prover goals output off when sending many script commands.
If non-nil, Proof General will automatically issue this command
to help speed up processing of long proof scripts.
See also ‘proof-shell-stop-silent-cmd
’.
NB: terminator not added to command.
Command to turn prover output on.
If non-nil, Proof General will automatically issue this command
to help speed up processing of long proof scripts.
See also ‘proof-shell-start-silent-cmd
’.
NB: Terminator not added to command.
Number of waiting commands in the proof queue needed to trigger silent mode.
Default is 2, but you can raise this in case switching silent mode
on or off is particularly expensive (or make it ridiculously large
to disable silent mode altogether).
See Handling Multiple Files, for more details about the final two settings in this group,
Command to the proof assistant to tell it that a file has been processed.
The format character ‘%s’ is replaced by a complete filename for a
script file which has been fully processed interactively with
Proof General. See ‘proof-format-filename
’ for other possibilities
to process the filename.
This setting used to interface with the proof assistant’s internal management of multiple files, so the proof assistant is kept aware of which files have been processed. Specifically, when scripting is deactivated in a completed buffer, it is added to Proof General’s list of processed files, and the prover is told about it by issuing this command.
If this is set to nil, no command is issued.
See also: ‘proof-shell-inform-file-retracted-cmd
’,
‘proof-shell-process-file
’, ‘proof-shell-compute-new-files-list
’.
Command to the proof assistant to tell it that a file has been retracted.
The format character ‘%s’ is replaced by a complete filename for a
script file which Proof General wants the prover to consider as not
completely processed. See ‘proof-format-filename
’ for other
possibilities to process the filename.
This is used to interface with the proof assistant’s internal management of multiple files, so the proof assistant is kept aware of which files have been processed. Specifically, when scripting is activated, the file is removed from Proof General’s list of processed files, and the prover is told about it by issuing this command. The action may cause the prover in turn to suggest to Proof General that files depending on this one are also unlocked.
If this is set to nil, no command is issued.
It is also possible to set this value to a function which will
be invoked on the name of the retracted file, and should remove
the ancestor files from ‘proof-included-files-list
’ by some
other calculation.
See also: ‘proof-shell-inform-file-processed-cmd
’,
‘proof-shell-process-file
’, ‘proof-shell-compute-new-files-list
’.
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
.
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.
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.
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.
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.
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.
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).
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).
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
’.
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.
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).
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.
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.
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.
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.
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.
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.
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.
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.
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
’.
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.
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 Handling Multiple Files, for more details about how to use the
final four settings described here.
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
’.
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
’.
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
’.
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.
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
’.
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.
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
’.
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.
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
.