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.

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 (Elisp)Syntax Tables).

See section Proof script mode, for more details of the parsing functions.

Variable: proof-terminal-string

String 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-string’, or ‘proof-script-parse-function’.

Variable: proof-electric-terminator-noterminator: If non-nil, electric terminator does not actually insert a terminator.

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.

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.

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

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 (see (Elisp)Syntax Tables) 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.

Finally, the function proof-looking-at-syntactic-context is used internally to help determine the syntactic structure of the buffer. You can test it to check the settings above. If necessary, you can override this with a system-specific function.

Function: proof-looking-at-syntactic-context: Determine if current point is at beginning or within comment/string context.
If so, return a symbol indicating this (’comment or 'string). This function invokes <PA-syntactic-context> if that is defined, otherwise it calls ‘proof-looking-at-syntactic-context’.

3.2 Recognizing proofs

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

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

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 get theorem name after ‘proof-goal-with-hole-regexp’ match.
String or Int. If an int N, use ‘match-string’ to get the value of the Nth parenthesis matched. If a string, use ‘replace-match’. In this case, ‘proof-goal-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 built 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.

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.

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

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 a list of the appropriate commands (given 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 list of commands to undo 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 span, return commands 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 to return list of commands to forget 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-unprocessed-begin). This may involve forgetting a number of definitions, declarations, or whatever.

If return value is nil, it 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.

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.

3.6 Omitting proofs for speed

In normal operation, the commands in an asserted region are sent successively to the proof assistant. When the proof assistant reports an error, processing stops. This ensures the consistency of the development. Proof General supports omitting portions of the asserted region to speed processing up at the cost of consistency. Portions that can be potentially omitted are called opaque proofs in Proof General, because usually only opaque proofs (in the sense of Coq) can be omitted without risking to break the following code. This feature is also described in the Proof General manual, see (ProofGeneral)Script processing commands and see (ProofGeneral)Omitting proofs for speed.

The omit proofs feature works in a simple, straightforward way: After parsing the asserted region, Proof General uses regular expressions to search for commands that start (proof-script-proof-start-regexp) and end (proof-script-proof-end-regexp) an opaque proof. If one is found, the opaque proof is replaced with a cheating command (proof-script-proof-admit-command). From this description it is immediate, that the omit proof feature does only work if proofs are not nested. If a nested proof is found, a warning is displayed and omitting proofs stops at that location for the currently asserted region.

In Coq, commands with non-local effects, such as Hint, may appear inside proofs. Additionally, admitting a proof of a Let declaration causes a warning in Coq. To treat such cases, the predicate proof-script-cmd-prevents-proof-omission is applied to all commands inside proofs and the regular expression proof-script-cmd-force-next-proof-kept is matched against all commands outside proofs. In case of a hit, the current or, respectively, the next proof is treated as non-opaque and is not omitted. Note that a match of proof-script-cmd-force-next-proof-kept is only handled if the matching command and the following proof appear in the same asserted region. If the proof is asserted separately, the information about the match in the previously asserted region is lost and the proof may thus be omitted.

To enable the omit proofs feature, the following settings must be configured.

Variable: proof-omit-proofs-configured

t if the omit proofs feature has been configured by the proof assitant.
See also ‘proof-omit-proofs-option’ or the Proof General manual for a description of the feature. This option can only be set, if all of ‘proof-script-proof-start-regexp’, ‘proof-script-proof-end-regexp’, ‘proof-script-definition-end-regexp’ and ‘proof-script-proof-admit-command’ have been configured.

The omit proofs feature skips over opaque proofs in the source code, admitting the theorems, to speed up processing.

If ‘proof-omit-proofs-option’ is set by the user, all proof commands in the source following a match of ‘proof-script-proof-start-regexp’ up to and including the next match of ‘proof-script-proof-end-regexp’, are omitted (not send to the proof assistant) and replaced by ‘proof-script-proof-admit-command’. If a match for ‘proof-script-definition-end-regexp’ is found while searching forward for the proof end or if ‘proof-script-cmd-prevents-proof-omission’ recognizes a proof command that prevents proof omission then the current proof (up to and including the match of ‘proof-script-definition-end-regexp’ or ‘proof-script-proof-end-regexp’) is considered to be not opaque and not omitted, thus all these proof commands _are_ sent to the proof assistant.

The feature does not work for nested proofs. If a match for ‘proof-script-proof-start-regexp’ is found before the next match for ‘proof-script-proof-end-regexp’ or ‘proof-script-definition-end-regexp’, the search for opaque proofs immediately stops and all commands following the previous match of ‘proof-script-proof-start-regexp’ are sent verbatim to the proof assistant.

All the regular expressions for this feature are matched against the commands inside proof action items, that is as strings, without surrounding space.

Variable: proof-script-proof-start-regexp: Regular expression for the start of a proof for the omit proofs feature.
See ‘proof-omit-proofs-configured’.

Variable: proof-script-proof-end-regexp: Regular expression for the end of an opaque proof for the omit proofs feature.
See ‘proof-omit-proofs-configured’.

Variable: proof-script-definition-end-regexp: Regexp for the end of a non-opaque proof for the omit proofs feature.
See ‘proof-omit-proofs-configured’.

Variable: proof-script-proof-admit-command: Proof command to be inserted instead of omitted proofs.

Variable: proof-script-cmd-prevents-proof-omission: Optional predicate to match commands that prevent omitting the current proof.
If set, this option should contain a function that takes a proof command (as string) as argument and returns t or nil. If set, the function is called on every proof command inside a proof while scanning for proofs to omit. The predicate should return t if the command has effects ouside the proof, potentially breaking the script if the current proof is omitted. If the predicate returns t, the proof is considered to be not opaque and thus not omitted.

Variable: proof-script-cmd-force-next-proof-kept

Optional regexp for commands that prevent omitting the next proof.
If set, this option should contain a regular expression that matches proof-script commands that prevent the omission of proofs dirctly following this command. When scanning the newly asserted region for proofs to omit, every proof-script command outside proofs is matched against this regexp. If it matches and the next command matches ‘proof-script-proof-start-regexp’ this following proof will not be omitted.

Note that recognition of commands with this regular expression does only work if the command and the following proof are asserted together.

3.7 Proof status statistic

The commands proof-check-report and proof-check-annotate build on the omit-proofs feature. Using its machinery, proof-check-proofs, the inner working horse of both commands, splits the current buffer into opaque proofs and all other material. The other material is asserted in the usual way and proof-check-proofs aborts if it detects an error in there. For opaque proofs it first tries to assert them in the usual way too. If this succeeds the proof is considered valid. Otherwise the proof is replaced with proof-script-proof-admit-command and the proof is considered invalid. In order to consider Admitted proofs as invalid ones, proofs whose last command matches proof-omit-cheating-regexp count as invalid. To associate theorem names with opaque proofs, the function proof-get-proof-info-fn is called, which is identical to proof-tree-get-proof-info, See section Proof Tree Elisp configuration.

To enable proof status statistics, the omit-proofs feature must be configured, See section Omitting proofs for speed. Additionally, the following settings must be configured.

Variable: proof-get-proof-info-fn

Return proof name and state number for ‘proof-check-proofs’.
Proof assistant specific function for ‘proof-check-proofs’. This function takes no arguments, it is called after completely processing the proof script up to a certain point (including all callbacks in spans). It must return a list, which contains, in the following order:

* the current state number (as positive integer) * the name of the current proof (as string) or nil

The proof assistant should return to the same state when the state number is supplied to ‘proof-retract-command-fn’. Processing the command returned by ‘proof-retract-command-fn’ without processing any other command after calling this function should be a no-op.

(This function has the same signature and specification as ‘proof-tree-get-proof-info’.)

Variable: proof-retract-command-fn: Function for retract command to a certain state.
This function takes a state as argument as returned by ‘proof-get-proof-info-fn’. It should return a command that brings the proof assistant back to the same state.

Variable: proof-omit-cheating-regexp

Regular expression matching proof closing commands for incomplete proofs.
If set, this regular expression is applied to the last command of opaque proofs. If it matches the proofs counts as invalid for the proof-status statistics and annotation feature. For Coq this is used to mark Admitted proofs as invalid.

This option can be left at ‘nil’.

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

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

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

3.11 Completely asserted buffers

When switching scripting from buffer A to buffer B Proof General normally offers the choice of either completely retracting or completely asserting buffer A. The option to completely assert buffer A is offered, because the material in B may depend on A. Even if B does not depend on A, it does no harm if one keeps the development of A loaded in the proof assistant. This observation is true for many proof assistants.

One exception is Coq. Assume file B depends on file A. When Coq processes B it does not read the sources of A. Instead it loads a compiled object representation of A. Therefore, when switching from A to B, it does make no sense to keep the material of A loaded in the proof assistant. For Coq, the material of A may even provoke errors on correct input. Therefore, for coq, the right behaviour is to completely retract buffer A before switching to B.

Variable: proof-no-fully-processed-buffer: Set to t if buffers should always retract before scripting elsewhere.
Leave at nil if fully processed buffers make sense for the current proof assistant. If nil the user can choose to fully assert a buffer when starting scripting in a different buffer. If t there is only the choice to fully retract the active buffer before starting scripting in a different buffer. This last behavior is needed for Coq.

3.12 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 M-x complete.

If this table is empty or needs adjusting, please make changes using ‘customize-variable’ and post suggestions at https://github.com/ProofGeneral/PG/issues

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.

This document was generated on November 21, 2024 using texi2html 1.82.