Proof General user manual
|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|
Coq Proof General is an instantiation of Proof General for the Coq proof assistant. It supports most of the generic features of Proof General.
|11.1 Coq-specific commands|
|11.2 Multiple File Support|
|11.3 Editing multiple proofs|
|11.4 User-loaded tactics|
|11.5 Holes feature|
|11.6 Proof-Tree Visualization|
Coq Proof General supplies the following key-bindings:
Inserts “Intros ”
Inserts “Apply ”
Inserts “Section ”
Inserts “End <section-name>.” (this should work well with nested sections).
Prompts for a SearchIsos argument.
Since version 4.1 Coq Proof General has multiple file support. It consists of the following points:
coqtopwhen changing the active scripting buffer
Different buffers may require different load path’ or different
-I options. Because Coq cannot undo changes in the
load path, Proof General is forced to restart
the active scripting buffer changes.
Locking those buffers on which the current active scripting
buffer depends. This is controlled by the user option
Customizing Coq Multiple File Support and
Require command is processed it may be necessary
to save and compile some buffers. Because this feature
conflicts with existing customization habits, it is switched off
by default. When it is properly configured, one can freely switch
between different buffers. Proof General will compile the
necessary files whenever a
Require command is processed.
The compilation feature does currently not support ML modules.
The current version works reliably, even when stress-tested with changing random files in large Coq projects. However, some features have been spared for the next release, Current Limitations.
To enable the automatic compilation feature there are three points to adhere to:
coq-compile-before-requiremust be turned on (menu
Coq -> Settings -> Compile Before Require).
coq-prog-argsmust be deleted.
-Ioptions and lists of two strings
-R "dir" -as "path"(for more details see the documentation of ‘coq-load-path’ or Customizing Coq Multiple File Support).
coq-compile-commandcan be set to an external compilation command. For standard dependency analysis with
coqdepand compilation with
coq-compile-commandcan be left empty. In this case Proof General calls
|11.2.1 Automatic Compilation in Detail|
|11.2.2 Locking Ancestors|
|11.2.3 Customizing Coq Multiple File Support|
|11.2.4 Current Limitations|
coq-compile-before-require is enabled, Proof
General looks for
Require commands in text that gets
asserted (i.e., in text that is moved from the editing region to
the queue region, Locked, queue, and editing regions). If
Proof General finds a
Require command, it checks the
dependencies and (re-)compiles files as necessary. Only after
this compilation is finished, Proof General starts sending the
asserted text to the Coq process.
Declare ML Module commands are currently not recognized.
Proof General uses
coqdep in order to translate the
qualified identifiers in
Require commands to coq library
file names. Therefore, in Coq version prior to
Require Arith works, while
Require Arith.Le gives an error. The use of
is also the reason
why nonstandard load path elements must be configured in
Once the library file name has been determined, its dependencies
must be checked and out-of-date files must be compiled. This can
either be done internally, by Proof General itself, or by an
external command. If
coq-compile-command is the empty
string, Proof General does dependency checking and compilation
itself. Otherwise the command in
started as an external process after substituting certain keys,
Customizing Coq Multiple File Support.
For an external compilation command Proof General uses the
general compilation facilities of Emacs
(See (emacs)Compilation) with its own customization variables.
The compilation command must be customized in
coq-compile-command and the flag
Settings -> Confirm External Compilation)
whether the user must confirm the compilation command. The output
of the compilation appears then in the
When Proof General compiles itself, output is only shown in case
of errors. It then appears in the buffer
*coq-compile-response*. With internal as well as with external
one can use
C-x ` (bound to
See (emacs)Compilation Mode) to jump to error locations.
Note however, that
coqdep does not produce error messages
with location information, so
C-x ` cannot work for errors
For simplicity, internal compilation is currently done with synchronously running external commands. Therefore, for internal compilation, Emacs is locked and unresponsive until the compilation finishes.
Proof General cannot know if some library files have been updated
outside of Proof General, therefore, it must perform the
dependency checking for each
Require command. If the
continuous confirmation of the external compilation commands
becomes tedious, disable
coq-confirm-external-compilation (see menu
Require command causes a compilation of some files
one may wish to save some buffers to disk beforehand. The option
coq-compile-auto-save controls how and which files are
saved. There are two orthogonal choices: One may wish to save all
or only the Coq source files, and, one may or may not want to
confirm the saving of each file.
Locking ancestor files works as a side effect of dependency checking. This means that ancestor locking does only work when Proof General performs dependency checking and compilation itself. If an external command is used, Proof General does not see all dependencies and can therefore only lock direct ancestors.
Currently, locking ancestor files might not exactly do what Coq
users expect. There are two ways around this problem:
You can either switch ancestor locking completely off via
coq-lock-ancestors (Customizing Coq Multiple File Support) or you can generally permit editing in locked
sections with selecting
Quick Options ->
Freely Edit (which will set the option
In the default setting,
when you want to edit a locked ancestor, you are
forced to completely retract the current scripting buffer. The
right behaviour for Coq would be to retract the current scripting
buffer only up to the point before the appropriate
command. At the users choice it should also be possible to unlock
the ancestor without retracting the current scripting buffer. The
latter would be adequate, if you just want to add a lemma in the
ancestor and want to continue the development in the
current scripting buffer without interruption.
The customization settings for multiple file support of Coq Proof
General are in a separate customization group, the
coq-auto-compile group. To view all options in this
M-x customize-group coq-auto-compile or select
Proof-General -> Advanced -> Customize -> Coq ->
Coq Auto Compile -> Coq Auto Compile.
If non-nil, check dependencies of required modules and compile if necessary.
If non-nil ProofGeneral intercepts "Require" commands and checks if the required library module and its dependencies are up-to-date. If not, they are compiled from the sources before the "Require" command is processed.
This option can be set/reset via menu ‘Coq -> Settings -> Compile Before Require’.
Buffers to save before checking dependencies for compilation.
There are two orthogonal choices: Firstly one can save all or only the coq buffers, where coq buffers means all buffers in coq mode except the current buffer. Secondly, Emacs can ask about each such buffer or save all of them unconditionally.
This makes four permitted values:
'ask-coq to confirm saving all
modified Coq buffers,
'ask-all to confirm saving all modified
'save-coq to save all modified Coq buffers without
'save-all to save all modified buffers without
The following two options deal with the load path. Proof General
divides the load path into the standard load path (which is
hardwired in the tools and need not be set explicitly), the
nonstandard load path (which must always be set explicitly), and
the current directory (which must be set explicitly for
coqdep). The option
coq-load-path determines the
nonstandard load path and
determines whether the current directory is put into the load
Non-standard coq library load path.
This list specifies the LoadPath extension for coqdep, coqc and coqtop. Usually, the elements of this list are strings (for "-I") or lists of two strings (for "-R" dir "-as" path).
The possible forms of elements of this list correspond to the 3
forms of include options (’-I’ and
'-R'). An element can be
- A string, specifying a directory to be mapped to the empty logical path ('-I'). - A list of the form '(rec dir path)' (where dir and path are strings) specifying a directory to be recursively mapped to the logical path
For convenience the symbol
'rec' can be omitted and entries of
the form ’(dir path)’ are interpreted as ’(rec dir path)’.
Under normal circumstances this list does not need to
contain the coq standard library or "." for the current
directory (see ‘
If ‘t’ let coqdep search the current directory too.
Should be ‘t’ for normal users. If ‘t’ pass "-I dir" to coqdep when processing files in directory "dir" in addition to any entries in ‘
The following two options configure an external compilation process.
External compilation command. If empty ProofGeneral compiles itself.
If unset (the empty string) ProofGeneral computes the dependencies of required modules with coqdep and compiles as necessary. This internal dependency checking does currently not handle ML modules.
If a non-empty string, the denoted command is called to do the dependency checking and compilation. Before executing this command the following keys are substituted as follows:
%p the (physical) directory containing the source of the required module %o the Coq object file in the physical directory that will be loaded %s the Coq source file in the physical directory whose object will be loaded %q the qualified id of the "Require" command %r the source file containing the "Require"
For instance, "make -C %p %o" expands to "make -C bar foo.vo" when module "foo" from directory "bar" is required.
After the substitution the command can be changed in the
minibuffer if ‘
coq-confirm-external-compilation’ is t.
If set let user change and confirm the compilation command.
Otherwise start the external compilation without confirmation.
This option can be set/reset via menu ‘Coq -> Settings -> Confirm External Compilation’.
Locking ancestors can be disabled with the following option.
If non-nil, lock ancestor module files.
If external compilation is used (via ‘
only the direct ancestors are locked. Otherwise all ancestors are
locked when the "Require" command is processed.
The following option controls which warnings of
are treated as errors.
Regexp to match errors in the output of coqdep.
coqdep indicates errors not always via a non-zero exit status, but sometimes only via printing warnings. This regular expression is used for recognizing error conditions in the output of coqdep (when coqdep terminates with exit status 0). Its default value matches the warning that some required library cannot be found on the load path and ignores the warning for finding a library at multiple places in the load path. If you want to turn the latter condition into an error, then set this variable to "^\*\*\* Warning".
The following two options do only influence the behaviour if Proof General does dependency checking and compilation itself. These options determine whether Proof General should descend into other Coq libraries and into the Coq standard library.
Directories in which ProofGeneral should not compile modules.
List of regular expressions for directories in which ProofGeneral should not compile modules. If a library file name matches one of the regular expressions in this list then ProofGeneral does neither compile this file nor check its dependencies for compilation. It makes sense to include non-standard coq library directories here if they are not changed and if they are so big that dependency checking takes noticeable time.
If non-nil, ProofGeneral does not compile modules from the coq library.
Should be ‘t’ for normal coq users. If ‘nil’ library modules are compiled if their sources are newer.
This option has currently no effect, because Proof General uses coqdep to translate qualified identifiers into library file names and coqdep does not output dependencies in the standard library.
The last three Emacs constants are internal parameters. They only need to be changed under very special, unforeseen circumstances. They can only be set in Emacs lisp code because they are no customizable user options.
Substitutions for ‘
Value must be a list of substitutions, where each substitution is a 2-element list. The first element of a substitution is the regexp to substitute, the second the replacement. The replacement is evaluated before passing it to ‘
it might be a string, or one of the symbols
'requiring-file, which are bound to, respectively, the physical
directory containing the source file, the Coq object file in
'physical-dir that will be loaded, the Coq source file in
'physical-dir whose object will be loaded, the qualified module
identifier that occurs in the "Require" command, and the file
that contains the "Require".
Regular expression matching Require commands in Coq.
Should match "Require" with its import and export variants up to (but not including) the first character of the first required module. The required modules are matched separately with ‘
Regular expression matching one Coq module identifier.
Should match precisely one complete module identifier and surrounding white space. The module identifier must be matched with group number 1. Note that the trailing dot in "Require A." is not part of the module identifier and should therefore not be matched by this regexp.
In the current release some aspects of multiple file support have not been implemented. The following points will hopefully addressed in the next release:
Declare ML Modulecommands.
Coq allows the user to enter top-level commands while editing a proof script. For example, if the user realizes that the current proof will fail without an additional axiom, he or she can add that axiom to the system while in the middle of the proof. Similarly, the user can nest lemmas, beginning a new lemma while in the middle of an earlier one, and as the lemmas are proved or their proofs aborted they are popped off a stack.
Coq Proof General supports this feature of Coq. Top-level commands entered while in a proof are well backtracked. If new lemmas are started, Coq Proof General lets the user work on the proof of the new lemma, and when the lemma is finished it falls back to the previous one. This is supported to any nesting depth that Coq allows.
Warning! Using Coq commands for navigating inside the different proofs
Resume and especially
Suspend) are not supported,
backtracking will break syncronization.
Special note: The old feature that moved nested proofs outside the current proof is disabled.
Another feature that Coq allows is the extension of the grammar of the
proof assistant by new tactic commands. This feature interacts with the
proof script management of Proof General, because Proof General needs to
know when a tactic is called that alters the proof state. When the user
tries to retract across an extended tactic in a script, the algorithm
for calculating how far to undo has a default behavior that is not
always accurate in proof mode: do "
Coq Proof General does not currently support dynamic tactic extension in Coq: this is desirable but requires assistance from the Coq core. Instead we provide a way to add tactic and command names in the ‘.emacs’ file. Four Configurable variables allows to register personal new tactics and commands into four categories:
Back" to be backtracked;
Undo" to be backtracked;
We give an example of existing commands that fit each category.
coq-user-state-preserving-commands: example: "
coq-user-state-changing-commands: example: "
coq-user-state-changing-tactics: example: "
coq-user-state-preserving-tactics: example: "
This variables are regexp string lists. See their documentations in
C-h v coq-user...) for details on how to set them in your
Here is a simple example:
(setq coq-user-state-changing-commands '("MyHint" "MyRequire")) (setq coq-user-state-preserving-commands '("Show\\s-+Mydata"))
The regexp character sequence
\\s-+ means "one or more
whitespaces". See the Emacs documentation of
regexp-quote for the
syntax and semantics. WARNING: you need to restart Emacs to make the
changes to these variables effective.
In case of losing synchronization, the user can use C-c C-z to
move the locked region to the proper position,
proof-frob-locked-end, see section Escaping script management) or
C-c C-v to re-issue an erroneously back-tracked tactic without
recording it in the script.
Holes are an experimental feature for complex expression editing by filling in templates. It is inspired from other tools, like Pcoq (http://www-sop.inria.fr/lemme/pcoq/index.html). The principle is simple, holes are pieces of text that can be "filled" by various means. The Coq command insertion menu system makes use of the holes system. Almost all holes operations are available in the Holes menu.
Notes: Holes make use of the Emacs abbreviation mechanism, it will
work without problem if you don’t have an abbrev table defined for Coq
in your config files. Use
C-h v abbrev-file-name to see the name
of the abbreviation file.
If you already have such a table it won’t be automatically overwritten
(so that you keep your own abbreviations). But you must read the abbrev
file given in the Proof General sources to be able to use the command
insertion menus. You can do the following to merge your abbreviations
with ProofGeneral’s abbreviations:
M-x read-abbrev-file, then
select the file named
coq-abbrev.el in the
ProofGeneral/coq directory. At Emacs exit you will be asked if
you want to save abbrevs; answer yes.
Starting with Proof General version 4.2 and Coq version 8.4, Coq Proof General has full support for proof-tree visualization, see section Graphical Proof-Tree Visualization.
Proof-tree visualization does currently neither support bullets and braces nor the command “Grab Existential Variables”.
For the visualization to work properly, proofs must be started with “Proof.”, which is encouraged practice anyway (see Coq Bug #2776).
|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|
This document was generated by David Aspinall on October 19, 2012 using texi2html 1.82.
Click here to go back to the front page.