| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 | ||
| 4.2 Script input to the shell | ||
| 4.3 Settings for matching various output from proof process | ||
| 4.4 Settings for matching urgent messages from proof process | ||
| 4.5 Hooks and other settings |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 `proof-prog-args'.
Suggestion: this can be set in proof-pre-shell-start-hook from a variable
which is in the proof assistant's customization group. This allows
different proof assistants to coexist (albeit in separate Emacs sessions).
Remark: if `proof-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.
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-char, and add it if not.
If proof-terminal-char 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 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.
The number of seconds to wait after sending proof-shell-quit-cmd.
After this timeout, the proof shell will be killed off more rudely.
If your proof assistant takes a long time to clean up (for
example writing persistent databases out or the like), you may
need to bump up this value.
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 section 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.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
Hooks 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:
|
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 uses this hook for setting the pretty printer width if the window width has changed; Plastic uses it to remove literate-style markup from `string'. The x-symbol support uses this hook to convert special characters into tokens for the proof assistant.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
A special character which terminates an annotated prompt.
Set to nil if proof assistant does not support annotated prompts.
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.
Proof shell's value for comint-prompt-pattern, which see.
NB!! This pattern is just for interaction in comint (shell buffer).
You don't really need to set it. The important one to set is
`proof-shell-annotated-prompt-regexp', which see.
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. The special character should appear in
this regexp, and should be the value of proof-shell-wakeup-char.
Regexp matching output from an aborted proof.
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.
Regexp matching the end of the proof state output, or nil.
If nil, just use the rest of the output following proof-shell-start-goals-regexp.
A regular expression matching the name of assumptions.
At the moment, this setting is not used in the generic Proof General.
In the future it will be used for a generic implementation for `pg-topterm-goalhyp-fn',
used to help parse the goals buffer to annotate it for proof by pointing.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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, or timing statistics.
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.
It is nice 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.
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.
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 telling Proof General to set some variable.
This allows the proof assistant to configure Proof General directly
and dynamically.
If the regexp matches output from the proof assistant, there should be
two match strings: (match-string 1) should be the name of the elisp
variable to be set, and (match-string 2) should be the value of the
variable (which will be evaluated as a lisp expression).
A good markup for the second string is to delimit with #'s, since these are not valid syntax for elisp evaluation.
Elisp errors will be trapped when evaluating; set
proof-show-debug-messages to be informed when this happens.
Example uses are to adjust PG's internal copies of proof assistant's settings, or to make automatic dynamic syntax adjustments in Emacs to match changes in theory, etc.
If you pick a dummy variable name (e.g. `proof-dummy-setting') you can just evaluation arbitrary elisp expressions for their side effects, to adjust menu entries, or even launch auxiliary programs. But use with care - there is no protection against catastrophic elisp!
This setting could also be used to move some configuration settings from PG to the prover, but this is not really supported (most settings must be made before this mechanism will work). In future, the PG standard protocol, pgip, will use this mechanism for making all settings.
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.
A pair (regexp . function) to match a processed file name.
If regexp matches output, then the function function is invoked on the output string chunk. 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.
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.
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. Its
output is stored in `proof-included-files-list'. Its input is the
string of which `proof-shell-retract-files-regexp' matched a
substring. 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 regular expression to match a Require-type of command, or nil.
If set to a regexp, then `proof-done-advancing-require-function'
should also be set, and will be called immediately after the match.
This can be used to adjust `proof-included-files-list' based on the
lines of script that have been processed/parsed, rather than relying
on information from the prover.
Invoked from `proof-done-advancing', see `proof-shell-require-command-regexp'.
The function is passed the span and the command as arguments.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 does not apply to lego, which does not need backslash escapes and does not allow filenames with quote characters.
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.
The default (and preferred) option is to use pty communication.
However there is a long-standing backslash/long line problem with
Solaris which gives a mess of ^G characters when some input is sent
which has a \ in the 256th position.
So we select pipes by default if it seems like we're on Solaris.
We do not force pipes everywhere because this risks loss of data.
Hooks run before proof shell is started.
Suggestion: set this to a function which configures just these proof
shell variables:
proof-prog-name
|
This is the bare minimum needed to get a shell buffer and
its friends configured in the function proof-shell-start.
Run after an error or interrupt has been reported in the response buffer.
Hook functions may inspect `proof-shell-error-or-interrupt-seen' 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
|
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 Poly/ML and other
systems where the system queries the user before returning to
the top level. For Poly/ML it can be used to send the string "f",
for example.
Set this variable to handle system specific output.
Errors, start of proofs, abortions of proofs and completions of
proofs are recognised in the function `proof-shell-process-output'.
All other output from the proof engine is simply reported to the
user in the response buffer.
To catch further special cases, set this variable to a pair of
functions '(condf . actf). Both are given (cmd string) as arguments.
`cmd' is a string containing the currently processed command.
`string' is the response from the proof system. To change the
behaviour of `proof-shell-process-output', (condf cmd string) must
return a non-nil value. Then (actf cmd string) is invoked.
See the documentation of `proof-shell-process-output' for the required
output format.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by David Aspinall on November, 7 2006 using texi2html 1.76.