[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

# 3. Proof Script Settings

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] | [ ? ]

## 3.1 Recognizing commands and comments

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.

Variable: proof-terminal-char

  Character that terminates commands sent to prover; 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``’.

Variable: proof-script-sexp-commands

  Non-nil if script has LISP-like syntax: 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``’.

Variable: proof-script-command-start-regexp

  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``’.

Variable: proof-script-command-end-regexp

  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.

Variable: proof-script-comment-start

  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``’.

Variable: proof-script-comment-start-regexp

  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.

Variable: proof-script-comment-end

  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.

Variable: proof-script-comment-end-regexp

  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.

Variable: proof-case-fold-search

  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] | [ ? ]

## 3.2 Recognizing proofs

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).

Variable: proof-goal-command-regexp

  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.

Variable: proof-goal-command-p

  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).

Variable: proof-goal-with-hole-regexp

  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.

Variable: proof-goal-with-hole-result

  How to build theorem name after matching with ‘``proof-goal-with-hole-regexp``’.
  String or Int. If an int N use `match-string` to recover the value of the Nth parenthesis matched. If it is a string use `replace-match`. In this case, `proof-save-with-hole-regexp` should match the entire command

Variable: proof-save-command-regexp

  Matches a save command.

Variable: proof-save-with-hole-regexp

  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.

Variable: proof-completed-proof-behaviour

  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
        'closeany  -  close as soon as the next command arrives, save or not
       'closegoal  -  close when the next "goal" command arrives
          'extend  -  keep extending the closed region until a save or goal.

  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.

Variable: proof-really-save-command-p

  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] | [ ? ]

## 3.3 Recognizing other elements

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.

Variable: proof-script-imenu-generic-expression

  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.

Variable: imenu-generic-expression

  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).

Variable: proof-script-next-entity-regexps

  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 'backward backregexp)
        (regexp matchnos 'forward forwardregexp)

  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`.

Variable: proof-script-find-next-entity-fn

  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] | [ ? ]

## 3.4 Configuring undo behaviour

The settings here are used to configure the way "undo" commands are calculated.

Variable: proof-non-undoables-regexp

  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.

Variable: proof-undo-n-times-cmd

  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.

Variable: proof-ignore-for-undo-count

  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``’.

Variable: proof-count-undos-fn

  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``’.

Function: proof-generic-count-undos span

  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``’.

Variable: proof-find-and-forget-fn

  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).

Function: proof-generic-find-and-forget span

  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.

Variable: proof-forget-id-command

  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``’.

Variable: pg-topterm-goalhyplit-fn

  Function to return cons if point is at a goal/hypothesis/literal.
  This is used to parse the proofstate output to mark it up for proof-by-pointing or literal command insertion. It should return a cons or nil. First element of the cons is a symbol, `'goal'`, `'hyp'` or `'lit'`. The second element is a string: the goal, hypothesis, or literal command itself.

  If you leave this variable unset, no proof-by-pointing markup will be attempted.

Variable: proof-kill-goal-command

  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 ‘``proof-kill-goal-command``’, followed by ‘``proof-find-and-forget-fn``’ if necessary.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 3.5 Nested proofs

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.

Variable: proof-nested-goals-history-p

  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.

Variable: proof-nested-undo-regexp

  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] | [ ? ]

## 3.6 Safe (state-preserving) commands

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).

Variable: proof-state-preserving-p

  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``’.

Function: proof-generic-state-preserving-p cmd

  Is cmd state preserving? Match on ‘``proof-non-undoables-regexp``’.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 3.7 Activate scripting hook

Variable: proof-activate-scripting-hook

  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] | [ ? ]

## 3.8 Automatic multiple files

See section Handling Multiple Files, for more details about this setting.

Variable: proof-auto-multiple-files

  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] | [ ? ]

## 3.9 Completions

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.

Variable: PA-completion-table

  List of identifiers to use for completion for this proof assistant.
  Completion is activated with c-ret.

  If this table is empty or needs adjusting, please make changes using ‘``customize-variable``’ and post suggestions at http://proofgeneral.inf.ed.ac.uk/trac

Command: proof-add-completions

  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 July, 24 2008 using texi2html 1.78.