| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The variables described in this chapter should be set in the script mode
before proof-config-done is called. These variables configure
recognition of commands in the proof script, and also control some of
the behaviour of script management.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The first four settings configure the generic parsing strategy for
commands in the proof script. Usually only one of these three needs to
be set. If the generic parsing functions are not flexible for your
needs, you can supply a value for proof-script-parse-function.
Note that for the generic functions to work properly, it is
essential that you set the syntax table for your mode properly,
so that comments and strings are recognized. See the Emacs
documentation to discover how to do this (particularly for the function
modify-syntax-entry).
See section Proof script mode, for more details of the parsing functions.
Character which terminates every command sent to proof assistant. nil if none.
To configure command recognition properly, you must set at least one
of these: `proof-script-sexp-commands', `proof-script-command-end-regexp',
`proof-script-command-start-regexp', `proof-terminal-char',
or `proof-script-parse-function'.
Non-nil if proof script has a LISP-like syntax, and commands are top-level sexps.
You should set this variable in script mode configuration.
To configure command recognition properly, you must set at least one
of these: `proof-script-sexp-commands', `proof-script-command-end-regexp',
`proof-script-command-start-regexp', `proof-terminal-char',
or `proof-script-parse-function'.
Regular expression which matches start of commands in proof script.
You should set this variable in script mode configuration.
To configure command recognition properly, you must set at least one
of these: `proof-script-sexp-commands', `proof-script-command-end-regexp',
`proof-script-command-start-regexp', `proof-terminal-char',
or `proof-script-parse-function'.
Regular expression which matches end of commands in proof script.
You should set this variable in script mode configuration.
The end of the command is considered to be the end of the match
of this regexp. The regexp may include a nested group, which
can be used to recognize the start of the following command
(or white space). If there is a nested group, the end of the
command is considered to be the start of the nested group,
i.e. (match-beginning 1), rather than (match-end 0).
To configure command recognition properly, you must set at least one
of these: `proof-script-sexp-commands', `proof-script-command-end-regexp',
`proof-script-command-start-regexp', `proof-terminal-char',
or `proof-script-parse-function'.
The next four settings configure the comment syntax. Notice that to get reliable behaviour of the parsing functions, you may need to modify the syntax table for your prover's mode. Read the Elisp manual for details about that.
String which starts a comment in the proof assistant command language.
The script buffer's comment-start is set to this string plus a space.
Moreover, comments are usually ignored during script management, and not
sent to the proof process.
You should set this variable for reliable working of Proof General,
as well as `proof-script-comment-end'.
Regexp which matches a comment start in the proof command language.
The default value for this is set as (regexp-quote proof-script-comment-start)
but you can set this variable to something else more precise if necessary.
String which ends a comment in the proof assistant command language.
Should be an empty string if comments are terminated by end-of-line
The script buffer's comment-end is set to a space plus this string,
if it is non-empty.
See also `proof-script-comment-start'.
You should set this variable for reliable working of Proof General.
Regexp which matches a comment end in the proof command language.
The default value for this is set as (regexp-quote proof-script-comment-end)
but you can set this variable to something else more precise if necessary.
Value for case-fold-search when recognizing portions of proof scripts.
Also used for completion, via `proof-script-complete'.
The default value is `nil'. If your prover has a case insensitive
input syntax, proof-case-fold-search should be set to `t' instead.
NB: This setting is not used for matching output from the prover.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Up to three settings each may be supplied for recognizing goal-like and
save-like commands. The -with-hole- settings are used to make a
record of the name of the theorem proved, and also to build a default
value for the rather complicated setting
proof-script-next-entity-regexps, which activates the function
menu feature.
The -p subsidiary predicates were added to allow more
discriminating behaviour for particular proof assistants. (This is a
typical example of where the core framework needs some additional
generalization, to simplify matters, and allow for a smooth handling of
nested proofs; the present state is only part of the way there).
Matches a goal command in the proof script.
This is used (1) to make the default value for `proof-goal-command-p',
used as an important part of script management to find the start
of an atomic undo block, and (2) to construct the default
for `proof-script-next-entity-regexps' used for function menus.
A function to test: is this really a goal command span?
This is added as a more refined addition to proof-goal-command-regexp,
to solve the problem that Coq and some other provers can have goals which
look like definitions, etc. (In the future we may generalize
proof-goal-command-regexp instead).
Regexp which matches a command used to issue and name a goal.
The name of the theorem is built from the variable
proof-goal-with-hole-result using the same convention as
for `query-replace-regexp'.
Used for setting names of goal..save regions and for default
configuration of other modes (function menu, imenu).
It's safe to leave this setting as nil.
String or Int: how to build the theorem name after matching
with proof-goal-with-hole-regexp. If it is an int N use match-string
to recover the value of the Nth parenthesis matched. If it is a string
use replace-match. It the later case, proof-goal-with-hole-regexp should
match the entire command
Matches a save command.
Regexp which matches a command to save a named theorem.
The name of the theorem is build from the variable
proof-save-with-hole-result using the same convention as
query-replace-regexp.
Used for setting names of goal..save and proof regions and for
default function-menu configuration in proof-script-find-next-entity.
It's safe to leave this setting as nil.
Indicates how Proof General treats commands beyond the end of a proof.
Normally goal...save regions are "closed", i.e. made atomic for undo.
But once a proof has been completed, there may be a delay before
the "save" command appears -- or it may not appear at all. Unless
nested proofs are supported, this can spoil the undo-behaviour in
script management since once a new goal arrives the old undo history
may be lost in the prover. So we allow Proof General to close
off the goal..[save] region in more flexible ways.
The possibilities are:
nil - nothing special; close only when a save arrives
|
If your proof assistant allows nested goals, it will be wrong to close off the portion of proof so far, so this variable should be set to nil.
NB: 'extend behaviour is not currently compatible with appearance of
save commands, so don't use that if your prover has save commands.
Is this really a save command?
This is a more refined addition to proof-save-command-regexp.
It should be a function taking a span and command as argument,
and can be used to track nested proofs. (See what is done in
isar/ for example). In the future, this setting should be
removed when the generic core is extended to handle nested
proofs smoothly.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
To configure Imenu (which in turn configures Speedbar),
you may use the following setting. If this is unset, a generic
setting based on proof-goal-with-hole-regexp is configured.
Regular expressions to help find definitions and proofs in a script.
Value for `imenu-generic-expression', see documentation of Imenu
and that variable for details.
The regex pattern to use for creating a buffer index.
If non-nil this pattern is passed to `imenu--generic-function' to create a buffer index.
The value should be an alist with elements that look like this:
(menu-title regexp index) |
or like this:
(menu-title regexp index function ARGUMENTS...) |
with zero or more ARGUMENTS. The former format creates a simple element in the index alist when it matches; the latter creates a special element of the form (name function position-marker ARGUMENTS...) with function and arguments beiong copied from `imenu-generic-expression'.
menu-title is a string used as the title for the submenu or nil if the entries are not nested.
regexp is a regexp that should match a construct in the buffer that is to be displayed in the menu; i.e., function or variable definitions, etc. It contains a substring which is the name to appear in the menu. See the info section on Regexps for more information.
index points to the substring in regexp that contains the name (of the function, variable or type) that is to appear in the menu.
The variable is buffer-local.
The variable `imenu-case-fold-search' determines whether or not the regexp matches are case sensitive. and `imenu-syntax-alist' can be used to alter the syntax table for the search.
For example, see the value of `lisp-imenu-generic-expression' used by `lisp-mode' and `emacs-lisp-mode' with `imenu-syntax-alist' set locally to give the characters which normally have \"punctuation\" syntax \"word\" syntax during matching."
To configure the function menu feature, there are a couple of settings. These can be used to recognize named proofs, and other elements in the proof script as well. (NOTE: it is likely that function menu support will be removed in favour of Imenu only in the next release of Proof General).
Regular expressions to help find definitions and proofs in a script.
This is the list of the form
(anyentity-regexp
discriminator-regexp ... discriminator-regexp) |
The idea is that anyentity-regexp matches any named entity in the proof script, on a line where the name appears. This is assumed to be the start or the end of the entity. The discriminators then test which kind of entity has been found, to get its name. A discriminator-regexp has one of the forms
(regexp matchnos)
(regexp matchnos |
If regexp matches the string captured by anyentity-regexp, then matchnos are the match numbers for the substrings which name the entity (these may be either a single number or a list of numbers).
If 'backward backregexp is present, then the start of the entity
is found by searching backwards for backregexp.
Conversely, if 'forward forwardregexp is found, then the end of
the entity is found by searching forwards for forwardregexp.
Otherwise, the start and end of the entity will be the region matched by anyentity-regexp.
This mechanism allows fairly complex parsing of the buffer, in particular, it allows for goal..save regions which are named only at the end. However, it does not parse strings, comments, or parentheses.
This variable may not need to be set: a default value which should
work for goal..saves is calculated from proof-goal-with-hole-regexp,
proof-goal-command-regexp, and proof-save-with-hole-regexp.
Name of function to find next interesting entity in a script buffer.
This is used to configure func-menu. The default value is
proof-script-find-next-entity, which searches for the next entity
based on fume-function-name-regexp which by default is set from
proof-script-next-entity-regexps.
The function should move point forward in a buffer, and return a cons cell of the name and the beginning of the entity's region.
Note that proof-script-next-entity-regexps is set to a default value
from proof-goal-with-hole-regexp and proof-save-with-hole-regexp in
the function proof-config-done, so you may not need to worry about any
of this. See whether function menu does something sensible by
default.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The settings here are used to configure the way "undo" commands are calculated.
Regular expression matching commands which are not undoable.
These are commands which should not appear in proof scripts,
for example, undo commands themselves (if the proof assistant
cannot "redo" an "undo").
Used in default functions `proof-generic-state-preserving-p'
and `proof-generic-count-undos'. If you don't use those,
may be left as nil.
Command to undo n steps of the currently open goal.
String or function.
If this is set to a string, `%s' will be replaced by the number of
undo steps to issue.
If this is set to a function, it should return the appropriate
command when called with an integer (the number of undo steps).
This setting is used for the default `proof-generic-count-undos'.
If you set `proof-count-undos-fn' to some other function, there is no
need to set this variable.
Matcher for script commands to be ignored in undo count.
May be left as nil, in which case it will be set to
`proof-non-undoables-regexp'.
Used in default function `proof-generic-count-undos'.
Function to calculate a command to issue undos to reach a target span.
The function takes a span as an argument, and should return a string
which is the command to undo to the target span. The target is
guaranteed to be within the current (open) proof.
This is an important function for script management.
The default setting `proof-generic-count-undos' is based on the
settings `proof-non-undoables-regexp' and
`proof-non-undoables-regexp'.
Count number of undos in a span, return command needed to undo that far.
Command is set using `proof-undo-n-times-cmd'.
A default value for `proof-count-undos-fn'.
For this function to work properly, you must configure
`proof-undo-n-times-cmd' and `proof-ignore-for-undo-count'.
Function that returns a command to forget back to before its argument span.
This setting is used to for retraction (undoing) in proof scripts.
It should undo the effect of all settings between its target span
up to (proof-locked-end). This may involve forgetting a number
of definitions, declarations, or whatever.
The special string proof-no-command means there is nothing to do.
This is an important function for script management.
Study one of the existing instantiations for examples of how to write it,
or leave it set to the default function `proof-generic-find-and-forget'
(which see).
Calculate a forget/undo command to forget back to span.
This is a long-range forget: we know that there is no
open goal at the moment, so forgetting involves unbinding
declarations, etc, rather than undoing proof steps.
This generic implementation assumes it is enough to find the
nearest following span with a `name' property, and retract
that using `proof-forget-id-command' with the given name.
If this behaviour is not correct, you must customize the function with something different.
Command to forget back to a given named span.
A string; `%s' will be replaced by the name of the span.
This is only used in the implementation of `proof-generic-find-and-forget',
you only need to set if you use that function (by not customizing
`proof-find-and-forget-fn'.
Function which returns cons cell if point is at a goal/hypothesis.
This is used to parse the proofstate output to mark it up for
proof-by-pointing. It should return a cons or nil. First element of
the cons is a symbol, 'goal' or 'hyp'. The second element is a
string: the goal or hypothesis itself.
If you leave this variable unset, no proof-by-pointing markup will be attempted.
Command to kill the currently open goal.
If this is set to nil, PG will expect proof-find-and-forget-fn
to do all the work of retracting to an arbitrary point in a file.
Otherwise, the generic split-phase mechanism will be used:
1. If inside an unclosed proof, use proof-count-undos.
2. If retracting to before an unclosed proof, use
|
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Proof General allows configuration for provers which have particular notions of nested proofs. The right thing may happen automatically, or you may need to adjust some of the following settings.
First, you should alter the next setting if the prover retains history for nested proofs.
Whether the prover supports recovery of history for nested proofs.
If it does (non-nil), Proof General will retain history inside
nested proofs.
If it does not, Proof General will amalgamate nested proofs into single
steps within the outer proof.
Second, it may happen (i.e. it does for Coq) that the prover has a history mechanism which necessitates keeping track of the number of nested "undoable" commands, even if the history of the proof itself is lost.
Regexp for commands that must be counted in nested goal-save regions.
Used for provers which allow nested atomic goal-saves, but with some nested history that must be undone specially.
At the moment, the behaviour is that a goal-save span has a 'nestedundos
property which is set to the number of commands within it which match
this regexp. The idea is that the prover-specific code can create a
customized undo command to retract the goal-save region, based on the
'nestedundos setting. Coq uses this to forget declarations, since
declarations in Coq reside in a separate context with its own (flat)
history.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
A proof command is "safe" if it can be issued away from the proof script. For this to work it should be state-preserving in the proof assistant (with respect to an on-going proof).
A predicate, non-nil if its argument (a command) preserves the proof state.
This is a safety-test used by proof-minibuffer-cmd to filter out scripting
commands which should be entered directly into the script itself.
The default setting for this function, `proof-generic-state-preserving-p'
tests by negating the match on `proof-non-undoables-regexp'.
Is cmd state preserving? Match on `proof-non-undoables-regexp'.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Hook run when a buffer is switched into scripting mode.
The current buffer will be the newly active scripting buffer.
This hook may be useful for synchronizing with the proof assistant, for example, to switch to a new theory (in case that isn't already done by commands in the proof script).
When functions in this hook are called, the variable
`activated-interactively' will be non-nil if
proof-activate-scripting was called interactively
(rather than as a side-effect of some other action).
If a hook function sends commands to the proof process,
it should wait for them to complete (so the queue is cleared
for scripting commands), unless activated-interactively is set.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
See section Handling Multiple Files, for more details about this setting.
Whether to use automatic multiple file management.
If non-nil, Proof General will automatically retract a script file
whenever another one is retracted which it depends on. It assumes
a simple linear dependency between files in the order which
they were processed.
If your proof assistant has no management of file dependencies, or one which depends on a simple linear context, you may be able to use this setting to good effect. If the proof assistant has more complex file dependencies then you should configure it to communicate with Proof General about the dependencies rather than using this setting.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Proof General allows provers to create a completion table to help writing keywords and identifiers in proof scripts. This is documented in the main Proof General user manual but summarized here for (a different kind of) completion.
Completions are filled in according to what has been recently typed, from a database of symbols. The database is automatically saved at the end of a session. Completion is usually a hand-wavy thing, so we don't make any attempt to maintain a precise completion table or anything.
The completion table maintained by `complete.el' is initialized
from PA-completion-table when `proof-script.el' is loaded.
This is done with the function proof-add-completions which
you may want to call at other times.
List of identifiers to use for completion for this proof assistant.
Completion is activated with C-return.
If this table is empty or needs adjusting, please make changes using
`customize-variable' and send suggestions to da+pg-support@@inf.ed.ac.uk
Add completions from <PA>-completion-table to completion database.
Uses `add-completion' with a negative number of uses and ancient
last use time, to discourage saving these into the users database.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by David Aspinall on November, 7 2006 using texi2html 1.76.