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

# 11. Coq Proof General

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

Coq Proof General supplies the following key-bindings:

`C-c C-a C-i`

  Inserts “intros ” and also introduces the name of the hypothesis proposed by coq on the current goal.

`C-c C-a C-s`

  Show the goal (enter for the current goal, i <enter> for the ith goal).

  Add the prefix C-u to see the answer with all pretty printing options temporarily disable (Set Printing All).

`C-c C-a C-c`

  Prompts for “Check ” query arguments, the default input name is built from the identifier under the cursor.

  Add the prefix C-u to see the answer with all pretty printing options temporarily disable (Set Printing All).

`C-c C-a C-p`

  The same for a “Print ” query.

`C-c C-a C-b`

  The same for a “About ” query.

`C-c C-a C-a`

  The same for a “SearchAbout ” query (no C-u prefix).

`C-c C-a C-o`

  The same for a Search “SearchIsos” (no C-u prefix).

`C-c C-a C-)`

  Inserts “End <section-name>.” (this should work well with nested sections).

## 11.2 Using the Coq project file

Before starting the Coq process, one need to set `coqtop` options, in particular the -I and -R command that set the directories to have in the coq load path. You can use file variables (Using file variables) as it was recommended on previous versions of ProofGeneral but there is now a better way. ProofGeneral knows how to extract this information from the Coq project file if there is one. The Coq project file must be named following variable ‘coq-project-filename’ (default: `_CoqProject`) and be on the root directory of your development.

It should contain something like:

    -R foo bar
    -I foo2
    -arg -foo3

The intial use of this file is to be given to the `coq_makefile` tool to generate a Makefile (see Coq documentation for details). It is parsed by ProofGeneral to guess the command line option. In this example the command line built by Proofgeneral will be `coqtop -foo3 -R foo bar -I foo2`.

This is the recommended way of configuring coqtop options for coq compilation, CoqIde and Proofgeneral. Its main advantage is that it avoids duplicating informations between these three tools.

For specific (and rare) per file configuration one can still use file variables (Using file variables).

### 11.2.1 Changing the name of the coq project file

One can change the name of the project file by:

(setq coq-project-filename "myprojectfile")

or:

(setq (make-local-variable ’coq-project-filename) "myprojectfile")

If this is for a project, the best is probably to have a .dir-locals.el at the root of the project, as explained in Using file variables. This file should contain something like:

    ((coq-mode . ((coq-project-filename . "myprojectfile"))))

or equivalently:

    ((coq-mode
      .
      ((eval
        .
        (progn
          (make-local-variable 'coq-project-filename)
          (setq coq-project-filename  "myprojectfile"))))))

### 11.2.2 Disabling the coq project file mechanism

If the variable ‘coq-use-project-file’ is nil, then Proofgeneral will not look at project file. therefore you can put this in your config file (.emacs) to disable the use of project file:

    (setq coq-use-project-file nil)

You can also use the .dir-locals.el as above to configure this setting on a per project basis.

## 11.3 Multiple File Support

Since version 4.1 Coq Proof General has multiple file support. It consists of the following points:

Restarting `coqtop` when changing the active scripting buffer

  Different buffers may require different load path’ or different sets of `-I` options. Because Coq cannot undo changes in the load path, Proof General is forced to restart `coqtop` when the active scripting buffer changes.

Locking ancestors

  Locking those buffers on which the current active scripting buffer depends. This is controlled by the user option `coq-lock-ancestors`, Customizing Coq Multiple File Support and Locking Ancestors.

(Re-)Compilation

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

There are actually two implementations of the Recompilation feature.

Synchronous single threaded compilation (stable)

  With synchronous compilation, coqdep and coqc are called synchronously for each Require command. Proof General is locked until the compilation finishes

Parallel asynchronous compilation (experimental)

  With parallel compilation, coqdep and coqc are launched in the background and Proof General stays responsive during compilation. Up to ‘coq-max-background-compilation-jobs’ coqdep and coqc processes may run in parallel.

To enable the automatic compilation feature, you have to follow these points:

- The option `coq-compile-before-require` must be turned on (menu `Coq -> Settings -> Compile Before Require`).
- Nonstandard load path elements must be configured in the option `coq-load-path`. `-I` options in `coq-prog-name` or `coq-prog-args` must be deleted.
- In `coq-load-path` use strings `"dir"` for `-I` options and lists of two strings `("dir" "path")` for `-R "dir" -as "path"` (for more details see the documentation of ‘coq-load-path’ or Customizing Coq Multiple File Support).
- For a nonstandard compilation procedure and limited ML module support, `coq-compile-command` can be set to an external compilation command. For standard dependency analysis with `coqdep` and compilation with `coqc` the option `coq-compile-command` can be left empty. In this case Proof General calls `coqdep` and `coqc` as needed.
- The default compilation method is synchronous compilation. In order to experience parallel background compilation on all your CPU cores, enable ‘coq-compile-parallel-in-background’ (menu `Coq -> Settings -> Compile Parallel In Background`). Configure `coq-max-background-compilation-jobs` if you want to limit the number of parallel background jobs.

### 11.3.1 Automatic Compilation in Detail

When `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. The Require command and the following text is only sent to Coq after the compilation finished.

`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 `8.3pl2`, `Require Arith` works, while `Require Arith.Le` gives an error. The use of `coqdep` is also the reason why nonstandard load path elements must be configured in `coq-load-path`.

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 `coq-compile-command` is 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 `coq-confirm-external-compilation` (menu `Coq -> Settings -> Confirm External Compilation`) determines whether the user must confirm the compilation command. The output of the compilation appears then in the `*compilation*` buffer.

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 compilation one can use `C-x `` (bound to `next-error`, 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 from `coqdep`.

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 `Coq -> Settings`).

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

With ‘coq-compile-parallel-in-background’ (menu `Coq -> Settings -> Compile Parallel In Background`) you can choose between two implementations of internal compilation.

Synchronous single threaded compilation

  This is the stable version supported since Proof General version 4.1. This method starts coqdep and coqc processes one after each other in synchronous subprocesses. Your Emacs session will be locked until compilation finishes. Use `C-g` to interrupt compilation.

Parallel asynchronous compilation

  This is the new version added in Proof General version 4.3. It runs up to `coq-max-background-compilation-jobs` coqdep and coqc jobs in parallel in asynchronous subprocesses (or uses all your CPU cores if `coq-max-background-compilation-jobs` equals `'all-cpus`). Your Emacs will stay responsive during compilation. Use `C-c C-c` or the tool bar icons for interrupt or restart to interrupt compilation.

  For the usual case, you have at most ‘coq-max-background-compilation-jobs’ parallel processes including your Proof General process. The usual case applies, when the Require commands are the first commands in the file. If you have other commands between two Require commands or before the first Require, then you may see Proof General and Coq running in addition to ‘coq-max-background-compilation-jobs’ compilation jobs.

  Actually, even with this method, not everything runs asynchronously. To translate module identifiers from the Coq sources into file names, Proof General runs coqdep on an automatically generated, one-line file. These coqdep jobs run synchronously while the Require commands are parsed. The coqdep jobs on the real source files do run asynchronously in the background.

### 11.3.2 Locking Ancestors

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.

In the default setting, when you want to edit a locked ancestor, you are forced to completely retract the current scripting buffer. You can simplify this by setting `proof-strict-read-only` to `'retract` (menu `Proof-General -> Quick Options -> Read Only -> Undo On Edit`). Then typing in some ancestor will immediately retract you current scripting buffer and unlock that ancestor.

You have two choices, if you don’t like ancestor locking in its default way. 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 `Proof-General` -> `Quick Options` -> `Read Only` -> `Freely Edit` (which will set the option `proof-strict-read-only` to `nil`).

[The right behaviour for Coq, namely to retract the current scripting buffer only up to the appropriate `Require` command, would be quite difficult to implement in the current Proof General infrastructure. Further, it has only dubious benefit, as Require commands are usually on the top of each file.]

### 11.3.3 Customizing Coq Multiple File Support

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 group do `M-x customize-group coq-auto-compile` or select menu entry `Proof-General -> Advanced -> Customize -> Coq -> Coq Auto Compile -> Coq Auto Compile`.

Variable: coq-compile-before-require

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

Variable: coq-compile-auto-save

  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 buffers, `'save-coq` to save all modified Coq buffers without confirmation and `'save-all` to save all modified buffers without confirmation.

The following two options are for the parallel compilation method.

Variable: coq-compile-parallel-in-background

  Choose the internal compilation method.
  When Proof General compiles itself, you have the choice between two implementations. If this setting is nil, then Proof General uses the old implementation and compiles everything sequentially with synchronous job. With this old method Proof General is locked during compilation. If this setting is t, then the new method is used and compilation jobs are dispatched in parallel in the background. The maximal number of parallel compilation jobs is set with ‘``coq-max-background-compilation-jobs``’.

  This option can be set/reset via menu ‘`Coq -> Settings -> Compile Parallel In Background`’.

Variable: coq-max-background-compilation-jobs

  Maximal number of parallel jobs, if parallel compilation is enabled.
  Use the number of available CPU cores if this is set to `'all-cpus`. This variable is the user setting. The value that is really used is ‘``coq-internal-max-jobs``’. Use ‘``coq-max-jobs-setter``’ or the customization system to change this variable. Otherwise your change will have no effect, because ‘``coq-internal-max-jobs``’ is not adapted.

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 `coq-load-path-include-current` determines whether the current directory is put into the load path of `coqdep`.

Variable: coq-load-path

  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 'path' ('-R dir -as path').
        - A list of the form '(norec dir path)', specifying a directory
          to be mapped to the logical path 'path' ('-I dir -as 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 ‘``coq-load-path-include-current``’).

Variable: coq-load-path-include-current

  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 ‘``coq-load-path``’.

The following two options configure an external compilation process.

Variable: coq-compile-command

  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.

Variable: coq-confirm-external-compilation

  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.

Variable: coq-lock-ancestors

  If non-nil, lock ancestor module files.
  If external compilation is used (via ‘``coq-compile-command``’) then only the direct ancestors are locked. Otherwise all ancestors are locked when the "Require" command is processed.

The following option controls which warnings of `coqdep` are treated as errors.

Variable: coq-coqdep-error-regexp

  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.

Variable: coq-compile-ignored-directories

  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.

Variable: coq-compile-ignore-library-directory

  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.

Variable: coq-compile-substitution-list

  Substitutions for ‘``coq-compile-command``’.
  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 ‘``replace-regexp-in-string``’, so it might be a string, or one of the symbols `'physical-dir`, `'module-object`, `'module-source`, `'qualified-id` and `'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".

Variable: coq-require-command-regexp

  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 ‘``coq-require-id-regexp``’

Variable: coq-require-id-regexp

  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.

### 11.3.4 Current Limitations

In the current release some aspects of multiple file support have not been implemented. The following points will hopefully be addressed at some stage.

- Support `Declare ML Module` commands.
- Increase precision when comparing modification times. Because of an Emacs limitation, modification time stamps of files have only a precision of 1 second. If several compiled Coq object files have been created in the same second, Proof General is optimistic and does not recompile. (Note that GNU make behaves the same on file systems that record time stamps only with a precision of 1 second.) Emacs version 24.3 implements high precision time stamps on files.

## 11.4 Editing multiple proofs

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.

## 11.5 User-loaded tactics

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

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:

- state changing commands, which need "`Back`" to be backtracked;
- state changing tactics, which need "`Undo`" to be backtracked;
- state preserving commands, which do not need to be backtracked;
- state preserving tactics, which do not need to be backtracked;

We give an example of existing commands that fit each category.

- `coq-user-state-preserving-commands`: example: "`Print`"
- `coq-user-state-changing-commands`: example: "`Require`"
- `coq-user-state-changing-tactics`: example: "`Intro`"
- `coq-user-state-preserving-tactics`: example: "`Idtac`"

This variables are regexp string lists. See their documentations in emacs (`C-h v coq-user...`) for details on how to set them in your ‘`.emacs`’ file.

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.

## 11.6 Holes feature

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.

## 11.7 Proof-Tree Visualization

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. To find out which versions of Prooftree are compatible with this version of Proof General, see section Graphical Proof-Tree Visualization or the Prooftree website.

For the visualization to work properly, proofs must be started with `Proof`, which is encouraged practice anyway (see Coq Bug #2776). Without `Proof` you lose the initial proof goal, possibly having two or more initial goals in the display.

To support `Grab Existential Variables` Prooftree can actually display several graphically independent proof trees in several layers.

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

This document was generated by David Aspinall on October 11, 2013 using texi2html 1.82.