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

10.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 “Search ” 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).

10.2 Using the Coq project file

The Coq project file is the recommended way to configure the Coq load path and the mapping of logical module names to physical file path (-R,-Q,-I options). The project file is typically named _CoqProject and must be located at the directory root of your Coq project. Proof General searches for the Coq project file starting at the current directory and walking the directory structure upwards. The Coq project file contains the common options (especially -R) and a list of the files of the project, see the Coq reference manual, Section “Building a Coq project”.

The Coq project file should contain something like:

-R foo bar
-I foo2
-arg -foo3
file.v
bar/other_file.v
...

Proof General only extracts the common options from the Coq project file and uses them for coqtop background processes as well as for coqdep and coqc when you use the auto compilation feature, Automatic Compilation in Detail. For the example above, Proof General will start coqtop -emacs -foo3 -R foo bar -I foo2 (remark: -emacs is always added to the options).

NOTE: -arg must be followed by one and only one option to pass to coqtop/coqc, use several -arg to issue several options. One per line (limitation of Proof General).

For backward compatibility, one can also configure the load path with the option coq-load-path, but this is not compatible with CoqIde or coq_makefile.

NOTE: the Coq project file cannot define which version of coqtop is launched. See section Opam-switch-mode support for how to switch between different Coq versions. Alternatively, for a fixed version, you need either to launch emacs with the right executable in the path or use file variables (see section Using file variables below or see (emacs)File Variables) or directory variables, see (emacs)Directory Variables.

10.2.1 Changing the name of the coq project file

To change the name of the Coq project file, configure coq-project-filename (select menu Proof-General -> Advanced -> Customize -> Coq and scroll down to “Coq Project Filename”). Customizing coq-project-filename this way will change the Coq project file name permanently and globally.

If you only want to change the name of the Coq project file for one project you can set the option as local file variable, Using file variables. This can be done either directly in every file or once for all files of a directory tree with a .dir-locals.el file, see (emacs)Directory Variables. The file .dir-locals.el should then contain

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

Note that variables set in .dir-locals.el are automatically made buffer local (such that files in different directories can have their independent setting of coq-project-filename). If you make complex customizations using eval in .dir-locals.el, you might want to add appropriate calls to make-local-variable.

Documentation of the user option coq-project-filename:

Variable: coq-project-filename: The name of coq project file.
The coq project file of a coq development (cf. Coq documentation on "makefile generation") should contain the arguments given to coq_makefile. In particular it contains the -I and -R options (preferably one per line). If ‘coq-use-coqproject’ is t (default) the content of this file will be used by Proof General to infer the ‘coq-load-path’ and the ‘coq-prog-args’ variables that set the coqtop invocation by Proof General. This is now the recommended way of configuring the coqtop invocation. Local file variables may still be used to override the coq project file’s configuration. .dir-locals.el files also work and override project file settings.

10.2.2 Disabling the coq project file mechanism

To disable the Coq project file feature in Proof General, set coq-use-project-file to nil (select menu Proof-General -> Advanced -> Customize -> Coq and scroll down to “Coq Use Project File”).

Variable: coq-use-project-file: If t, when opening a Coq file read the dominating _CoqProject.
If t, when a Coq file is opened, Proof General will look for a project file (see ‘coq-project-filename’) somewhere in the current directory or its parent directories. If there is one, its contents are read and used to determine the arguments that must be given to coqtop. In particular it sets the load path (including the -R lib options) (see ‘coq-load-path’).

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

10.3 Proof using annotations

In order to process files asynchronously and pre-compile files (.vos and .vok files), it is advised (inside sections) to list the section variables (and hypothesis) on which each lemma depends on. This must be done at the beginning of a proof with this syntax:

Lemma foo: ... .
Proof using x y H1 H2.

If the annotation is missing, then at Qed time (i.e. later in the script) coq complains with a warning and a suggestion of a correct annotation that should be added. ProofGeneral intercepts this suggestion and stores relevant information. Then depending on user preference it can either

insert immediately the “using...” annotation after “Proof”, without replaying the proof.
highlight the place where the annotation should be inserted and allow the user to perform the insertion later either via right click menu on the proof or by M-x coq-insert-suggested-dependency (it won’t replay the proof)
ask the user each time which of the two solutions above he wants
ignore completely the suggestion.

This can be configured either via Coq menu or by setting variable coq-accept-proof-using-suggestion to one of the following values: 'always, 'highlight, 'ask or 'never.

10.4 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 some buffers and compile some files. When automatic (re-)compilation is enabled (it’s off by default), one can freely work in different buffers within one Proof General session. 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.

Parallel asynchronous compilation (stable, default): 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. Compiled interfaces (-vos for Coq 8.11 or newer) and quick compilation (-quick/-vio for Coq 8.5 or newer) is supported with various modes, Quick and inconsistent compilation.
Synchronous single threaded compilation (obsolete): With synchronous compilation, coqdep and coqc are called synchronously for each Require command. Proof General is locked until the compilation finishes. Neither quick nor vos compilation is supported with synchronously compilation.

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

Set the option coq-compile-before-require (menu Coq -> Auto Compilation -> Compile Before Require) to enable compilation before processing Require commands. By default, this enables parallel asynchronous compilation.
Nonstandard load path elements must be configured via a Coq project file (this is the recommended option), Using the Coq project file or via option coq-load-path. -I or -R options in coq-prog-name or coq-prog-args must be deleted.
Configure coq-max-background-compilation-jobs if you want to limit the number of parallel background jobs and set coq-compile-keep-going (menu Coq -> Auto Compilation -> Keep going) to let compilation continue after the first error.

To abort parallel background compilation, use C-c C-c (proof-interrupt-process), the tool bar interrupt icon, the menu entry Abort Background Compilation (menu Coq -> Auto Compilation) or kill the Coq toplevel via C-c C-x (proof-shell-exit). To abort synchronous single threaded compilation, simply hit C-g.

10.4.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 has finished.

Declare ML Module commands are currently not recognized and dependencies on ML Modules reported by coqdep are ignored.

Proof General uses coqdep to determine which libraries a Require command will load and which files must be up-to-date. Because Proof General cannot know whether files are updated outside of Emacs, it checks for every Require command the complete dependency tree and recompiles files as necessary.

Output from the compilation is only shown in case of errors. It then appears in the buffer *coq-compile-response*. One can use C-x ` (bound to next-error, see (emacs)Compilation Mode) to jump to error locations. Sometimes the compilation commands do not produce error messages with location information, then C-x ` does only work in a limited way.

Proof General supports both vos and quick/vio compilation to speed up compilation of required modules at the price of consistency. Because quick/vio compilation does not seem to have a benefit with vos compilation present, the former is only supported for Coq before 8.11. Both can be configured via the settings coq-compile-vos and coq-compile-quick and via menu entries in Coq -> Auto Compilation, Quick and inconsistent compilation.

Similar to make -k, background compilation can be configured to continue as far as possible after the first error, see option coq-compile-keep-going (menu Coq -> Auto Compilation -> Keep going). The keep-going option applies to errors from coqdep and coqc. However, when starting coqc or coqdep fails), the compilation is immediately aborted.

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 old, now outdated version supported since Proof General 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. This method supports compilation via an external command (such as make), see option coq-compile-command in Customizing Coq Multiple File Support below. Synchronous compilation does neither support quick/vio nor vos compilation.

Parallel asynchronous compilation

This is the newer, recommended and default 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. To abort the background compilation process, use C-c C-c (proof-interrupt-process), the tool bar interrupt icon, the menu entry Abort Background Compilation (menu Coq -> Auto Compilation) or kill the Coq toplevel via C-c C-x (proof-shell-exit).

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.

Parallel asynchronous compilation supports both vos and quick/vio compilation, but exclusively, depending on the Coq version, Quick and inconsistent compilation.

10.4.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 your 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 menu Coq -> Auto Compilation -> Lock Ancestors or coq-lock-ancestors (Customizing Coq Multiple File Support). Alternatively, 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.]

10.4.3 Quick and inconsistent compilation

Coq now supports two different modes for speeding up compilation at the price of consistency. Since Coq 8.11, -vos compiles interfaces into .vos files and since Coq 8.5 -quick/-vio produces .vio files. Proof General supports both modes with parallel asynchronous compilation, but exclusively, depending on the detected Coq version. For Coq 8.11 or newer only -vos can be used. There are a number of different compilation options supported, see below.

For Coq 8.11 or newer (decided by the automatic Coq version detection of Proof General or by the setting coq-pinned-version) required modules are either compiled to .vo or .vos files, depending on the setting coq-compile-vos, which can also be set on menu Coq -> Auto Compilation -> vos compilation. There are four choices:

vos-and-vok: First compile using -vos, skipping proofs. When compilation finished, run coqc -vok in a second stage to check proofs on all files that require it. Some universe constraints might be missed, rendering this method possibly inconsistent.
vos: Only compile using -vos, skipping proofs. No coqc -vok run to check proofs. Obviously inconsistent.
ensure-vo: Compile without -vos to .vo files, checking all proofs and universe constraints. Only consistent choice.
unset (nil): Compile with -vos if coq-compile-quick (see below) equals quick-no-vio2vo. Otherwise compile without -vos to .vo. This value provides an upgrade path for users that configured coq-compile-quick in the past.

For vos-and-vok the second -vok stage runs asynchronously coq-compile-second-stage-delay seconds after the last Require command has been processed. Errors might pop up later and interrupt your normal interaction with Coq. Because the second stage is not time critical, it runs on coq-max-background-second-stage-percentage per cent of the cores configured for the first stage. When coq-compile-keep-going is configured and an error occurs, the second -vok stage is run on those dependencies not affected by the error.

For Coq version 8.5 until before 8.11, Proof General supports quick or vio compilation with parallel asynchronous compilation. There are 4 modes that can be configured with coq-compile-quick or by selecting one of the radio buttons in the Coq -> Auto Compilation -> Quick compilation menu. For Coq before 8.11 coq-compile-vos is ignored.

Value no-quick was provided for the transition, for those that have not switched there development to Proof using. Use quick-no-vio2vo, if you want quick recompilation without producing .vo files. Option quick-and-vio2vo recompiles with -quick/-vio as quick-no-vio2vo does, but schedules a second vio2vo stage for missing .vo files. Finally, use ensure-vo for only importing .vo files with complete universe checks.

Note that with all of no-quick, quick-no-vio2vo and quick-and-vio2vo your development might be unsound because proofs might have been skipped and universe constraints are not fully present in .vio files.

There are a few peculiarities of quick compilation in Coq 8.5 and possibly also in other versions.

Quick compilation runs noticeably slower when section variables are not declared via Proof using.
Even when section variables are declared, quick compilation runs slower on very small files, probably because of the comparatively big size of the .vio files. You can speed up quick compilation noticeably by running on a RAM disk.
If both, the .vo and the .vio files are present, Coq loads the more recent one, regardless of whether -quick, and emits a warning when the .vio is more recent than the .vo.
Under some circumstances, files compiled when only the .vio file of some library was present are not compatible with (other) files compiled when also the .vo file of that library was present, see Coq issue #5223 for details. As a rule of thumb one should run vio2vo compilation only before or after library loading.
Apart from the previous point, Coq works fine when libraries are present as a mixture of .vio and .vo files. While make insists on building all prerequisites as either .vio or .vo files, Proof General just checks whether an up-to-date compiled library file is present.
To ensure soundness, all library dependencies must be compiled as .vo files and loaded into one Coq instance.

Detailed description of the 4 possible settings of coq-compile-quick:

no-quick

Compile outdated prerequisites without -quick, producing .vo files, but don’t compile prerequisites for which an up-to-date .vio file exists. Delete or overwrite outdated .vo files.

quick-no-vio2vo

Compile outdated prerequisites with -quick, producing .vio files, but don’t compile prerequisites for which an up-to-date .vo file exists. Delete or overwrite outdated .vio files.

quick-and-vio2vo

Same as quick-no-vio2vo, but start a second vio2vo stage for missing .vo files. Everything described previously for the second -vok stage applies here as well.

Warning: This mode does only work when you process require commands in batches. Slowly single-stepping through require’s might lead to inconsistency errors when loading some libraries, see Coq issue #5223. To mitigate this risk, vio2vo compilation only starts after a certain delay after the last require command of the current queue region has been processed. This is controlled by coq-compile-second-stage-delay, Customizing Coq Multiple File Support.

ensure-vo

Ensure that all library dependencies are present as .vo files and delete outdated .vio files or .vio files that are more recent than the corresponding .vo file. This setting is the only one that ensures soundness.

The options no-quick and ensure-vo are compatible with Coq 8.4 or older. When Proof General detects such an older Coq version, it changes the quick compilation mode automatically. For this to work, the option coq-compile-quick must only be set via the customization system or via the menu.

10.4.4 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 -> Auto Compilation -> 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.

This option can be set via menu ‘Coq -> Auto Compilation -> Auto Save’.

The following options configure parallel compilation.

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 -> Auto Compilation -> Compile Parallel In Background’.

The options coq-compile-vos and coq-compile-quick are described in detail above, Quick and inconsistent compilation.

Variable: coq-compile-keep-going

Continue compilation after the first error as far as possible.
Similar to ‘`make -k’’, with this option enabled, the background compilation continues after the first error as far as possible. With this option disabled, background compilation is immediately stopped after the first error.

This option can be set/reset via menu ‘Coq -> Auto Compilation -> Keep going’.

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.

Variable: coq-max-background-second-stage-percentage

Percentage of ‘coq-max-background-compilation-jobs’ for the second stage.
This setting configures the maximal number of ‘`-vok’’ or vio2vo background jobs running in a second stage as percentage of ‘coq-max-background-compilation-jobs’.

For backward compatibility, if this option is not customized, it is initialized from the now deprecated option ‘coq-max-background-vio2vo-percentage’.

Variable: coq-compile-second-stage-delay

Delay in seconds before starting the second stage compilation.
The delay is applied to both ‘`-vok’’ and vio2vo second stages. For Coq < 8.11 and vio2vo delay helps to avoid running into a library inconsistency with 'quick-and-vio2vo, see Coq issue #5223.

For backward compatibility, if this option is not customized, it is initialized from the now deprecated option ‘coq-compile-vio2vo-delay’.

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.

This option can be set via menu ‘Coq -> Auto Compilation -> Lock Ancestors’.

The sequential compilation setting supports an external compilation command (which could be a parallel running make). For this set coq-compile-parallel-in-background to nil and configure the compilation command in coq-compile-command.

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 -> Auto Compilation -> Confirm External Compilation’.

The preferred way to configure the load path and the mapping of logical library names to physical file path is the Coq project file, Using the Coq project file. Alternatively one can configure these things with the following options.

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 path and "-Q" dir path).

The possible forms of elements of this list correspond to the 4 forms of include options (‘-I’ ‘-Q’ and ‘-R’). An element can be

  - A list of the form ‘(’ocamlimport dir)', specifying (in 8.5) a
    directory to be added to ocaml 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 path’).
  - A list of the form ‘(’recnoimport dir path)' (where dir and
    path are strings) specifying a directory to be recursively
    mapped to the logical path ‘path’ (‘-Q dir path’), but not
    imported (modules accessible for import with qualified names
    only).  Note that -Q dir "" has a special, nonrecursive meaning.
  - A list of the form (8.4 only) ‘(’nonrec 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)’.

A plain string maps to -Q ... "" in 8.5, and -I ... in 8.4.

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

warning: if you use coq <= 8.4, the meaning of these options is not the same (-I is for coq path).

Variable: coq-load-path-include-current

If t, let coqdep search the current directory too.
Should be t for normal users. If t, pass -Q dir "" to coqdep when processing files in directory "dir" in addition to any entries in ‘coq-load-path’.

This setting is only relevant with Coq < 8.5.

During library dependency checking Proof General does not dive into the Coq standard library or into libraries that are installed as user contributions. This stems from coqdep, which does not output dependencies to these directories. The internal dependency check can also ignore additional libraries.

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. The regular expressions in here are always matched against the .vo file name, regardless whether ‘`-quick’’ would be used to compile the file or not.

10.4.5 Current Limitations

No support for Declare ML Module commands and files depending on an ML module.
When a compiled library has the same time stamp as the source file, it is considered outdated. Some old file systems (for instance ext3) or Emacs before version 24.3 support only time stamps with one second granularity. On such configurations Proof General will perform some unnecessary compilations.

10.5 Omitting proofs for speed

To speed up asserting larger chunks, Proof General can omit complete opaque proofs by silently replacing the whole proof script with Admitted, Script processing commands. For files with big proofs this can bring down the processing time to 10% with the obvious disadvantage that errors in the omitted proofs go unnoticed.

The omit-proof feature works when

proofs are not nested
opaque and non-opaque proofs start with Proof. or Proof using
opaque proofs end with Qed or Admitted
non-opaque proofs or definition end with Defined

Aborted proofs can be present if they start with a variant of Proof and end with Abort. They are handled like non-opaque proofs (i.e., not omitted).

To enable omitting proofs, configure proof-omit-proofs-option or select Proof-General -> Quick Options -> Processing -> Omit Proofs.

For both, proof-goto-point and proof-process-buffer, a prefix argument toggles the omit-proofs feature for one invocation.

If a nested proof is detected while searching for opaque proofs to omit, a warning is displayed and the complete remainder of the asserted region is sent unmodified to Coq.

If the proof script relies on sections, it is highly recommended to use a Proof using annotation for all lemmas contained in a Section, otherwise Coq will compute a wrong type for these lemmas when this omitting-proofs feature is enabled.

To automate this, we recall that ProofGeneral provides a dedicated feature to generate these Proof using annotations (a defective form being e.g. Proof using Type if no section hypothesis is used), see the menu command Coq > "Proof using" mode and Proof using annotations for details.

Note that the omit-proof feature works by examining the asserted region with different regular expressions to recognize proofs and to differentiate opaque from non-opaque proofs. This approach is necessarily imprecise and the omit-proofs feature may therefore cause unexpected errors in the proof script. Currently, Proof General correctly handles the following cases for Coq.

Commands, such as Hint, that may appear inside proofs but may have effects outside the proof cause the proof to be considered as non-opaque.
A Let declaration followed by a proof to supply the term causes this proof to be considered as non-opaque. Note that such declarations are only handled correctly if the Let and the proof are asserted together. If the proof is asserted separately it may be treated as opaque and thus be omitted.

The following cases are currently not handled correctly.

All capitalized commands make Proof General believe the proof is non-opaque, even if they have proof-local effect only, such as Focus or Unshelve.

10.6 Proof status statistic for Coq

The command proof-check-report (menu Proof-General -> Check Opaque Proofs) generates the proof status of all opaque proofs in the current buffer, i.e., it generates an overview that shows which of the opaque proofs in the current buffer are currently valid and which are failing, where Admitted proofs count as failing. This command is useful for a development process where invalid proofs are permitted and vos compilation (See section Quick and inconsistent compilation) and the omit proofs feature (See section Omitting proofs for speed) are used to work at the most interesting or challenging point instead of on the first invalid proof.

The command proof-check-annotate (menu Proof-General -> Annotate Failing Proofs) can then be used to consistently annotate failing proofs with a FAIL comment or to check, e.g., in continuous integration, that such comments are present.

See See section Proof status statistic for more details.

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

Special note: The old feature that moved nested proofs outside the current proof is disabled.

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

10.9 Indentation tweaking

Indentation of Coq script is provided by Proof General, but it may behave badly especially if you use syntax extensions. You can sometimes fix this problem by telling PG that some token should be considered as identical to other ones by the indentation mechanism. Use the two variables coq-smie-user-tokens and coq-smie-monadic-tokens. This variables contains associations between user tokens and the existing pg tokens they should be equated too.

coq-smie-user-tokens
this is where users should put ther own tokens. For instance:
(setq coq-smie-user-tokens '((\"xor\" . \"or\") (\"ifb\" . \"if\")))
to have token \"xor\" and \"ifb\" be considered as having
coq-smie-monadic-tokens
is specific to monadic operators: it contains usual monadic notations by default (but you can redefine it if needed).

Specific tokens are defined for the two usual monadic forms:
```
"let monadic" E "<- monadic" E "in monadic" E
E "<- monadic" E ";; monadic" E
```
The default value of coq-smie-monadic-tokens gives the following concrete syntax to these tokens:
((";;" . ";; monadic") ("do" . "let monadic") ("<-" . "<- monadic") (";" . "in monadic"))
thus allowing for the following:
```
  do x <- foo;
  do y <- bar;
  ...
```
and
```
  x <- foo;;
  y <- bar;;
  ...
```

NOTE: This feature is experimental.

NOTE: the “pg tokens” are actually the ones PG generates internally by exploring the file around the indentation point. Consequently this refers to internals of PoofGeneral. Contact the Proof General team if you need help.

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

10.11 Proof-Tree Visualization

Starting with Proof General version 4.5 and Coq version 8.11, Coq Proof General has (again) 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.

10.12 Showing Proof Diffs

Coq 8.10 supports automatically highlighting the differences between successive proof steps in Proof General. The feature is described in the Coq Documentation, section Showing differences between proof steps.

The Coq proof diff does more than a basic "diff" operation. For example:

diffs are computed on a per-token basis (as determined by the Coq lexer) rather than on a per-character basis, probably a better match for how people understand the output. (For example, a token-based diff between "abc" and "axc" will highlight all of "abc" and "axc" as a difference, while a character-based diff would indicate that "a" and "c" are in common and that only the "b"/"x" is a difference.)
diffs ignore the order of hypotheses
tactics that only change the proof view are handled specially, for example "swap" after a "split" will show the diffs between before "split" and after "swap", which is more useful
some error messages have been instrumented to show diffs where it is helpful

To enable or disable diffs, set coq-diffs (select menu Coq -> Diffs) to "on", "off" or "removed". "on" highlights added tokens with the background color from diff-refine-added. "removed" highlights removed tokens with the background color from diff-refine-removed. With the "removed" setting, lines that have both added and removed text may be shown twice, as "before" and "after" lines. To preserve the settings for the next time you start Proof General, select Coq -> Settings -> Save Settings.

The colors used to highlight diffs are configurable in the Proof-General -> Advanced -> Customize -> Proof Faces menu. The 4 Coq Diffs ... faces control the highlights. Lines that have added or removed tokens are shown with the entire line highlighted with a Coq Diffs ... Bg face. The added or removed tokens themselves are highlighted with non-Bg faces.

10.13 Opam-switch-mode support

Coq can be installed using opam (the OCaml package manager), which makes it easy to manage several different switches, having each a different version of Coq.

Instead of running a command like opam switch ... in a terminal and restarting emacs to benefit from a different switch, one can:

Install the opam-switch-mode and use the dedicated mode bar menu OPSW it provides.
Configure Proof General using the customization option coq-kill-coq-on-opam-switch, so that the Coq background process is killed when changing the opam switch through opam-switch-mode.

Variable: coq-kill-coq-on-opam-switch

If t kill coq when the opam switch changes (requires ‘opam-switch-mode’).
When ‘opam-switch-mode’ is loaded and the user changes the opam switch through ‘opam-switch-mode’ then this option controls whether the coq background process (the proof shell) is killed such that the next assert command starts a new proof shell, probably using a different coq version from a different opam switch.

See https://github.com/ProofGeneral/opam-switch-mode for ‘opam-switch-mode’

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