Proof General

2 Basic Script Management

This chapter is an introduction to using the script management facilities of Proof General. We begin with a quick walkthrough example, then describe the concepts and functions in more detail.

Walkthrough example in Isabelle
Proof scripts
Script buffers
Summary of Proof General buffers
Script editing commands
Script processing commands
Proof assistant commands
Toolbar commands
Interrupting during trace output

2.1 Walkthrough example in Isabelle

Here’s a short example in Isabelle to see how script management is used. The file you are asked to type below is included in the distribution as isar/Example.thy. If you’re not using Isabelle, substitute some lines from a simple proof for your proof assistant, or consult the example file supplied with Proof General for your prover, called something like foo/example.foo for a proof assistant Foo.

This walkthrough is keyboard based, but you could easily use the toolbar and menu functions instead. The best way to learn Emacs key bindings is by using the menus. You’ll find the keys named below listed on the menus.

First, start Emacs with Proof General loaded. According to how you have installed Proof General, this may be by typing proofgeneral in a terminal, selecting it from a menu, or simply by starting Emacs itself.
Next, find a new file by C-x C-f and typing as the filename Walkthrough.thy. This should load Isabelle Proof General and the toolbar and Proof General menus will appear. You should have an empty buffer displayed.

The notation C-x C-f means control key with ‘x’ followed by control key with ‘f’. This is a standard notation for Emacs key bindings, used throughout this manual. This function also appears on the File menu of Emacs. The remaining commands used will be on the Proof-General menu or toolbar.

If you’re not using Isabelle, you must choose a different file extension, appropriately for your proof assistant. If you don’t know what to use, see the previous chapter for the list of supported assistants and file extensions.

Turn on electric terminator by typing C-c ; and enter:
```
theory Walkthrough imports Main begin;
```
This first command begins the definition of a new theory inside Isabelle, which extends the theory Main. (We’re assuming that you have Isabelle/HOL available, which declares the Main theory. You should be able to see the list of installed logics in Isabelle on the Logics menu).

Electric terminator sends commands to the proof assistant as you type them. At the moment you type the semicolon, the theory command will be sent to Isabelle behind the scenes. First, there is a short delay while Isabelle is launched; you may see a welcome message. Then, you may notice that the command briefly is given an orange/pink background (or shown in inverse video if you don’t have a colour display), before you see a window containing text like this:

theory Walkthrough

which reflects the command just executed.

In this case of this first command, it is hard to see the orange/pink stage because the command is processed very quickly on modern machines. But in general, processing commands can take an arbitrary amount of time (or not terminate at all). For this reason, Proof General maintains a queue of commands which are sent one-by-one from the proof script. As Isabelle successfully processes commands in the queue, they will turn from the orange/pink colour into blue.

The blue regions indicate text that has been read by the prover and should not be edited, to avoid confusion between what the prover has processed and what you are looking at. To enforce this (and avoid potentially expensive reprocessing) the blue region can be made read-only. This is controlled by the menu item:

  Proof-General -> Quick Options -> Read Only

The first option ‘Strict Read Only’ was formerly the default for Proof General, and causes the blue region to be locked. Because of this, the term locked region term is used in Proof General documentation to mean the blue portion of the text which has been processed, although it is no longer locked by default. The current default is ‘Undo on Edit’ which causes the prover to undo back to any user edits. So if you change a processed piece of text you will need to re-process it. The final option, ‘Freely Edit’, allows you to freely edit the buffer without causing the prover to reprocess it. This can quickly lead to confusion and a loss of synchronization between what you are reading and what the prover has processed, so it is best used sparingly.

Electric terminator mode is popular, but not enabled by default because of the principle of least surprise. Moreover, in Isabelle, the semicolon terminators are optional so proof scripts are usually written without them to avoid clutter. You’ll notice that although you typed a semi-colon it was not included in the buffer! The electric terminator tries to be smart about comments and strings but sometimes it may be confused (e.g., adding a semi-colon inside an already written comment), or you may need to type several terminator commands together. In this case you can use the standard Emacs quote next character, typing C-q ; to quote the semi-colon. Alternatively you can use a prefix argument, as in M-3 ; to type three semi-colons.

Without using electric terminator, you can trigger processing the text up to the current position of the point with the key C-c C-RET, or just up to the next command with C-c C-n. We show the rest of the example in Isabelle with semi-colons, but these will not appear in the final text.

Coq, on the other hand, requires a full-stop terminator at the end of each line. If you want to enable electric terminator, use the menu item: Proof-General -> Quick Options -> Processing -> Electric Terminator

If you want to keep electric terminator enabled all the time, you can customize Proof General to do so, See Customizing Proof General. For the common options, customization is easy: just use the menu item Proof General -> Quick Options to make your choices, and Proof-General -> Quick Options -> Save Options to save your choices.

Next type on a new line:
```
theorem my_theorem: "A & B --> B & A";
```

The goal we have set ourselves to prove should be displayed in the goals buffer.

Now type:
```
proof
  assume "A & C";
```

This will update the goals buffer.

But whoops! That was the wrong command, we typed C instead of B.

Press C-c C-BS to pretend that didn’t happen.

Note: BS means the backspace key. This key press sends an undo command to Isabelle, and deletes the assume command from the proof script. If you just want to undo without deleting, you can type C-c C-u instead, or use the left-arrow toolbar navigation button.

Instead, let’s try:
```
  assume "A & B";
```
Which is better.
From this assumption we can get B and A by the trivial step .. which splits the assumption using an elimination step:
```
  then obtain B and A ..;
```
Finally, we establish the goal by the trivial step .. again, which triggers an introduction rule:
```
  then show "B & A" ..;
```

After this proof step, the message from Isabelle indicates that the proof has succeeded, so we can conclude the proof with the qed command.

Finally, type:
```
qed;
```

This last command closes the proof and saves the proved theorem.

Moving the mouse pointer over the qed command now reveals that the entire proof has been aggregated into a single segment (if you did this before, you would see highlighting of each command separately).

Suppose we decide to call the theorem something more sensible. Move the cursor up into the locked region, somewhere between ‘theorem’ and ‘qed’, enter C-c C-RET.

You see that the locked segment for the whole proof is now unlocked (and uncoloured): it is transferred back into the editing region.

The command C-c C-RET moves the end of the locked region to the cursor position, or as near as possible above or below it, sending undoing commands or proof commands as necessary. In this case, the locked region will always be moved back to the end of the theory line, since that is the closest possible position to the cursor that appears before it. If you simply want to retract the whole file in one go, you can use the key C-c C-r (which corresponds to the up arrow on the toolbar), which will automatically move the cursor to the top of the file.

Now improve the goal name, for example:
```
theorem and_commutes: "A & B --> B & A"
```
You can swiftly replay the rest of the buffer now with C-c C-b (or the down arrow on the toolbar).
At the end of the buffer, you may insert the command
```
end
```
to complete the theory.

Notice that if you right-click on one of the highlighted regions in the blue area you will see a context menu for the region. This includes a “show/hide” option for folding a proof, as well as some editing commands for copying the region or rearranging its order in the processed text: “move up/move down”. (These latter commands occasionally help you reorder text without needing to reprove it, although they risk breaking the proof!)

Finally, once you are happy with your theory, you should save the file with C-x C-s before moving on to edit another file or exiting Emacs. If you forget to do this, Proof General or Emacs will surely prompt you sooner or later!

2.2 Proof scripts

A proof script is a sequence of commands which constructs definitions, declarations, theories, and proofs in a proof assistant. Proof General is designed to work with text-based interactive proof assistants, where the mode of working is usually a dialogue between the human and the proof assistant.

Primitive interfaces for proof assistants simply present a shell (command interpreter) view of this dialogue: the human repeatedly types commands to the shell until the proof is completed. The system responds at each step, perhaps with a new list of subgoals to be solved, or perhaps with a failure report. Proof General manages the dialogue to show the human only the information which is relevant at each step.

Often we want to keep a record of the proof commands used to prove a theorem, to build up a library of proved results. An easy way to store a proof is to keep a text file which contains a proof script; proof assistants usually provide facilities to read a proof script from a file instead of the terminal. Using the file, we can replay the proof script to prove the theorem again.

Using only a primitive shell interface, it can be tedious to construct proof scripts with cut-and-paste. Proof General helps out by issuing commands directly from a proof script file, while it is being written and edited. Proof General can also be used conveniently to replay a proof step-by-step, to see the progress at each stage.

Scripting is the process of building up a proof script file or replaying a proof. When scripting, Proof General sends proof commands to the proof assistant one at a time, and prevents you from editing commands which have been successfully completed by the proof assistant, to keep synchronization. Regions of the proof script are analysed based on their syntax and the behaviour of the proof assistant after each proof command.

2.3 Script buffers

A script buffer is a buffer displaying a proof script. Its Emacs mode is particular to the proof assistant you are using (but it inherits from proof-mode).

A script buffer is divided into three regions: locked, queue and editing. The proof commands in the script buffer can include a number of Goal-save sequences.

Locked, queue, and editing regions
Goal-save sequences
Active scripting buffer

2.3.1 Locked, queue, and editing regions

The three regions that a script buffer is divided into are:

The locked region, which appears in blue (underlined on monochrome displays) and contains commands which have been sent to the proof process and verified. The commands in the locked region cannot be edited.
The queue region, which appears in pink (inverse video) and contains commands waiting to be sent to the proof process. Like those in the locked region, these commands can’t be edited.
The editing region, which contains the commands the user is working on, and can be edited as normal Emacs text.

These three regions appear in the buffer in the order above; that is, the locked region is always at the start of the buffer, and the editing region always at the end. The queue region only exists if there is input waiting to be processed by the proof process.

Proof General has two fundamental operations which transfer commands between these regions: assertion (or processing) and retraction (or undoing).

Assertion causes commands from the editing region to be transferred to the queue region and sent one by one to the proof process. If the command is accepted, it is transferred to the locked region, but if an error occurs it is signalled to the user, and the offending command is transferred back to the editing region together with any remaining commands in the queue.

Assertion corresponds to processing proof commands, and makes the locked region grow.

Retraction causes commands to be transferred from the locked region to the editing region (again via the queue region) and the appropriate ’undo’ commands to be sent to the proof process.

Retraction corresponds to undoing commands, and makes the locked region shrink. For details of the commands available for doing assertion and retraction, See Script processing commands.

2.3.2 Goal-save sequences

A proof script contains a sequence of commands used to prove one or more theorems.

As commands in a proof script are transferred to the locked region, they are aggregated into segments which constitute the smallest units which can be undone. Typically a segment consists of a declaration or definition, or all the text from a goal command to the corresponding save (e.g. qed) command, or the individual commands in the proof of an unfinished goal. As the mouse moves over the the region, the segment containing the pointer will be highlighted.

Proof General therefore assumes that the proof script has a series of proofs which look something like this:

   goal mythm is G
   …
   save theorem mythm

interspersed with comments, definitions, and the like. Of course, the exact syntax and terminology will depend on the proof assistant you use.

The name mythm can appear in a menu for the proof script to help quickly find a proof (see Imenu and Speedbar).

2.3.3 Active scripting buffer

You can edit as many script buffers as you want simultaneously, but only one buffer at a time can be used to process a proof script incrementally: this is the active scripting buffer.

The active scripting buffer has a special indicator: the word Scripting appears in its mode line at the bottom of the screen. This is coloured to indicate the status: if it has a pink or blue background, the prover is processing the text (busy when pink). If it is in green, the buffer is completely processed.

When you use a scripting command, it will automatically turn a buffer into the active scripting mode. You can also do this by hand, via the menu command ’Toggle Scripting’ or the key C-c C-s.

C-c C-s: proof-toggle-active-scripting

When active scripting mode is turned on, several things may happen to get ready for scripting (exactly what happens depends on which proof assistant you are using and some user settings). First, the proof assistant is started if it is not already running. Second, a command is sent to the proof assistant to change directory to the directory of the current buffer. If the current buffer corresponds to a file, this is the directory the file lives in. This is in case any scripting commands refer to files in the same directory as the script. The third thing that may happen is that you are prompted to save some unsaved buffers. This is in case any scripting commands may read in files which you are editing. Finally, some proof assistants may automatically read in files which the current file depends on implicitly. In Isabelle, for example, there is an implicit dependency between a .ML script file and a .thy theory file which defines its theory.

If you have a partly processed scripting buffer and use C-c C-s, or you attempt to use script processing in a new buffer, Proof General will ask you if you want to retract what has been proved so far, Scripting incomplete in buffer myproof.v, retract? or if you want to process the remainder of the active buffer, Completely process buffer myproof.v instead? before you can start scripting in a new buffer. If you refuse to do either, Proof General will give an error message: Cannot have more than one active scripting buffer!.

To turn off active scripting, the buffer must be completely processed (all blue), or completely unprocessed. There are two reasons for this. First, it would certainly be confusing if it were possible to split parts of a proof arbitrarily between different buffers; the dependency between the commands would be lost and it would be tricky to replay the proof.³ Second, we want to interface with file management in the proof assistant. Proof General assumes that a proof assistant may have a notion of which files have been processed, but that it will only record files that have been completely processed. For more explanation of the handling of multiple files, See Switching between proof scripts.

Command: proof-toggle-active-scripting &optional arg ¶: Toggle active scripting mode in the current buffer.
With arg, turn on scripting iff arg is positive.

2.4 Summary of Proof General buffers

Proof General manages several kinds of buffers in Emacs. Here is a summary of the different kinds of buffers you will use when developing proofs.

The proof shell buffer is an Emacs shell buffer used to run your proof assistant. Usually it is hidden from view (but see Escaping script management). Communication with the proof shell takes place via two or three intermediate buffers.
A script buffer, as we have explained, is a buffer for editing a proof script. The active scripting buffer is the script buffer which is currently being used to send commands to the proof shell.
The goals buffer displays the list of subgoals to be solved for a proof in progress. During a proof it is usually displayed together with the script buffer. The goals buffer has facility for proof-by-pointing.
The response buffer displays other output from the proof assistant, for example error messages or informative messages. The response buffer is displayed whenever Proof General puts a new message in it.
The trace buffer is a special version of the response buffer. It may be used to display unusual debugging output from the prover, for example, tracing proof tactics or rewriting procedures. This buffer is also displayed whenever Proof General puts a new message in it (although it may be quickly replaced with the response or goals buffer in two-buffer mode).

Normally Proof General will automatically reveal and hide the goals and response buffers as necessary during scripting. However there are ways to customize the way the buffers are displayed, for example, to prevent auxiliary buffers being displayed at all (see Display customization).

The menu Proof General -> Buffers provides a convenient way to display or switch to a Proof General buffer: the active scripting buffer; the goal or response buffer; the tracing buffer; or the shell buffer. Another command on this menu, Clear Responses, clears the response and tracing buffer.

2.5 Script editing commands

Proof General provides a few functions for editing proof scripts. The generic functions mainly consist of commands to navigate within the script. Specific proof assistant code may add more to these basics.

Indentation is controlled by the user option proof-script-indent (see User options). When indentation is enabled, Proof General will indent lines of proof script with the usual Emacs functions, particularly TAB, indent-for-tab-command. Unfortunately, indentation in Proof General 4.5 is somewhat slow. Therefore with large proof scripts, we recommend proof-script-indent is turned off.

Here are the commands for moving around in a proof script, with their default key-bindings:

C-c C-a: proof-goto-command-start
C-c C-e: proof-goto-command-end
C-c C-.: proof-goto-end-of-locked

Command: proof-goto-command-start ¶: Move point to start of current (or final) command of the script.

Command: proof-goto-command-end ¶: Set point to end of command at point.

The variable proof-terminal-string is a prover-specific string to terminate proof commands. LEGO and Isabelle used a semicolon, ‘;’. Coq employs a full-stop ‘.’.

Command: proof-goto-end-of-locked &optional switch ¶: Jump to the end of the locked region, maybe switching to script buffer.
If called interactively or switch is non-nil, switch to script buffer. If called interactively, a mark is set at the current location with ‘push-mark’

2.6 Script processing commands

Here are the commands for asserting and retracting portions of the proof script, together with their default key-bindings. Sometimes assertion and retraction commands can only be issued when the queue is empty. You will get an error message Proof Process Busy! if you try to assert or retract when the queue is being processed.⁴

C-c C-n: proof-assert-next-command-interactive
C-c C-u: proof-undo-last-successful-command
C-c C-BS: proof-undo-and-delete-successful-command
C-c C-RET: proof-goto-point
C-c C-b: proof-process-buffer
C-c C-r: proof-retract-buffer
C-c terminator-character: proof-electric-terminator-toggle

The last command, proof-electric-terminator-toggle, is triggered using the character which terminates proof commands for your proof assistant’s script language. LEGO and Isabelle used C-c ;, for Coq, use C-c .. This not really a script processing command. Instead, if enabled, it causes subsequent key presses of ; or . to automatically activate proof-assert-next-command-interactive for convenience.

Rather than use a file command inside the proof assistant to read a proof script, a good reason to use C-c C-b (proof-process-buffer) is that with a faulty proof script (e.g., a script you are adapting to prove a different theorem), Proof General will stop exactly where the proof script fails, showing you the error message and the last processed command. So you can easily continue development from exactly the right place in the script.

In normal development, one often jumps into the middle or to the end of some file, because this is the point, where a lemma must be added or a definition must be fixed. Before starting the real work, one needs to assert the file up to that point, usually with C-c C-RET (proof-goto-point). Even for medium sized files, asserting a big portion can take several seconds. There are different ways to speed this process up.

One can split the development into smaller files. This works quite well with Coq, automatic background compilation, Automatic Compilation in Detail, and the fast compilation options, Quick and inconsistent compilation.
One can configure proof-omit-proofs-option to t to omit complete opaque proofs when larger chunks are asserted. A proof is opaque, if its proof script or proof term cannot influence the following code. In Coq, opaque proofs are finished with Qed, non-opaque ones with Defined. When this omit proofs feature is configured, complete opaque proofs are silently replace with a suitable cheating command (Admitted for Coq) before sending the proof to the proof assistant. 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. For checking the proofs occasionally, a prefix argument for proof-goto-point and proof-process-buffer causes these commands to disregard the setting of proof-omit-proofs-option. Currently, the omit proofs feature is only supported for Coq.
An often used poor man’s solution is to collect all new material at the end of one file, regardless where the material really belongs. When the final theorem has been proved, one cleans up the mess and moves all stuff where it really belongs.

Here is the full set of script processing commands.

Command: proof-assert-next-command-interactive ¶: Process until the end of the next unprocessed command after point.
If inside a comment, just process until the start of the comment.

Command: proof-undo-last-successful-command ¶: Undo last successful command at end of locked region.

Command: proof-undo-and-delete-last-successful-command ¶

Undo and delete last successful command at end of locked region.
Useful if you typed completely the wrong command. Also handy for proof by pointing, in case the last proof-by-pointing command took the proof in a direction you don’t like.

Notice that the deleted command is put into the Emacs kill ring, so you can use the usual ‘yank’ and similar commands to retrieve the deleted text.

Command: proof-goto-point &optional raw ¶: Assert or retract to the command at current position.
Calls ‘proof-assert-until-point’ or ‘proof-retract-until-point’ as appropriate. With prefix argument raw the omit proofs feature (‘proof-omit-proofs-option’) is temporaily disabled to check all proofs in the asserted region.

Command: proof-process-buffer &optional raw ¶: Process the current (or script) buffer, and maybe move point to the end.
With prefix argument raw the omit proofs feature (‘proof-omit-proofs-option’) is temporaily disabled to check all proofs in the asserted region.

Command: proof-retract-buffer &optional called-interactively ¶: Retract the current buffer, and maybe move point to the start.
Point is only moved according to ‘proof-follow-mode’, if called-interactively is non-nil, which is the case for all interactive calls.

Command: proof-electric-terminator-toggle &optional arg ¶: Toggle ‘proof-electric-terminator-enable’. With arg, turn on iff ARG>0.
This function simply uses customize-set-variable to set the variable.

Command: proof-assert-until-point-interactive ¶: Process the region from the end of the locked-region until point.
If inside a comment, just process until the start of the comment.

Command: proof-retract-until-point-interactive &optional delete-region ¶: Tell the proof process to retract until point.
If invoked outside a locked region, undo the last successfully processed command. If called with a prefix argument (delete-region non-nil), also delete the retracted region from the proof-script.

As experienced Emacs users will know, a prefix argument is a numeric argument supplied by some key sequence typed before a command key sequence. You can supply a specific number by typing Meta with the digits, or a “universal” prefix of C-u. See See (emacs)Arguments for more details. Several Proof General commands, like proof-retract-until-point-interactive, may accept a prefix argument to adjust their behaviour somehow.

2.7 Proof assistant commands

There are several commands for interacting with the proof assistant and Proof General, which do not involve the proof script. Here are the key-bindings and functions.

C-c C-l: proof-display-some-buffers
C-c C-p: proof-prf
C-c C-t: proof-ctxt
C-c C-h: proof-help
C-c C-i: proof-query-identifier
C-c C-f: proof-find-theorems
C-c C-w: pg-response-clear-displays
C-c C-c: proof-interrupt-process
C-c C-v: proof-minibuffer-cmd
C-c C-s: proof-shell-start
C-c C-x: proof-shell-exit

Command: proof-display-some-buffers ¶: Display the response, trace, goals, or shell buffer, rotating.
A fixed number of repetitions of this command switches back to the same buffer. Also move point to the end of the response buffer if it’s selected. If in three window or multiple frame mode, display two buffers. The idea of this function is to change the window->buffer mapping without adjusting window layout.

Command: proof-prf ¶: Show the current proof state.
Issues a command to the assistant based on proof-showproof-command.

Command: proof-ctxt ¶: Show the current context.
Issues a command to the assistant based on proof-context-command.

Command: proof-help ¶: Show a help or information message from the proof assistant.
Typically, a list of syntax of commands available. Issues a command to the assistant based on proof-info-command.

Command: proof-query-identifier string ¶: Query the prover about the identifier string.
If called interactively, string defaults to the current word near point.

Command: proof-find-theorems arg ¶: Search for items containing given constants.
Issues a command based on arg to the assistant, using proof-find-theorems-command. The user is prompted for an argument.

Command: pg-response-clear-displays ¶: Clear Proof General response and tracing buffers.
You can use this command to clear the output from these buffers when it becomes overly long. Particularly useful when ‘proof-tidy-response’ is set to nil, so responses are not cleared automatically.

Command: proof-interrupt-process ¶

Interrupt the proof assistant. Warning! This may confuse Proof General.

This sends an interrupt signal to the proof assistant, if Proof General thinks it is busy.

This command is risky because we don’t know whether the last command succeeded or not. The assumption is that it didn’t, which should be true most of the time, and all of the time if the proof assistant has a careful handling of interrupt signals.

Some provers may ignore (and lose) interrupt signals, or fail to indicate that they have been acted upon yet stop in the middle of output. In the first case, PG will terminate the queue of commands at the first available point. In the second case, you may need to press enter inside the prover command buffer (e.g., with Isabelle2009 press RET inside isabelle).

Command: proof-minibuffer-cmd cmd ¶

Send cmd to proof assistant. Interactively, read from minibuffer.
The command isn’t added to the locked region.

If a prefix arg is given and there is a selected region, that is pasted into the command. This is handy for copying terms, etc from the script.

If ‘proof-strict-state-preserving’ is set, and ‘proof-state-preserving-p’ is configured, then the latter is used as a check that the command will be safe to execute, in other words, that it won’t ruin synchronization. If when applied to the command it returns false, then an error message is given.

warning: this command risks spoiling synchronization if the test ‘proof-state-preserving-p’ is not configured, if it is only an approximate test, or if ‘proof-strict-state-preserving’ is off (nil).

As if the last two commands weren’t risky enough, there’s also a command which explicitly adjusts the end of the locked region, to be used in extreme circumstances only. See Escaping script management.

There are a few commands for starting, stopping, and restarting the proof assistant process. The first two have key bindings but restart does not. As with any Emacs command, you can invoke these with M-x followed by the command name.

Command: proof-shell-start ¶

Initialise a shell-like buffer for a proof assistant.
Does nothing if proof assistant is already running.

Also generates goal and response buffers.

If ‘proof-prog-name-ask’ is set, query the user for the process command.

Command: proof-shell-exit &optional dont-ask ¶

Query the user and exit the proof process.

This simply kills the ‘proof-shell-buffer’ relying on the hook function

‘proof-shell-kill-function’ to do the hard work. If optional argument dont-ask is non-nil, the proof process is terminated without confirmation.

The kill function uses ‘<PA>-quit-timeout’ as a timeout to wait after sending ‘proof-shell-quit-cmd’ before rudely killing the process.

This function should not be called if ‘proof-shell-exit-in-progress’ is t, because a recursive call of ‘proof-shell-kill-function’ will give strange errors.

Command: proof-shell-restart ¶

Clear script buffers and send ‘proof-shell-restart-cmd’.
All locked regions are cleared and the active scripting buffer deactivated.

If the proof shell is busy, an interrupt is sent with ‘proof-interrupt-process’ and we wait until the process is ready.

The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant process.

It is up to the proof assistant how much context is cleared: for example, theories already loaded may be "cached" in some way, so that loading them the next time round only performs a re-linking operation, not full re-processing. (One way of caching is via object files, used by Coq).

2.9 Interrupting during trace output

If your prover generates output which is recognized as tracing output in Proof General, you may need to know about a special provision for interrupting the prover process. If the trace output is voluminous, perhaps looping, it may be difficult to interrupt with the ordinary C-c C-c (proof-interrupt-process) or the corresponding button/menu. In this case, you should try Emacs’s quit key, C-g. This will cause a quit in any current editing commands, as usual, but during tracing output it will also send an interrupt signal to the prover. Hopefully this will stop the tracing output, and Emacs should catch up after a short delay.

Here’s an explanation of the reason for this special provision. When large volumes of output from the prover arrive quickly in Emacs, as typically is the case during tracing (especially tracing looping tactics!), Emacs may hog the CPU and spend all its time updating the display with the trace output. This is especially the case when features like output fontification and token display are active. If this happens, ordinary user input in Emacs is not processed, and it becomes difficult to do normal editing. The root of the problem is that Emacs runs in a single thread, and pending process output is dealt with before pending user input. Whether or not you see this problem depends partly on the processing power of your machine (or CPU available to Emacs when the prover is running). One way to test is to start an Emacs shell with M-x shell and type a command such as yes which produces output indefinitely. Now see if you can interrupt the process! (Warning — on slower machines especially, this can cause lockups, so use a fresh Emacs.)

3 Advanced Script Management and Editing

If you are working with large proof developments, you may want to know about the advanced script management and editing features of Proof General covered in this chapter.

Document centred working
Automatic processing
Visibility of completed proofs
Switching between proof scripts
View of processed files
Retracting across files
Asserting across files
Automatic multiple file handling
Escaping script management
Editing features

3.1 Document centred working

Proof scripts can be annotated with the output produced by the prover while they are checked. By hovering the mouse on the completed regions you can see any output that was produced when they were checked. Depending on the proof language (it works well with declarative languages), this may enable a “document centred” way of working, where you may not need to keep a separate window open for displaying prover output.

This way of working is controlled by several settings. To help configure things appropriately for document-centred working, there are two short-cut commands:

Proof-General -> Quick Options -> Display -> Document Centred 
Proof-General -> Quick Options -> Display -> Default

which change settings appropriately between a document centred mode and the original classic Proof General behaviour and appearance. The first command also engages automatic processing of the whole buffer, explained in the following section further below.

The behaviour can be fine-tuned with the individual settings. Starting with the classic settings, first, you may select

Proof-General -> Quick Options -> Processing -> Full Annotations

to ensure that the details are recorded in the script. This is not the default because it can cause long sequences of commands to execute more slowly as the output is collected from the prover eagerly when the commands are executed, and printing can be be slow for large and complex expressions. It also increases the space requirements for Emacs buffers. However, when interactively developing smaller files, it is very useful.

Next, you may deselect

Proof-General -> Quick Options -> Display -> Auto Raise

which will prevent the prover output being eagerly displayed. You can still manually arrange your Emacs windows and frames to ensure the output buffers are present if you want.

3.2 Automatic processing

If you like making your hair stand on end, the electric terminator mode is probably not enough. Proof General has another feature that will automatically send text to the prover, while you aren’t looking.

Enabling

Proof-General -> Quick Options -> Processing -> Process Automatically

Causes Proof General to start processing text when Emacs is idle for a while. You can choose either to send just the next command beyond the point, or the whole buffer. See

Proof-General -> Quick Options -> Processing -> Automatic Processing Mode

for the choices.

The text will be sent in a fast loop that processes more quickly than C-c C-b (i.e., proof-process-buffer, the down toolbar button), but ignores user input and doesn’t update the display. But the feature tries to be non-intrusive to the user: if you start to type something or use the mouse, the fast loop will be interrupted and revert to a slower interactive loop with display updates.

In the check next command mode, the successfully checked region will briefly flash up as green to indicate it is okay.

You can use C-c C-. (proof-goto-end-of-locked) to find out where processing got to, as usual. Text is only sent if the last interactive command processed some text (i.e., wasn’t an undo step backwards into the buffer) and processing didn’t stop with an error. To start automatic processing again after an error, simply hit C-c C-n after editing the buffer. To turn the automatic processing on or off from the keyboard, you can use the key binding:

C-c >: proof-autosend-toggle

Command: proof-autosend-toggle &optional arg ¶: Toggle ‘proof-autosend-enable’. With arg, turn on iff ARG>0.
This function simply uses customize-set-variable to set the variable.

3.3 Visibility of completed proofs

Large developments may consist of large files with many proofs. To help see what has been proved without the detail of the proof itself, Proof General can hide portions of the proof script. Two different kinds of thing can be hidden: comments and (what Proof General designates as) the body of proofs.

You can toggle the visibility of a proof script portion by using the context sensitive menu triggered by clicking the right mouse button on a completed proof, or the key C-c v, which runs pg-toggle-visibility.

You can also select the “disappearing proofs” mode from the menu,

  Proof-General -> Quick Options -> Display -> Disappearing Proofs

This automatically hides each the body of each proof portion as it is completed by the proof assistant. Two further menu commands in the main Proof-General menu, Show all and Hide all apply to all the completed portions in the buffer.

Notice that by design, this feature only applies to completed proofs, after they have been processed by the proof assistant. When files are first visited in Proof General, no information is stored about proof boundaries.

The relevant elisp functions and settings are mentioned below.

Command: pg-toggle-visibility ¶: Toggle visibility of region under point.

Command: pg-show-all-proofs ¶: Display all completed proofs in the buffer.

Command: pg-hide-all-proofs ¶: Hide all completed proofs in the buffer.

User Option: proof-disappearing-proofs ¶

Non-nil causes Proof General to hide proofs as they are completed.

The default value is nil.

3.4 Switching between proof scripts

Basic modularity in large proof developments can be achieved by splitting proof scripts across various files. Let’s assume that you are in the middle of a proof development. You are working on a soundness proof of Hoare Logic in a file called⁵ HSound.v. It depends on a number of other files which develop underlying concepts e.g. syntax and semantics of expressions, assertions, imperative programs. You notice that the current lemma is too difficult to prove because you have forgotten to prove some more basic properties about determinism of the programming language. Or perhaps a previous definition is too cumbersome or even wrong.

At this stage, you would like to visit the appropriate file, say sos.v and retract to where changes are required. Then, using script management, you want to develop some more basic theory in sos.v. Once this task has been completed (possibly involving retraction across even earlier files) and the new development has been asserted, you want to switch back to HSound.v and replay to the point you got stuck previously.

Some hours (or days) later you have completed the soundness proof and are ready to tackle new challenges. Perhaps, you want to prove a property that builds on soundness or you want to prove an orthogonal property such as completeness.

Proof General lets you do all of this while maintaining the consistency between proof script buffers and the state of the proof assistant. However, you cannot have more than one buffer where only a fraction of the proof script contains a locked region. Before you can employ script management in another proof script buffer, you must either fully assert or retract the current script buffer.

3.5 View of processed files

Proof General tries to be aware of all files that the proof assistant has processed or is currently processing. In the best case, it relies on the proof assistant explicitly telling it whenever it processes a new file which corresponds⁶ to a file containing a proof script.

If the current proof script buffer depends on background material from other files, proof assistants typically process these files automatically. If you visit such a file, the whole file is locked as having been processed in a single step. From the user’s point of view, you can only retract but not assert in this buffer. Furthermore, retraction is only possible to the beginning of the buffer.

Unlike a script buffer that has been processed step-by-step via Proof General, automatically loaded script buffers do not pass through a “red” phase to indicate that they are currently being processed. This is a limitation of the present implementation. Proof General locks a buffer as soon as it sees the appropriate message from the proof assistant. Different proof assistants may use different messages: either early locking when processing a file begins (e.g. LEGO) or late locking when processing a file ends (e.g. Isabelle).

With early locking, you may find that a script which has only been partly processed (due to an error or interrupt, for example), is wrongly completely locked by Proof General. Visit the file and retract back to the start to fix this.

With late locking, there is the chance that you can break synchronization by editing a file as it is being read by the proof assistant, and saving it before processing finishes.

In fact, there is a general problem of editing files which may be processed by the proof assistant automatically. Synchronization can be broken whenever you have unsaved changes in a proof script buffer and the proof assistant processes the corresponding file. (Of course, this problem is familiar from program development using separate editors and compilers). The good news is that Proof General can detect the problem and flashes up a warning in the response buffer. You can then visit the modified buffer, save it and retract to the beginning. Then you are back on track.

3.6 Retracting across files

Make sure that the current script buffer has either been completely asserted or retracted (Proof General enforces this). Then you can retract proof scripts in a different file. Simply visit a file that has been processed earlier and retract in it, using the retraction commands from see Script processing commands. Apart from removing parts of the locked region in this buffer, all files which depend on it will be retracted (and thus unlocked) automatically. Proof General reminds you that now is a good time to save any unmodified buffers.

3.7 Asserting across files

Make sure that the current script buffer has either been completely asserted or retracted. Then you can assert proof scripts in a different file. Simply visit a file that contains no locked region and assert some command with the usual assertion commands, see Script processing commands. Proof General reminds you that now is a good time to save any unmodified buffers. This is particularly useful as assertion may cause the proof assistant to automatically process other files.

3.8 Automatic multiple file handling

To make it easier to adapt Proof General for a proof assistant, there is another possibility for multiple file support — that it is provided automatically by Proof General and not integrated with the file-management system of the proof assistant.

In this case, Proof General assumes that the only files processed are the ones it has sent to the proof assistant itself. Moreover, it (conservatively) assumes that there is a linear dependency between files in the order they were processed.

If you only have automatic multiple file handling, you’ll find that any files loaded directly by the proof assistant are not locked when you visit them in Proof General. Moreover, if you retract a file it may retract more than is strictly necessary (because it assumes a linear dependency).

For further technical details of the ways multiple file scripting is configured, see Handling multiple files in the Adapting Proof General manual.

3.9 Escaping script management

Occasionally you may want to review the dialogue of the entire session with the proof assistant, or check that it hasn’t done something unexpected. Experienced users may also want to directly communicate with the proof assistant rather than sending commands via the minibuffer, see Proof assistant commands.

Although the proof shell is usually hidden from view, it is run in a buffer which you can use to interact with the prover if necessary. You can switch to it using the menu:

  Proof-General -> Buffers -> Shell

Warning: you can probably cause confusion by typing in the shell buffer! Proof General may lose track of the state of the proof assistant. Output from the assistant is only fully monitored when Proof General is in control of the shell. When in control, Proof General watches the output from the proof assistant to guess when a file is loaded or when a proof step is taken or undone. What happens when you type in the shell buffer directly depends on how complete the communication is between Proof General and the prover (which depends on the particular instantiation of Proof General).

If synchronization is lost, you have two options to resynchronize. If you are lucky, it might suffice to use the key:

C-c C-z: proof-frob-locked-end

This command is disabled by default, to protect novices using it accidently.

If proof-frob-locked-end does not work, you will need to restart script management altogether (see Proof assistant commands).

Command: proof-frob-locked-end ¶

Move the end of the locked region backwards to regain synchronization.
Only for use by consenting adults.

This command can be used to repair synchronization in case something goes wrong and you want to tell Proof General that the proof assistant has processed less of your script than Proof General thinks.

You should only use it to move the locked region to the end of a proof command.

3.10 Editing features

To make editing proof scripts more productive, Proof General provides some additional editing commands.

One facility is the input ring of previously processed commands. This allows a convenient way of repeating an earlier command or a small edit of it. The feature is reminiscent of history mechanisms provided in shell terminals (and the implementation is borrowed from the Emacs Comint package). The input ring only contains commands which have been successfully processed (coloured blue). Duplicated commands are only entered once. The size of the ring is set by the variable pg-input-ring-size.

M-p: pg-previous-matching-input-from-input
M-n: pg-next-matching-input-from-input

Command: pg-previous-input arg ¶: Cycle backwards through input history, saving input.
If called interactively, arg is given by the prefix argument.

Command: pg-next-input arg ¶: Cycle forwards through input history.
If called interactively, arg is given by the prefix argument.

Command: pg-previous-matching-input regexp n ¶: Search backwards through input history for match for regexp.
(Previous history elements are earlier commands.) With prefix argument n, search for Nth previous match. If n is negative, find the next or Nth next match.

Command: pg-next-matching-input regexp n ¶: Search forwards through input history for match for regexp.
(Later history elements are more recent commands.) With prefix argument n, search for Nth following match. If n is negative, find the previous or Nth previous match.

Command: pg-previous-matching-input-from-input n ¶: Search backwards through input history for match for current input.
(Previous history elements are earlier commands.) With prefix argument n, search for Nth previous match. If n is negative, search forwards for the -Nth following match.

Command: pg-next-matching-input-from-input n ¶: Search forwards through input history for match for current input.
(Following history elements are more recent commands.) With prefix argument n, search for Nth following match. If n is negative, search backwards for the -Nth previous match.

4 Unicode symbols and special layout support

Proof General inherits support for displaying Unicode (and any other) fonts from the underlying Emacs program. If you are lucky, your system will be able to use or synthesise a font that provides a rich set of mathematical symbols. To store symbols directly in files you need to use a particular coding, for example UTF-8. Newer Emacs versions can handle a multitude of different coding systems and will try to automatically detect an appropriate one; consult the Emacs documentation for more details. Of course, the prover that you are using will need to understand the same encodings and symbol meanings.

Alternatively, you can use the Unicode Tokens mode provided in Proof General to display mathematical symbols in place of sequences of other characters (usually plain ASCII). This can provide better compatibility, portability, and flexibility. Even if you use real Unicode characters as prover input, the Unicode Tokens mode can provide some helpful facilities for input shorthands and giving special layout.

Maths menu
Unicode Tokens mode
Configuring tokens symbols and shortcuts
Special layout
Moving between Unicode and tokens
Finding available tokens shortcuts and symbols
Selecting suitable fonts

4.1 Maths menu

The Maths Menu minor mode (adapted from a menu by Dave Love) simply adds a menu Maths to the main menubar for inserting common mathematical symbols. You can enable or disable it via the menu

  Proof-General -> Quick Options -> Minor Modes -> Unicode Maths Menu

(proof-maths-menu-toggle). Whether or not the symbols display well the menus depends on the font used to display the menus (which depends on the Emacs version, toolkit and platform). Ordinarily, the symbols inserted into the text will be Unicode characters which will be saved in the file using the encoding selected by standard Emacs mechanisms.

4.2 Unicode Tokens mode

The Unicode Tokens minor mode has been written specially for Proof General (with thanks to Stefan Monnier for providing inspiration and a starting point). It supports the display of symbols when the underlying text of the file and buffer actually contains something else, typically, plain ASCII text. It provides backward compatibility with the older X-Symbol mode.

Unicode Tokens can be enabled or disabled using the menu:

  Proof-General -> Quick Options -> Display -> Unicode Tokens

The mode to allows ASCII tokens (i.e., sequences of plain ASCII characters) to be displayed as Unicode character compositions, perhaps with additional text properties. The additional text properties allow the use of tokens to cause font changes (bold, italic), text size changes, and sub-script/super-script.

For example, the ASCII sequences /\ or \<And> could be displayed as a conjunction symbol. The sequence x __ y might be written to display y as subscript. This allows a file to be stored in perfectly portable plain ASCII encoding, but be displayed and edited with real symbols and appealing layout. Of course, the proof assistant needs to understand the underlying tokens in each case.

Technically, the mechanism is based on Emacs Font Lock facility, using the composition text property to display ASCII character sequence tokens as something else. This means that the underlying buffer text is not altered. This is a major advantage over the older X-Symbol (and the experimental version of Unicode Tokens in PG 3.7.1), which had the annoying risk of saving your buffer text in a corrupted format. This can never happen with the new mode.

When the Unicode Tokens mode is enabled, Maths Menu is automatically modified to insert tokenised versions of the Unicode characters (whenever a reverse mapping can be found). This means that you can still use the Maths Menu to conveniently input symbols. You can easily add custom key bindings for particular symbols you need to enter often (see Adding your own keybindings for examples).

The Unicode Tokens mode also allows short-cut sequences of ordinary characters to quickly type tokens (similarly to the facility provided by X-Symbol). These, along with the token settings themselves, are configured on a per-prover basis.

4.3 Configuring tokens symbols and shortcuts

To edit the strings used to display tokens, or the collection of short-cuts, you can edit the file PA-unicode-tokens.el, or customize the main variables it contains, for example PA-token-name-alist and PA-shortcut-alist.

E.g., for Isabelle

  M-x customize-variable isar-token-name-alist RET

provides an interface to the tokens, and

  M-x customize-variable isar-shortcut-alist

an interface to the shortcuts.

Where possible, it is better to use the more fine grained way is available to do this, which edits the separate tables which are combine to form the big list of tokens. This is available via the menus, e.g., in Isabelle, use

  Tokens -> Customize -> Extended Symbols

to customize the symbols used for the “extended” (non standard) symbol list.

4.4 Special layout

The Unicode Tokens mode supports both symbol tokens used to display character sequences in different ways and control tokens used to control the layout of the text in various ways, such as superscript, subscript, large, small, bold, italic, etc. (The size and position layout is managed using Emacs’s display text property)

As well as displaying token sequences as special symbols, symbol tokens themselves can define layout options as well; for example you might define a token \<hugeOplus> to display a large circled-plus glyph. If you try the customization mentioned in the section above you will see the options available when defining symbols.

These options are fixed layout schemes which also make layout tokens easy to configure for provers. The layout possibilities include the ones shown in the table below. There are two ways of configuring control tokens for layout: character controls and region controls. The character controls apply to the next “character”, although this is a prover-specific notion and might actually mean the next word or identifier. An example might be writing BOLDCHAR x to make a bold x. Similarly the region controls apply to a delineated region of text, for example, writing BEGINBOLD this is bold ENDBOLD could cause the enclosed text this is bold to be displayed in a bold font.

The control tokens that have been configured populate the Tokens menu, so, for example, you may be able to select a region of text and then use the menu item:

  Tokens -> Format Region -> Bold

to cause the bold region tokens to be inserted around the selected text, which should cause the buffer presentation to show the text in a bold format (hiding the tokens).

Here is the table of layout controls available. What you actually can use will depend on the configuration for the underlying prover.

sub: lower the text (subscript)
sup: raise the text (superscript)
bold: make the text be in the bold weight of the current font
italic: make the text be in the italic variant of the current font
big: make the text be in a bigger size of the current font
small: make the text be in a smaller size of the current font
underline: underline the text
overline: overline the text
script: display the text in a “script” font
frakt: display the text in a “fraktur” font
serif: display the text in a serif font
sans: display the text in a sans serif font
keyword: display the text in the keyword face (font-lock-keyword-face)
function: display the text in the function name face (font-lock-function-name-face)
type: display the text in the type name face (font-lock-type-face)
preprocessor: display the text in the preprocessor face (font-lock-preprocessor-face)
doc: display the text in the documentation face (font-lock-doc-face)
builtin: display the text in the builtin face (font-lock-builtin-face)

Notice that the fonts can be set conveniently by the menu commands

        Tokens -> Set Fonts -> Script

etc. See Selecting suitable fonts, for more.

The symbols used to select the various font-lock faces (see M-x list-faces-display to show them) allow you to define custom colouring of text for proof assistant input and output, exploiting rich underlying syntax mechanisms of the prover.

Face: unicode-tokens-serif-font-face ¶: Serif (roman) font face.

Face: unicode-tokens-sans-font-face ¶: Sans serif font face.

Face: unicode-tokens-fraktur-font-face ¶: Fraktur font face.

Face: unicode-tokens-script-font-face ¶: Script font face.

4.5 Moving between Unicode and tokens

If you want to share text between applications (e.g., email some text from an Isabelle theory file which heavily uses symbols), it is useful to convert to and from Unicode with cut-and-paste operations. The default buffer cut and paste functions will copy the underlying text, which contains the tokens (ASCII format). To copy and convert or paste then convert back, use these commands:

  Tokens -> Copy as unicode
  Tokens -> Paste from unicode

Both of these are necessarily approximate. The buffer presentation may use additional controls (for super/subscript layout or bold fonts, etc), which cannot be converted. Pasting relies on being able to identify a unique token mapped from a single Unicode character; the token table may not include such an entry, or may be ambiguous.

Command: unicode-tokens-copy beg end ¶: Copy presentation of region between beg and end.
This is an approximation; it makes assumptions about the behaviour of symbol compositions, and will lose layout information.

Command: unicode-tokens-paste ¶: Paste text from clipboard, converting Unicode to tokens where possible.

If you are using a mixture of “real” Unicode and tokens like this you may want to be careful to check the buffer contents: the command unicode-tokens-highlight-unicode helps you to manage this. It is available on the Tokens menu as

  Tokens -> Highlight Real Unicode Chars

Alternative ways to check are to toggle the display of tokens using

  Tokens -> Reveal Symbol Tokens

(the similar entry for Control Tokens displays tokens being used to control layout). Or simply toggle the tokens mode, which will leave the true Unicode tokens untouched.

Variable: unicode-tokens-highlight-unicode ¶: Non-nil to highlight Unicode characters.

4.6 Finding available tokens shortcuts and symbols

Two commands (both on the Tokens menu) allow you to see the tokens and shortcuts available:

        Tokens -> List Tokens
        Tokens -> List Shortcuts

Additionally, you can view the complete Unicode character set available in the default Emacs font, with

        Tokens -> List Unicode Characters

(this uses a list adapted from Norman Walsh’s unichars.el).

Note that the Unicode Tokens modes displays symbols defined by symbol tokens in a special font.

Command: unicode-tokens-list-tokens ¶: Show a buffer of all tokens.

Command: unicode-tokens-list-shortcuts ¶: Show a buffer of all the shortcuts available.

Command: unicode-tokens-list-unicode-chars ¶: Insert each Unicode character into a buffer.
Lets you see which characters are available for literal display in your Emacs font.

4.7 Selecting suitable fonts

The precise set of symbol glyphs that are available to you will depend in complicated ways on your operating system, Emacs version, configuration options used when Emacs was compiled, installed font sets, and (even) command line options used to start Emacs. So it is hard to give comprehensive and accurate advice in this manual. In general, things work much better with Emacs 23 than earlier versions.

To improve flexibility, Unicode Tokens mode allows you to select another font to display symbols from the default font that is used to display text in the buffer. This is the font that is configured by the menu

        Tokens -> Set Fonts -> Symbol

its customization name is unicode-tokens-symbol-font-face, but notice that only the font family aspect of the face is used. Similarly, other fonts can be configured for controling different font families (script, fraktur, etc).

For symbols, good results are possible by using a proportional font for displaying symbols that has many symbol glyphs, for example the main font StixGeneral font from the Stix Fonts project (http://www.stixfonts.org/). At the time of writing you can obtain a beta version of these fonts in TTF format from http://olegueret.googlepages.com/stixfonts-ttf. On recent Linux distributions and with an Emacs 23 build that uses Xft, simply copy these ttf files into the .fonts directory inside your home directory to make them available.

Another font I like is DejaVu Sans Mono. It covers all of the standard Isabelle symbols. Some of the symbols are currently not perfect; however this font is an open source effort so users can contribute or suggest improvements. See http://dejavu-fonts.org.

If you are stuck with Emacs 22, you need to use the fontset mechanism which configures sets of fonts to use for display. The default font sets may not include enough symbols (typical symptom: symbols display as empty boxes). To address this, the menu command

        Tokens -> Set Fonts -> Make Fontsets

constructs a number of fontsets at particular point sizes, based on several widely available fonts. See pg-fontsets.el for the code. After running this command, you can select from additional fontsets from the menus for changing fonts.

For further suggestions, please search (and contribute!) to the Proof General wiki at http://proofgeneral.inf.ed.ac.uk/wiki.

Face: unicode-tokens-symbol-font-face ¶: The default font used for symbols. Only :family and :slant attributes are used.

Variable: unicode-tokens-font-family-alternatives ¶: Not documented.

5 Support for other Packages

Proof General makes some configuration for other Emacs packages which provide various useful facilities that can make your editing more effective.

Sometimes this configuration is purely at the proof assistant specific level (and so not necessarily available), and sometimes it is made using Proof General settings.

When adding support for a new proof assistant, we suggest that these other packages are supported, as a convention.

The packages currently supported include font-lock, imenu and speedbar, outline-mode, completion, and etags.

Syntax highlighting
Imenu and Speedbar
Support for outline mode
Support for completion
Support for tags

5.1 Syntax highlighting

Proof script buffers are decorated (or fontified) with colours, bold and italic fonts, etc, according to the syntax of the proof language and the settings for font-lock-keywords made by the proof assistant specific portion of Proof General. Moreover, Proof General usually decorates the output from the proof assistant, also using font-lock.

To automatically switch on fontification in Emacs, you may need to engage M-x global-font-lock-mode.

By the way, the choice of colour, font, etc, for each kind of markup is fully customizable in Proof General. Each face (Emacs terminology) is controlled by its own customization setting. You can display a list of all of them using the customize menu:

Proof General -> Advanced -> Customize -> Faces -> Proof Faces.

5.2 Imenu and Speedbar

The Emacs package imenu (Index Menu) provides a menu built from the names of entities (e.g., theorems, definitions, etc) declared in a buffer. This allows easy navigation within the file. Proof General configures both packages automatically so that you can quickly jump to particular proofs in a script buffer.

(Developers note: the automatic configuration is done with the settings proof-goal-with-hole-regexp and proof-save-with-hole-regexp. Better configuration may be made manually with several other settings, see the Adapting Proof General manual for further details).

To use Imenu, select the option

        Proof-General -> Quick Options -> Minor Modes -> Index Menu

This adds an "Index" menu to the main menu bar for proof script buffers. You can also use M-x imenu for keyboard-driven completion of tags built from names in the buffer.

Speedbar displays a file tree in a separate window on the display, allowing quick navigation. Middle/double-clicking or pressing + on a file icon opens up to display tags (definitions, theorems, etc) within the file. Middle/double-clicking on a file or tag jumps to that file or tag.

To use Speedbar, use

        Proof-General -> Quick Options -> Minor Modes -> Speedbar

If you prefer the old fashioned way, ‘M-x speedbar’ does the same job.

For more information about Speedbar, see http://cedet.sourceforge.net/speedbar.shtml.

5.3 Support for outline mode

Proof General configures Emacs variables (outline-regexp and outline-heading-end-regexp) so that outline minor mode can be used on proof script files. The headings taken for outlining are the "goal" statements at the start of goal-save sequences, see Goal-save sequences. If you want to use outline to hide parts of the proof script in the locked region, you need to disable proof-strict-read-only.

Use M-x outline-minor-mode to turn on outline minor mode. Functions for navigating, hiding, and revealing the proof script are available in menus.

Please note that outline-mode may not work well in processed proof script files, because of read-only restrictions of the protected region. This is an inherent problem with outline because it works by modifying the buffer. If you want to use outline with processed scripts, you can turn off the Strict Read Only option.

See See (emacs)Outline Mode for more information about outline mode.

5.4 Support for completion

You might find the completion facility of Emacs useful when you’re using Proof General. The key C-RET is defined to invoke the complete command. Pressing C-RET cycles through completions displaying hints in the minibuffer.

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.

Proof General has the additional facility for setting a completion table for each supported proof assistant, which gets loaded into the completion database automatically. Ideally the completion table would be set from the running process according to the identifiers available are within the particular context of a script file. But until this is available, this table may be set to contain a number of standard identifiers available for your proof assistant.

The setting PA-completion-table holds the list of identifiers for a proof assistant. The function proof-add-completions adds these into the completion database.

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

The completion facility uses a library completion.el which usually ships with Emacs, and supplies the complete function.

Command: complete ¶

Fill out a completion of the word before point.
Point is left at end. Consecutive calls rotate through all possibilities. Prefix args:

C-u: leave point at the beginning of the completion, not the end.
a number: rotate through the possible completions by that amount
0: same as -1 (insert previous completion)

See the comments at the top of ‘completion.el’ for more info.

5.5 Support for tags

An Emacs "tags table" is a description of how a multi-file system is broken up into files. It lists the names of the component files and the names and positions of the functions (or other named subunits) in each file. Grouping the related files makes it possible to search or replace through all the files with one command. Recording the function names and positions makes possible the M-. command which finds the definition of a function by looking up which of the files it is in.

Some instantiations of Proof General (currently Coq) are supplied with external programs (coqtags) for making tags tables. For example, invoking ‘coqtags *.v’ produces a file TAGS for all files ‘*.v’ in the current directory. Invoking ‘coqtags `find . -name \*.v`’ produces a file TAGS for all files ending in ‘.v’ in the current directory structure. Once a tag table has been made for your proof developments, you can use the Emacs tags mechanisms to find tags, and complete symbols from tags table.

One useful key-binding you might want to make is to set the usual tags completion key M-tab to run tag-complete-symbol to use completion from names in the tag table. To set this binding in Proof General script buffers, put this code in your .emacs file:

(add-hook 'proof-mode-hook
  (lambda () (local-set-key '(meta tab) 'tag-complete-symbol)))

Since this key-binding interferes with a default binding that users may already have customized (or may be taken by the window manager), Proof General doesn’t do this automatically.

Apart from completion, there are several other operations on tags. One common one is replacing identifiers across all files using tags-query-replace. For more information on how to use tags, See (emacs)Tags.

To use tags for completion at the same time as the completion mechanism mentioned already, you can use the command M-x add-completions-from-tags-table.

Command: add-completions-from-tags-table ¶: Add completions from the current tags table.

6 Subterm Activation and Proof by Pointing

This chapter describes what you can do from inside the goals buffer, providing support for these features exists for your proof assistant.

As of Proof General 4.4, this support has existed only for LEGO and proof-by-pointing functionality has been temporarily removed from the interface. If you would like to see subterm activation support for Proof General in another proof assistant, please petition the developers of that proof assistant to provide it!

Goals buffer commands

6.1 Goals buffer commands

When you are developing a proof, the input focus (Emacs cursor) is usually on the script buffer. Therefore Proof General binds some mouse buttons for commands in the goals buffer, to avoid the need to move the cursor between buffers.

The mouse bindings are these:

mouse-1: pg-goals-button-action
C-mouse-3: proof-undo-and-delete-last-successful-command
C-S-mouse-1: pg-identifier-under-mouse-query

Where mouse-1 indicates the left mouse button, and mouse-3 indicates the right hand mouse button. The functions available provide a way to construct commands automatically (pg-goals-button-action) and to inspect identifiers (pg-identifier-under-mouse-query) as the Info toolbar button does.

Proof-by-pointing is a cute idea. It lets you automatically construct parts of a proof by clicking. You can ask the proof assistant to try to do a step in the proof, based on where you click. If you don’t like the command which was inserted into the script, you can comment use the control key with the right button to undo the step and delete it from your script (proof-undo-and-delete-last-successful-command).

Proof-by-pointing may construct several commands in one go. These are sent back to the proof assistant altogether and appear as a single step in the proof script. However, if the proof is later replayed (without using PBP), the proof-by-pointing constructions will be considered as separate proof commands, as usual.

The main function for proof-by-pointing is pg-goals-button-action.

Command: pg-goals-button-action event ¶

Construct a proof-by-pointing command based on the mouse-click event.
This function should be bound to a mouse button in the Proof General goals buffer.

The event is used to find the smallest subterm around a point. A position code for the subterm is sent to the proof assistant, to ask it to construct an appropriate proof command. The command which is constructed will be inserted at the end of the locked region in the proof script buffer, and immediately sent back to the proof assistant. If it succeeds, the locked region will be extended to cover the proof-by-pointing command, just as for any proof command the user types by hand.

Proof-by-pointing uses markup describing the term structure of the concrete syntax output by the proof assistant. This markup is useful in itself: it allows you to explore the structure of a term using the mouse (the smallest subexpression that the mouse is over is highlighted), and easily copy subterms from the output to a proof script.

Command: pg-identifier-under-mouse-query event ¶: Query the prover about the identifier near mouse click event.

7 Graphical Proof-Tree Visualization

Since version 4.2, Proof General supports proof-tree visualization on graphical desktops via the additional program Prooftree. Currently, proof-tree visualization is only supported for the Coq proof assistant.

This version of Proof General requires Prooftree version 0.11. Check the Prooftree website, to see if some later versions are also compatible. (Because of the communication protocol, Proof General is always only compatible with certain versions of Prooftree.)

For installation instructions and more detailed information about Prooftree, please refer to the Prooftree website and the Prooftree man page. For information about how to support proof-tree visualization for a different proof assistant, see Section Configuring Proof-Tree Visualization in the Adapting Proof General manual.

Starting and Stopping Proof-Tree Visualization
Features of Prooftree
Prooftree Customization

7.1 Starting and Stopping Proof-Tree Visualization

When proof-tree visualization is supported (currently only for the Coq proof assistant), you can start the visualization via the proof-tree button in the tool-bar, via the menu

   Proof-General -> Start/Stop Prooftree

or via the keyboard shortcut C-c C-d, all of which invoke proof-tree-external-display-toggle.

If you are inside a proof, the graphical display is started immediately for your current proof. Otherwise the display starts as soon as you start the next proof. Starting the proof-tree display in the middle of a proof involves an automatic reexecution of your current proof script in the locked region, which should be almost unnoticeable, except for the time it takes.

The proof-tree display stops at the end of the proof or when you invoke proof-tree-external-display-toggle by one of the three indicated means again. Alternatively you can also close the proof-tree window.

Proof General launches only one instance of Prooftree, which can manage an arbitrary amount of proof-tree windows.

7.2 Features of Prooftree

The proof-tree window provides visual information about the status of the different branches in your proof (by coloring completely proved branches in green, for example) and means for inspecting previous proof states without the need to retract parts of your proof script. Currently, Prooftree provides the following features:

Navigation in the proof tree and display of all previous proof states and proof commands.
Display branches of the proof in different colors according to their proof state, distinguishing branches with open, partially or fully instantiated existential variables as well as branches that have been finished by a cheating command such as admit.
Display the status of existential variables and their dependencies.
Mark proof commands that introduce or instantiate a given existential variable.
Snapshots of proof trees for reference when you retract your proof to try a different approach.
Trigger a retract (undo) operation with a selected sequent as target.
Insert proof scripts from the proof tree in the current buffer.

For a more elaborated description please consult the help dialog of Prooftree or the Prooftree man page.

7.3 Prooftree Customization

The location of the Prooftree program and command line arguments can be configured in the customization group proof-tree. You can visit this customization group inside a running instance of Proof General by typing M-x customize-group <RET> proof-tree <RET>.

The graphical aspects of the proof-tree rendering, fonts and colors can be changed inside Prooftree by invoking the Configuration item of the main menu.

Prover specific parts such as the regular expressions for recognizing subgoals, existential variables and navigation and cheating commands are in the customization group proof-tree-internals. Under normal circumstances there should be no need to change one of these internal settings.

8 Customizing Proof General

There are two ways of customizing Proof General: it can be customized for a user’s preferences using a particular proof assistant, or it can be customized by a developer to add support for a new proof assistant. The latter kind of customization we call instantiation, or adapting. See the Adapting Proof General manual for how to do this. Here we cover the user-level customization for Proof General.

There are two kinds of user-level settings in Proof General:

Settings that apply globally to all proof assistants.
those that can be adjusted for each proof assistant individually.

The first sort have names beginning with proof-. The second sort have names which begin with a symbol corresponding to the proof assistant: for example, isa-, coq-, etc. The symbol is the root of the mode name. See Quick start guide, for a table of the supported modes. To stand for an arbitrary proof assistant, we write PA- for these names.

In this chapter we only consider the generic settings: ones which apply to all proof assistants (globally or individually). The support for a particular proof assistant may provide extra individual customization settings not available in other proof assistants. See the chapters covering each assistant for details of those settings.

Basic options
How to customize
Display customization
User options
Changing faces
Tweaking configuration settings

8.1 Basic options

Proof General has some common options which you can toggle directly from the menu:

   Proof-General -> Quick Options

The effect of changing one of these options will be seen immediately (or in the next proof step). The window-control options on this menu are described shortly. See Display customization.

To save the current settings for these options (only), use the Save Options command in the submenu:

   Proof-General -> Quick Options -> Save Options

or M-x customize-save-customized.

The options on this sub-menu are also available in the complete user customization options group for Proof General. For this you need to know a little bit about how to customize in Emacs.

8.2 How to customize

Proof General uses the Emacs customization library to provide a friendly interface. You can access all the customization settings for Proof General via the menu:

   Proof-General -> Advanced -> Customize

Using the customize facility is straightforward. You can select the setting to customize via the menus, or with M-x customize-variable. When you have selected a setting, you are shown a buffer with its current value, and facility to edit it. Once you have edited it, you can use the special buttons set, save and done. You must use one of set or save to get any effect. The save button stores the setting in your .emacs file. The command M-x customize-save-customized or Emacs menubar item Options -> Save Options saves all settings you have edited.

A technical note. In the customize menus, the variable names mentioned later in this chapter may be abbreviated — the "proof-" or similar prefixes are omitted. Also, some of the option settings may have more descriptive names (for example, on and off) than the low-level lisp values (non-nil, nil) which are mentioned in this chapter. These features make customize rather more friendly than raw lisp.

You can also access the customize settings for Proof General from other (non-script) buffers. Use the menu:

   Options -> Customize Emacs -> Top-level Customization Group

and select the External and then Proof-General groups.

The complete set of customization settings will only be available after Proof General has been fully loaded. Proof General is fully loaded when you visit a script file for the first time, or if you type M-x load-library RET proof RET.

For more help with customize, see See (emacs)Customization.

8.3 Display customization

By default, Proof General displays two buffers during scripting, in a split window on the display. One buffer is the script buffer. The other buffer is either the goals buffer (*goals*) or the response buffer (*response*). Proof General raises and switches between these last two automatically.

Proof General allows several ways to customize this default display model, by splitting the Emacs frames in different ways and maximising the amount of information shown, or by using multiple frames. The customization options are explained below; they are also available on the menu:

  Proof-General -> Quick Options -> Display

and you can save your preferred default.

If your screen is large enough, you may prefer to display all three of the interaction buffers at once. This is useful, for example, to see output from the proof-find-theorems command at the same time as the subgoal list. Set the user option proof-three-window-enable to make Proof General keep both the goals and response buffer displayed.

If you prefer to switch windows and buffers manually when you want to see the prover output, you can customize the user option proof-auto-raise-buffers to prevent the automatic behaviour. You can browse interaction output by hovering the mouse over the command regions in the proof script.

User Option: proof-auto-raise-buffers ¶

If non-nil, automatically raise buffers to display latest output.
If this is not set, buffers and windows will not be managed by Proof General.

The default value is t.

User Option: proof-three-window-enable ¶

Whether response and goals buffers have dedicated windows.
If non-nil, Emacs windows displaying messages from the prover will not be switchable to display other windows.

This option can help manage your display.

Setting this option triggers a three-buffer mode of interaction where the goals buffer and response buffer are both displayed, rather than the two-buffer mode where they are switched between. It also prevents Emacs automatically resizing windows between proof steps.

If you use several frames (the same Emacs in several windows on the screen), you can force a frame to stick to showing the goals or response buffer.

The default value is t.

Sometimes during script management, there is no response from the proof assistant to some command. In this case you might like the empty response window to be hidden so you have more room to see the proof script. The setting proof-delete-empty-windows helps you do this.

User Option: proof-delete-empty-windows ¶

If non-nil, automatically remove windows when they are cleaned.
For example, at the end of a proof the goals buffer window will be cleared; if this flag is set it will automatically be removed. If you want to fix the sizes of your windows you may want to set this variable to 'nil' to avoid windows being deleted automatically. If you use multiple frames, only the windows in the currently selected frame will be automatically deleted.

The default value is nil.

This option only has an effect when you have set proof-three-window-mode.

If you are working on a machine with a window system, you can use Emacs to manage several frames on the display, to keep the goals buffer displayed in a fixed place on your screen and in a certain font, for example. A convenient way to do this is via the user option

User Option: proof-multiple-frames-enable ¶

Whether response and goals buffers have separate frames.
If non-nil, Emacs will make separate frames (screen windows) for the goals and response buffers, by altering the Emacs variable ‘special-display-regexps’.

The default value is nil.

Multiple frames work best when proof-delete-empty-windows is off and proof-three-window-mode is on.

Finally, there are two commands available which help to switch between buffers or refresh the window layout. These are on the menu:

  Proof-General -> Buffers

Command: proof-display-some-buffers ¶: Display the response, trace, goals, or shell buffer, rotating.
A fixed number of repetitions of this command switches back to the same buffer. Also move point to the end of the response buffer if it’s selected. If in three window or multiple frame mode, display two buffers. The idea of this function is to change the window->buffer mapping without adjusting window layout.

Command: proof-layout-windows ¶

Refresh the display of windows according to current display mode.

For multiple frame mode, this function obeys the setting of ‘pg-response-eagerly-raise’, which see.

For single frame mode:

- In two panes mode, this uses a canonical layout made by splitting Emacs windows in equal proportions. The splitting is vertical if Emacs width is smaller than ‘split-width-threshold’ and horizontal otherwise. You can then adjust the proportions by dragging the separating bars.

- In three pane mode, there are three display modes, depending

  where the three useful buffers are displayed: scripting
  buffer, goals buffer and response buffer.

  Here are the three modes:

  - vertical: the 3 buffers are displayed in one column.
  - hybrid: 2 columns mode, left column displays scripting buffer
    and right column displays the 2 others.
  - horizontal: 3 columns mode, one for each buffer (script, goals,
    response).

  By default, the display mode is automatically chosen by
  considering the current Emacs frame width: if it is smaller
  than ‘split-width-threshold’ then vertical mode is chosen,
  otherwise if it is smaller than 1.5 * ‘split-width-threshold’
  then hybrid mode is chosen, finally if the frame is larger than
  1.5 * ‘split-width-threshold’ then the horizontal mode is chosen.

  You can change the value of ‘split-width-threshold’ at your
  will.

  If you want to force one of the layouts, you can set variable
  ‘proof-three-window-mode-policy’ to 'vertical, 'horizontal or
  'hybrid.  The default value is 'smart which sets the automatic
  behaviour described above.

User Option: proof-shrink-windows-tofit ¶

If non-nil, automatically shrink output windows to fit contents.
In single-frame mode, this option will reduce the size of the goals and response windows to fit their contents.

The default value is nil.

User Option: proof-colour-locked ¶

If non-nil, colour the locked region with ‘proof-locked-face’.
If this is not set, buffers will have no special face set on locked regions.

The default value is t.

User Option: proof-output-tooltips ¶

Non-nil causes Proof General to add tooltips for prover output.
Hovers will be added when this option is non-nil. Prover outputs can be displayed when the mouse hovers over the region that produced it and output is available (see ‘proof-full-annotation’). If output is not available, the type of the output region is displayed. Changes of this option will not be reflected in already-processed regions of the script.

The default value is nil.

8.4 User options

Here is a list of the important user options for Proof General, apart from the display options mentioned above.

User options can be set via the customization system already mentioned, via the old-fashioned M-x edit-options mechanism, or simply by adding setq’s to your .emacs file. The first approach is strongly recommended.

Unless mentioned, all of these settings can be changed dynamically, without needing to restart Emacs to see the effect. But you must use customize to be sure that Proof General reconfigures itself properly.

User Option: proof-splash-enable ¶

If non-nil, display a splash screen when Proof General is loaded.

The default value is t.

User Option: proof-electric-terminator-enable ¶

If non-nil, use electric terminator mode.
If electric terminator mode is enabled, pressing a terminator will automatically issue ‘proof-assert-next-command’ for convenience, to send the command straight to the proof process. If the command you want to send already has a terminator character, you don’t need to delete the terminator character first. Just press the terminator somewhere nearby. Electric!

The default value is nil.

User Option: proof-next-command-insert-space ¶

If non-nil, PG will use heuristics to insert newlines or spaces in scripts.
In particular, if electric terminator is switched on, spaces or newlines will be inserted as the user types commands to the prover.

The default value is t.

User Option: proof-toolbar-enable ¶

If non-nil, display Proof General toolbar for script buffers.

The default value is t.

User Option: proof-query-file-save-when-activating-scripting ¶

If non-nil, query user to save files when activating scripting.

Often, activating scripting or executing the first scripting command of a proof script will cause the proof assistant to load some files needed by the current proof script. If this option is non-nil, the user will be prompted to save some unsaved buffers in case any of them corresponds to a file which may be loaded by the proof assistant.

You can turn this option off if the save queries are annoying, but be warned that with some proof assistants this may risk processing files which are out of date with respect to the loaded buffers!

The default value is t.

User Option: PA-script-indent ¶

If non-nil, enable indentation code for proof scripts.

The default value is t.

User Option: PA-one-command-per-line ¶

If non-nil, format for newlines after each command in a script.

The default value is t.

Variable: proof-omit-proofs-option ¶

Set to t to omit complete opaque proofs for speed reasons.
When t, complete opaque proofs in the asserted region are not sent to the proof assistant (and thus not checked). For files with big proofs this can drastically reduce the processing time for the asserted region at the cost of not checking the proofs. For partial and non-opaque proofs in the asserted region all proof commands are sent to the proof assistant.

Using a prefix argument for ‘proof-goto-point’ (M-x proof-goto-point) or ‘proof-process-buffer’ (M-x proof-process-buffer) temporarily disables omitting proofs.

User Option: proof-prog-name-ask ¶

If non-nil, query user which program to run for the inferior process.

The default value is nil.

Variable: PA-prog-args ¶

Arguments to be passed to ‘proof-prog-name’ to run the proof assistant.
If non-nil, will be treated as a list of arguments for ‘proof-prog-name’. Otherwise ‘proof-prog-name’ will be split on spaces to form arguments.

Remark: Arguments are interpreted strictly: each one must contain only one word, with no space (unless it is the same word). For example if the arguments are -x foo -y bar, then the list should be ’("-x" "foo" "-y" "bar"), notice that ’("-x foo" "-y bar") is wrong.

Variable: PA-prog-env ¶: Modifications to ‘process-environment’ made before running ‘proof-prog-name’.
Each element should be a string of the form ENVVARNAME=value. They will be added to the environment before launching the prover (but not pervasively). For example for coq on Windows you might need something like: (setq coq-prog-env ’("HOME=C:\Program Files\Coq\"))

User Option: proof-prog-name-guess ¶

If non-nil, use ‘proof-guess-command-line’ to guess ‘proof-prog-name’.
This option is compatible with ‘proof-prog-name-ask’. No effect if ‘proof-guess-command-line’ is nil.

The default value is nil.

User Option: proof-tidy-response ¶

Non-nil indicates that the response buffer should be cleared often.
The response buffer can be set either to accumulate output, or to clear frequently.

With this variable non-nil, the response buffer is kept tidy by clearing it often, typically between successive commands (just like the goals buffer).

Otherwise the response buffer will accumulate output from the prover.

The default value is t.

User Option: proof-keep-response-history ¶

Whether to keep a browsable history of responses.
With this feature enabled, the buffers used for prover responses will have a history that can be browsed without processing/undoing in the prover. (Changes to this variable take effect after restarting the prover).

The default value is nil.

User Option: pg-input-ring-size ¶

Size of history ring of previous successfully processed commands.

The default value is 32.

User Option: proof-general-debug ¶

Non-nil to run Proof General in debug mode.
This changes some behaviour (e.g. markup stripping) and displays debugging messages in the response buffer. To avoid erasing messages shortly after they’re printed, set ‘proof-tidy-response’ to nil. This is only useful for PG developers.

The default value is nil.

User Option: proof-follow-mode ¶

Choice of how point moves with script processing commands.
One of the symbols: 'locked, 'follow, 'followdown, 'ignore.

If 'locked, point sticks to the end of the locked region. If 'follow, point moves just when needed to display the locked region end. If 'followdown, point if necessary to stay in writeable region If 'ignore, point is never moved after movement commands or on errors.

If you choose 'ignore, you can find the end of the locked using M-x proof-goto-end-of-locked

The default value is locked.

User Option: proof-auto-action-when-deactivating-scripting ¶

If 'retract or 'process, do that when deactivating scripting.

With this option set to 'retract or 'process, when scripting is turned off in a partly processed buffer, the buffer will be retracted or processed automatically.

With this option unset (nil), the user is questioned instead.

Proof General insists that only one script buffer can be partly processed: all others have to be completely processed or completely unprocessed. This is to make sure that handling of multiple files makes sense within the proof assistant.

NB: A buffer is completely processed when all non-whitespace is locked (coloured blue); a buffer is completely unprocessed when there is no locked region.

For some proof assistants (such as Coq) fully processed buffers make no sense. Setting this option to 'process has then the same effect as leaving it unset (nil). (This behaviour is controlled by ‘proof-no-fully-processed-buffer’.)

The default value is nil.

User Option: proof-rsh-command ¶

Shell command prefix to run a command on a remote host.
For example,

   ssh bigjobs

Would cause Proof General to issue the command ‘ssh bigjobs coqtop’ to start Coq remotely on our large compute server called ‘bigjobs’.

The protocol used should be configured so that no user interaction (passwords, or whatever) is required to get going. For proper behaviour with interrupts, the program should also communicate signals to the remote host.

The default value is nil.

8.5 Changing faces

The numerous fonts and colours that Proof General uses are configurable. If you alter faces through the customize menus (or the command M-x customize-face), only the particular kind of display in use (colour window system, monochrome window system, console, …) will be affected. This means you can keep separate default settings for each different display environment where you use Proof General.

As well as the faces listed below, Proof General may use the regular font-lock- faces (eg font-lock-keyword-face, font-lock-variable-name-face, etc) for fontifying the proof script or proof assistant output. These can be altered to your taste just as easily, but note that changes will affect all other modes which use them!

Script buffer faces
Goals and response faces

8.5.1 Script buffer faces

Face: proof-queue-face ¶: Face for commands in proof script waiting to be processed.

Face: proof-locked-face ¶: Face for locked region of proof script (processed commands).

Face: proof-script-sticky-error-face ¶: Proof General face for marking an error in the proof script.

Face: proof-script-highlight-error-face ¶: Proof General face for highlighting an error in the proof script.

Face: proof-mouse-highlight-face ¶: General mouse highlighting face used in script buffer.

Face: proof-highlight-dependent-face ¶: Face for showing (backwards) dependent parts.

Face: proof-highlight-dependency-face ¶: Face for showing (forwards) dependencies.

Face: proof-declaration-name-face ¶: Face for declaration names in proof scripts.
Exactly what uses this face depends on the proof assistant.

Face: proof-tacticals-name-face ¶: Face for names of tacticals in proof scripts.
Exactly what uses this face depends on the proof assistant.

8.5.2 Goals and response faces

Face: proof-error-face ¶: Face for error messages from proof assistant.

Face: proof-warning-face ¶: Face for warning messages.
Warning messages can come from proof assistant or from Proof General itself.

Face: proof-debug-message-face ¶: Face for debugging messages from Proof General.

Face: proof-boring-face ¶: Face for boring text in proof assistant output.

Face: proof-active-area-face ¶: Face for showing active areas (clickable regions), outside of subterm markup.

Face: proof-eager-annotation-face ¶: Face for important messages from proof assistant.

The slightly bizarre name of the last face comes from the idea that while large amounts of output are being sent from the prover, some messages should be displayed to the user while the bulk of the output is hidden. The messages which are displayed may have a special annotation to help Proof General recognize them, and this is an "eager" annotation in the sense that it should be processed as soon as it is observed by Proof General.

8.6 Tweaking configuration settings

This section is a note for advanced users.

Configuration settings are the per-prover customizations of Proof General. These are not intended to be adjusted by the user. But occasionally you may like to test changes to these settings to improve the way Proof General works. You may want to do this when a proof assistant has a flexible proof script language in which one can define new tactics or even operations, and you want Proof General to recognize some of these which the default settings don’t mention. So please feel free to try adjusting the configuration settings and report to us if you find better default values than the ones we have provided.

The configuration settings appear in the customization group prover-config, or via the menu

    Proof-General -> Internals ->  Prover Config

One basic example of a setting you may like to tweak is:

Variable: proof-assistant-home-page ¶: Web address for information on proof assistant.
Used for Proof General’s help menu.

Most of the others are more complicated. For more details of the settings, see Adapting Proof General for full details. To browse the settings, you can look through the customization groups prover-config, proof-script and proof-shell. The group proof-script contains the configuration variables for scripting, and the group proof-shell contains those for interacting with the proof assistant.

Unfortunately, although you can use the customization mechanism to set and save these variables, saving them may have no practical effect because the default settings are mostly hard-wired into the proof assistant code. Ones we expect may need changing appear as proof assistant specific configurations. For example, proof-assistant-home-page is set in the Coq code from the value of the customization setting coq-www-home-page. At present there is no easy way to save changes to other configuration variables across sessions, other than by editing the source code. (In future versions of Proof General, we plan to make all configuration settings editable in Customize, by shadowing the settings as prover specific ones using the PA- mechanism).

9 Hints and Tips

Apart from the packages officially supported in Proof General, many other features of Emacs are useful when using Proof General, even though they need no specific configuration for Proof General. It is worth taking a bit of time to explore the Emacs manual to find out about them.

Here we provide some hints and tips for a couple of Emacs features which users have found valuable with Proof General. Further contributions to this chapter are welcomed!

Adding your own keybindings
Using file variables
Using abbreviations

9.1 Adding your own keybindings

Proof General follows Emacs convention for file modes in using C-c prefix key-bindings for its own functions, which is why some of the default keyboard short-cuts are quite lengthy.

Some users may prefer to add additional key-bindings for shorter sequences. This can be done interactively with the command M-x local-set-key, or for longevity, by adding code like this to your .emacs file:


(eval-after-load "proof-script" '(progn
 (define-key proof-mode-map [(control n)] 
                            'proof-assert-next-command-interactive)
 (define-key proof-mode-map [(control b)] 
                            'proof-undo-last-successful-command)
 ))

This lisp fragment adds bindings for every buffer in proof script mode (the Emacs keymap is called proof-mode-map). To just affect one prover, use a keymap name like coq-mode-map and evaluate after the library coq has been loaded.

To find the names of the functions you may want to bind, look in this manual, or query current bindings interactively with C-h k. This command (describe-key) works for menu operations as well; also use it to discover the current key-bindings which you’re losing by declarations such as those above. By default, C-n is next-line and C-b is backward-char-command; neither are really needed if you have working cursor keys.

If your keyboard has a super modifier (on my PC keyboard it has a Windows symbol and is next to the control key), you can freely bind keys on that modifier globally (since none are used by default). Use lisp like this:

(global-set-key [?\s-l] 'maths-menu-insert-lambda)
(global-set-key [?\s-l] 'maths-menu-insert-lambda)

(global-set-key [?\s-l] 'maths-menu-insert-lambda)
(global-set-key [?\s-L] 'maths-menu-insert-Lambda)
(global-set-key [?\s-D] 'maths-menu-insert-Delta)

(global-set-key [?\s-a] 'maths-menu-insert-for-all)
(global-set-key [?\s-e] 'maths-menu-insert-there-exists)
(global-set-key [?\s-t] 'maths-menu-insert-down-tack)
(global-set-key [?\s-b] 'maths-menu-insert-up-tack)

(global-set-key [?\s-\#] 'maths-menu-insert-music-sharp-sign)
(global-set-key [?\s-\.] 'maths-menu-insert-horizontal-ellipsis)

(global-set-key [?\s-3] 'proof-three-window-toggle)

This defines a bunch of short-cuts for inserting symbols taken from the Maths Menu, see Unicode symbols and special layout support and a short-cut for enabling three window mode, see Display customization.

9.2 Using file variables

A very convenient way to customize file-specific variables is to use File Variables (See (emacs)File Variables). This feature of Emacs permits to specify values for certain Emacs variables when a file is loaded. File variables and their values are written as a list at the end of the file.

Remark 1: The examples in the following are for Coq but the trick is applicable to other provers.

Remark 2: For Coq specifically, there is a recommended other way of configuring Coq command-line options: project files (Using the Coq project file). However file variables are useful to set a specific coqtop executable, or for defining file-specific command-line options. Actually, since project files are intended to be included in the distribution of a library (and included in its repository), the file variables can be used to set non versioned options like coq-prog-name.

Remark 3: For obvious security reasons, when emacs reads file variables, it asks for permission to the user before applying the assignment. You should read carefully the content of the variable before accepting. You can hit ! to accept definitely the exact values at hand.

Let us take a concrete example: suppose the makefile for foo.v is located in directory .../dir/, you need the right compile command in the compile-command emacs variable. Moreover suppose that you want coqtop to be found in a non standard directory. To put these values in file variables, here is what you should put at the end of foo.v:

(* 
*** Local Variables: ***
*** coq-prog-name: "../../coqsrc/bin/coqtop" ***
*** compile-command: "make -C .. -k bar/foo.vo" ***
*** End:***
*)

And then the right call to make will be done if you use the M-x compile command, and the correct coqtop will be called by ProofGeneral. Note that the lines are commented in order to be ignored by the proof assistant. It is possible to use this mechanism for all variables, See (emacs)File Variables.

NOTE: coq-prog-name should contain only the coqtop executable, not the options.

One can also specify file variables on a per directory basis, See (emacs)Directory Variables. You can achieve almost the same as above for all the files of a directory by storing

((coq-mode . ((coq-prog-name . "/home/xxx/yyy/coqsrc/bin/coqtop")
              (compile-command . "make -C .. -k"))))

into the file .dir-locals.el in one of the parent directories. The value in this file must be an alist that maps mode names to alists, where these latter alists map variables to values. You can aso put arbitrary code in this file See (emacs)Directory Variables.

Note: if you add such content to the .dir-locals.el file you should restart Emacs or revert your buffer.

9.3 Using abbreviations

A very useful package of Emacs supports automatic expansions of abbreviations as you type, See (emacs)Abbrevs.

For example, the proof assistant Coq has many command strings that are long, such as “reflexivity,” “Inductive,” “Definition” and “Discriminate.” Here is a part of the Coq Proof General abbreviations:

"abs" "absurd "
"ap" "apply "
"as" "assumption"

The above list was taken from the file that Emacs saves between sessions. The easiest way to configure abbreviations is as you write, by using the key presses C-x a g (add-global-abbrev) or C-x a i g (inverse-add-global-abbrev). To enable automatic expansion of abbreviations (which can be annoying), the Abbrev minor mode, type M-x abbrev-mode RET. When you are not in Abbrev mode you can expand an abbreviation by pressing C-x ' (expand-abbrev). See the Emacs manual for more details.

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.

Coq-specific commands
Using the Coq project file
Proof using annotations
Multiple File Support
Omitting proofs for speed
Editing multiple proofs
User-loaded tactics
Indentation tweaking
Holes feature
Proof-Tree Visualization
Showing Proof Diffs
Opam-switch-mode support

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. You need either to launch emacs with the right executable in the path or use See (emacs)File Variables or See (emacs)Directory Variables. See Using file variables below.

Changing the name of the coq project file
Disabling the coq project file mechanism

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-local.el file, See (emacs)Directory Variables. The file .dir-local.el should then contain

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

Note that variables set in .dir-local.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-local.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.

Automatic Compilation in Detail
Locking Ancestors
Quick and inconsistent compilation
Customizing Coq Multiple File Support
Current Limitations

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

With a prefix argument, both proof-goto-point and proof-process-buffer will temporarily disable the omit proofs feature and send the full proof script to Coq.

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.

10.6 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.7 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 Escaping script management) or C-c C-v to re-issue an erroneously back-tracked tactic without recording it in the script.

10.8 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.9 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.10 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 Graphical Proof-Tree Visualization. To find out which versions of Prooftree are compatible with this version of Proof General, see 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.11 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.12 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’

11 EasyCrypt Proof General

EasyCrypt Proof General is an instantiation of Proof General for the EasyCrypt proof assistant.

EasyCrypt specific commands
EasyCrypt weak-check mode
EasyCrypt customizations

11.1 EasyCrypt specific commands

EasyCrypt Proof General supplies the following key-bindings:

C-c C-a C-p: Prompts for “print” query arguments.
C-c C-a C-c: The same for a “check” query.

11.2 EasyCrypt weak-check mode

The EasyCrypt menu contains a Weak-check mode toggle menu, which allows you to enable or disable the EasyCrypt Weak-Check mode. When enabled, all smt calls are ignored and assumed to succeed.

11.3 EasyCrypt customizations

Here are some of the other user options specific to EasyCrypt. You can set these as usual with the customization mechanism.

User Option: easycrypt-prog-name ¶

Name of program to run EasyCrypt.

The default value is "easycrypt".

Variable: easycrypt-load-path ¶: Non-standard EasyCrypt library load path.
This list specifies the include path for EasyCrypt. The elements of this list are strings.

Variable: easycrypt-web-page ¶: URL of web page for EasyCrypt.

12 Shell Proof General

This instance of Proof General is not really for proof assistants at all, but simply provided as a handy way to use a degenerate form of script management with other tools.

Suppose you have a software tool of some kind with a command line interface, and you want to demonstrate several example uses of it, perhaps at a conference. But the command lines for your tool may be quite complicated, so you do not want to type them in live. Instead, you just want to cut and paste from a pre-recorded list. But watching somebody cut and paste commands into a window is almost as tedious as watching them type those commands!

Shell Proof General comes to the rescue. Simply record your commands in a file with the extension .pgsh, and load up Proof General. Now use the toolbar to send each line of the file to your tool, and have the output displayed clearly in another window. Much easier and more pleasant for your audience to watch!

If you wish, you may adjust the value of proof-prog-name in pgshell.el to launch your program rather than the shell interpreter.

We welcome feedback and suggestions concerning this subsidiary provision in Proof General. Please recommend it to your colleagues (e.g., the model checking crew).

History of Proof General

It all started some time in 1994. There was no Emacs interface for LEGO. Back then, Emacs militants worked directly with the Emacs shell to interact with the LEGO system.

David Aspinall convinced Thomas Kleymann that programming in Emacs Lisp wasn’t so difficult after all. In fact, Aspinall had already implemented an Emacs interface for Isabelle with bells and whistles, called Isamode. Soon after, the package lego-mode was born. Users were able to develop proof scripts in one buffer. Support was provided to automatically send parts of the script to the proof process. The last official version with the name lego-mode (1.9) was released in May 1995.

The interface project really took off the ground in November 1996. Yves Bertot had been working on a sophisticated user interface for the Coq system (CtCoq) based on the generic environment Centaur. He visited the Edinburgh LEGO group for a week to transfer proof-by-pointing technology. Even though proof-by-pointing is an inherently structure-conscious algorithm, within a week, Yves Bertot, Dilip Sequeira and Thomas Kleymann managed to implement a first prototype of proof-by-pointing in the Emacs interface for LEGO [BKS97].

Perhaps we could reuse even more of the CtCoq system. It being a structure editor did no longer seem to be such an obstacle. Moreover, to conveniently use proof-by-pointing in actual developments, one would need better support for script management.

In 1997, Dilip Sequeira implemented script management in our Emacs interface for LEGO following the recipe in [BT98]. Inspired by the project CROAP, the implementation made some effort to be generic. A working prototype was demonstrated at UITP’97.

In October 1997, Healfdene Goguen ported lego-mode to Coq. Part of the generic code in the lego package was outsourced (and made more generic) in a new package called proof. Dilip Sequeira provided some LEGO-specific support for handling multiple files and wrote a few manual pages. The system was reasonably robust and we shipped out the package to friends.

In June 1998, David Aspinall reentered the picture by providing an instantiation for Isabelle. Actually, our previous version wasn’t quite as generic as we had hoped. Whereas LEGO and Coq are similar systems in many ways, Isabelle was really a different beast. Fierce re-engineering and various usability improvements were provided by Aspinall and Kleymann to make it easier to instantiate to new proof systems. The major technical improvement was a truly generic extension of script management to work across multiple files.

It was time to come up with a better name than just proof mode. David Aspinall suggested Proof General and set about reorganizing the file structure to disentangle the Proof General project from LEGO at last. He cooked up some images and bolted on a toolbar, so a naive user can replay proofs without knowing a proof assistant language or even Emacs hot-keys. He also designed some web pages, and wrote most of this manual.

Despite views of some detractors, we demonstrated that an interface both friendly and powerful can be built on top of Emacs. Proof General 2.0 was the first official release of the improved program, made in December 1998.

Version 2.1 was released in August 1999. It was used at the Types Summer School held in Giens, France in September 1999 (see http://www-sop.inria.fr/types-project/types-sum-school.html). About 50 students learning Coq, Isabelle, and LEGO used Proof General for all three systems. This experience provided invaluable feedback and encouragement to make the improvements that went into Proof General 3.0.

Old News for 3.0
Old News for 3.1
Old News for 3.2
Old News for 3.3
Old News for 3.4
Old News for 3.5
Old News for 3.6
Old News for 3.7

Old News for 3.0

Proof General 3.0 (released November 1999) has many improvements over 2.x releases.

First, there are usability improvements. The toolbar was somewhat impoverished before. It now has twice as many buttons, and includes all of the useful functions used during proof which were previously hidden on the menu, or even only available as key-presses. Key-bindings have been re-organized, users of previous versions may notice. The menu has been redesigned and coordinated with the toolbar, and now gives easy access to more of the features of Proof General. Previously several features were only likely to be discovered by those keen enough to read this manual!

Second, there are improvements, extensions, and bug fixes in the generic basis. Proofs which are unfinished and not explicitly closed by a “save” type command are supported by the core, if they are allowed by the prover. The design of switching the active scripting buffer has been streamlined. The management of the queue of commands waiting to be sent to the shell has been improved, so there are fewer unnecessary "Proof Process Busy!" messages. The support for scripting with multiple files was improved so that it behaves reliably with Isabelle99; file reading messages can be communicated in both directions now. The proof shell filter has been optimized to give hungry proof assistants a better share of CPU cycles. Proof-by-pointing has been resurrected; even though LEGO’s implementation is incomplete, it seems worth maintaining the code in Proof General so that the implementors of other proof assistants are encouraged to provide support. For one example, we can certainly hope for support in Coq, since the CtCoq proof-by-pointing code has been moved into the Coq kernel lately. We need a volunteer from the Coq community to help to do this.

An important new feature in Proof General 3.0 is support for X-Symbol, which means that real logical symbols, Greek letters, etc can be displayed during proof development, instead of their ASCII approximations. This makes Proof General a more serious competitor to native graphical user interfaces.

Finally, Proof General has become much easier to adapt to new provers — it fails gracefully (or not at all!) when particular configuration variables are unset, and provides more default settings which work out-of-the-box. An example configuration for Isabelle is provided, which uses just 25 or so simple settings.

This manual has been updated and extended for Proof General 3.0. Amongst other improvements, it has a better description of how to add support for a new prover.

See the CHANGES file in the distribution for more information about the latest improvements in Proof General. Developers should check the ChangeLog in the developer’s release for detailed comments on internal changes.

Most of the work for Proof General 3.0 has been done by David Aspinall. Markus Wenzel helped with Isabelle support, and provided invaluable feedback and testing, especially for the improvements to multiple file handling. Pierre Courtieu took responsibility from Patrick Loiseleur for Coq support, although improvements in both Coq and LEGO instances for this release were made by David Aspinall. Markus Wenzel provided support for his Isar language, a new proof language for Isabelle. David von Oheimb helped to develop the generic version of his X-Symbol addition which he originally provided for Isabelle.

A new instantiation of Proof General is being worked on for Plastic, a proof assistant being developed at the University of Durham.

Old News for 3.1

Proof General 3.1 (released March 2000) is a bug-fix improvement over version 3.0. There are some minor cosmetic improvements, but large changes have been held back to ensure stability. This release solves a few minor problems which came to light since the final testing stages for 3.0. It also solves some compatibility problems, so now it works with various versions of Emacs which we hadn’t tested with before (non-mule GNU Emacs, certain Japanese Emacs versions).

We’re also pleased to announce HOL Proof General, a new instance of Proof General for HOL98. This is supplied as a "technology demonstration" for HOL users in the hope that somebody from the HOL community will volunteer to adopt it and become a maintainer and developer. (Otherwise, work on HOL Proof General will not continue).

Apart from that there are a few other small improvements. Check the CHANGES file in the distribution for full details.

The HOL98 support and much of the work on Proof General 3.1 was undertaken by David Aspinall while he was visiting ETL, Osaka, Japan, supported by the British Council and ETL.

Old News for 3.2

Proof General 3.2 introduced several new features and some bug fixes. One noticeable new feature is the addition of a prover-specific menu for each of the supported provers. This menu has a “favourites” feature that you can use to easily define new functions. Please contribute other useful functions (or suggestions) for things you would like to appear on these menus.

Because of the new menus and to make room for more commands, we have made a new key map for prover specific functions. These now all begin with C-c C-a. This has changed a few key bindings slightly.

Another new feature is the addition of prover-specific completion tables, to encourage the use of Emacs’s completion facility, using C-RET. See Support for completion, for full details.

A less obvious new feature is support for turning the proof assistant output on and off internally, to improve efficiency when processing large scripts. This means that more of your CPU cycles can be spent on proving theorems.

Adapting for new proof assistants continues to be made more flexible, and easier in several places. This has been motivated by adding experimental support for some new systems. One new system which had good support added in a very short space of time is PhoX (see the PhoX home page for more information). PhoX joins the rank of officially supported Proof General instances, thanks to its developer Christophe Raffalli.

Breaking the manual into two pieces was overdue: now all details on adapting Proof General, and notes on its internals, are in the Adapting Proof General manual. You should find a copy of that second manual close to wherever you found this one; consult the Proof General home page if in doubt.

The internal code of Proof General has been significantly overhauled for this version, which should make it more robust and readable. The generic code has an improved file structure, and there is support for automatic generation of autoload functions. There is also a new mechanism for defining prover-specific customization and instantiation settings which fits better with the customize library. These settings are named in the form PA-setting-name in the documentation; you replace PA by the symbol for the proof assistant you are interested in. See Customizing Proof General, for details.

Finally, important bug fixes include the robustification against write-file (C-x C-w), revert-buffer, and friends. These are rather devious functions to use during script management, but Proof General now tries to do the right thing if you’re deviant enough to try them out!

Work on this release was undertaken by David Aspinall between May-September 2000, and includes contributions from Markus Wenzel, Pierre Courtieu, and Christophe Raffalli. Markus added some Isar documentation to this manual.

Old News for 3.3

Proof General 3.3 includes a few feature additions, but mainly the focus has been on compatibility improvements for new versions of provers (in particular, Coq 7), and new versions of emacs (in particular, XEmacs 21.4).

One new feature is control over visibility of completed proofs, See Visibility of completed proofs. Another new feature is the tracking of theorem dependencies inside Isabelle. A context-sensitive menu (right-button on proof scripts) provides facility for browsing the ancestors and child theorems of a theorem, and highlighting them. The idea of this feature is that it can help you untangle and rearrange big proof scripts, by seeing which parts are interdependent. The implementation is provisional and not documented yet in the body of this manual. It only works for the "classic" version of Isabelle99-2.

Old News for 3.4

Proof General 3.4 adds improvements and also compatibility fixes for new versions of Emacs, in particular, for GNU Emacs 21, which adds the remaining pretty features that have only been available to XEmacs users until now (the toolbar and X-Symbol support).

One major improvement has been to provide better support for synchronization with Coq proof scripts; now Coq Proof General should be able to retract and replay most Coq proof scripts reliably. Credit is due to Pierre Courtieu, who also updated the documentation in this manual.

As of version 3.4, Proof General is distributed under the GNU General Public License (GPL). Compared with the previous more restrictive license, this means the program can now be redistributed by third parties, and used in any context without applying for a special license. Despite these legal changes, we would still appreciate if you send us back any useful improvements you make to Proof General.

Old News for 3.5

Old News for 3.6

There was no 3.6 release of Proof General.

Old News for 3.7

Proof General version 3.7.1 is an updated and enhanced version of Proof General 3.7. See CHANGES for more details.

Proof General version 3.7 collects together a cumulative set of improvements to Proof General 3.5. There are compatibility fixes for newer Emacs versions, and particularly for GNU Emacs: credit is due to Stefan Monnier for an intense period of debugging and patching. The options menu has been simplified and extended, and the display management is improved and repaired for Emacs API changes. There are some other usability improvements, some after feedback from use at TYPES Summer Schools. Many new features have been added to enhance Coq mode (thanks to Pierre Courtieu) and several improvements made for Isabelle (thanks to Makarius Wenzel, Stefan Berghofer and Tjark Weber).

Support has been added for the useful Emacs packages Speedbar and Index Menu, both usually distributed with Emacs. A compatible version of the Emacs package Math-Menu (for Unicode symbols) is bundled with Proof General. An experimental Unicode Tokens package has been added which will replace X-Symbol.

See the CHANGES file in the distribution for more complete details of changes since version 3.5, and the appendix History of Proof General for old news.

Prover	Extensions	Mode
Coq	`.v`	`coq-mode`
Phox	`.phx`	`phox-mode`
PG-Shell	`.pgsh`	`pgshell-mode`
EasyCrypt	`.ec`	`easycrypt-mode`

	Index Entry	Section

A
	active scripting buffer:	Active scripting buffer
	Alt:	Prerequisites for this manual
	annotation:	Document centred working
	Assertion:	Locked queue and editing regions
	Assertion:	Asserting across files
	auto raise:	Display customization
	Automatic processing:	Automatic processing
	autosend:	Automatic processing

B
	blue text:	Locked queue and editing regions
	buffer display customization:	Display customization

C
	Centaur:	History of Proof General
	colour:	Syntax highlighting
	completion:	Support for completion
	CtCoq:	History of Proof General
	Customization:	Customizing Proof General

D
	Dedicated windows:	User options
	display customization:	Display customization

E
	EasyCrypt Proof General:	EasyCrypt Proof General
	Editing region:	Locked queue and editing regions
	Emacs customization library:	How to customize

F
	Features:	Features of Proof General
	file variables:	Using file variables
	font lock:	Syntax highlighting
	frames:	Display customization
	Future:	Future

G
	generic:	History of Proof General
	goal:	Goal-save sequences
	goal-save sequences:	Goal-save sequences
	goals buffer:	Summary of Proof General buffers
	Greek letters:	Unicode symbols and special layout support

H
	history:	History of Proof General

I
	Imenu:	Imenu and Speedbar
	Indentation:	User options
	index menu:	Imenu and Speedbar
	Input ring:	Editing features
	Input ring:	User options

K
	key sequences:	Prerequisites for this manual
	keybindings:	Adding your own keybindings

L
	Locked region:	Locked queue and editing regions
	logical symbols:	Unicode symbols and special layout support

M
	maintenance:	Credits
	mathematical symbols:	Unicode symbols and special layout support
	Maths Menu:	Unicode symbols and special layout support
	Meta:	Prerequisites for this manual
	Multiple Files:	Advanced Script Management and Editing
	multiple frames:	Display customization
	multiple windows:	Display customization

N
	news:	News for Version 4.5
	news:	News for Version 4.4
	news:	News for Version 4.3
	news:	News for Version 4.2
	news:	News for Version 4.1
	news:	News for Version 4.0
	news:	Old News for 3.1
	news:	Old News for 3.2

O
	outline mode:	Support for outline mode

P
	pink text:	Locked queue and editing regions
	prefix argument:	Script processing commands
	proof assistant:	Introducing Proof General
	proof by pointing:	Summary of Proof General buffers
	proof by pointing:	History of Proof General
	Proof General:	Introducing Proof General
	Proof General Kit:	Future
	proof script:	Proof scripts
	Proof script indentation:	User options
	proof script mode:	Script buffers
	proof-tree visualization:	Graphical Proof-Tree Visualization

Q
	Query program name:	User options
	Queue region:	Locked queue and editing regions

R
	Remote host:	User options
	Remote shell:	User options
	response buffer:	Summary of Proof General buffers
	Retraction:	Locked queue and editing regions
	Retraction:	Retracting across files
	Running proof assistant remotely:	User options

S
	save:	Goal-save sequences
	script buffer:	Script buffers
	script management:	History of Proof General
	scripting:	Proof scripts
	Shell:	Escaping script management
	shell buffer:	Summary of Proof General buffers
	Shell Proof General:	Shell Proof General
	Speedbar:	Imenu and Speedbar
	Strict read-only:	User options
	structure editor:	History of Proof General
	subscripts:	Unicode symbols and special layout support
	superscripts:	Unicode symbols and special layout support
	Switching between proof scripts:	Switching between proof scripts
	symbols:	Unicode symbols and special layout support

T
	tags:	Support for tags
	three-buffer interaction:	Display customization
	Tokens Mode:	Unicode symbols and special layout support
	Toolbar button enablers:	User options
	Toolbar disabling:	User options
	Toolbar follow mode:	User options

U
	Undo in read-only region:	User options
	User options:	User options
	Using Customize:	How to customize

V
	Visibility of proofs:	Visibility of completed proofs

W
	Why use Proof General?:	Features of Proof General

X
	X-Symbols:	Unicode symbols and special layout support

	Index Entry	Section

A
	`add-completions-from-tags-table`:	Support for tags

C
	`complete`:	Support for completion

I
	`indent-for-tab-command`:	Script editing commands

P
	`pg-goals-button-action`:	Goals buffer commands
	`pg-hide-all-proofs`:	Visibility of completed proofs
	`pg-identifier-under-mouse-query`:	Goals buffer commands
	`pg-next-input`:	Editing features
	`pg-next-matching-input`:	Editing features
	`pg-next-matching-input-from-input`:	Editing features
	`pg-previous-input`:	Editing features
	`pg-previous-matching-input`:	Editing features
	`pg-previous-matching-input-from-input`:	Editing features
	`pg-response-clear-displays`:	Proof assistant commands
	`pg-show-all-proofs`:	Visibility of completed proofs
	`pg-toggle-visibility`:	Visibility of completed proofs
	`proof-active-area-face`:	Goals and response faces
	`proof-assert-next-command-interactive`:	Script processing commands
	`proof-assert-until-point-interactive`:	Script processing commands
	`proof-autosend-toggle`:	Automatic processing
	`proof-boring-face`:	Goals and response faces
	`proof-ctxt`:	Proof assistant commands
	`proof-debug-message-face`:	Goals and response faces
	`proof-declaration-name-face`:	Script buffer faces
	`proof-display-some-buffers`:	Proof assistant commands
	`proof-display-some-buffers`:	Display customization
	`proof-eager-annotation-face`:	Goals and response faces
	`proof-electric-terminator-toggle`:	Script processing commands
	`proof-error-face`:	Goals and response faces
	`proof-find-theorems`:	Proof assistant commands
	`proof-frob-locked-end`:	Escaping script management
	`proof-goto-command-end`:	Script editing commands
	`proof-goto-command-start`:	Script editing commands
	`proof-goto-end-of-locked`:	Script editing commands
	`proof-goto-point`:	Script processing commands
	`proof-help`:	Proof assistant commands
	`proof-highlight-dependency-face`:	Script buffer faces
	`proof-highlight-dependent-face`:	Script buffer faces
	`proof-interrupt-process`:	Proof assistant commands
	`proof-issue-goal`:	Toolbar commands
	`proof-issue-save`:	Toolbar commands
	`proof-layout-windows`:	Display customization
	`proof-locked-face`:	Script buffer faces
	`proof-minibuffer-cmd`:	Proof assistant commands
	`proof-mouse-highlight-face`:	Script buffer faces
	`proof-prf`:	Proof assistant commands
	`proof-process-buffer`:	Script processing commands
	`proof-query-identifier`:	Proof assistant commands
	`proof-queue-face`:	Script buffer faces
	`proof-retract-buffer`:	Script processing commands
	`proof-retract-until-point-interactive`:	Script processing commands
	`proof-script-highlight-error-face`:	Script buffer faces
	`proof-script-sticky-error-face`:	Script buffer faces
	`proof-shell-exit`:	Proof assistant commands
	`proof-shell-restart`:	Proof assistant commands
	`proof-shell-start`:	Proof assistant commands
	`proof-tacticals-name-face`:	Script buffer faces
	`proof-toggle-active-scripting`:	Active scripting buffer
	`proof-undo-and-delete-last-successful-command`:	Script processing commands
	`proof-undo-last-successful-command`:	Script processing commands
	`proof-warning-face`:	Goals and response faces

U
	`unicode-tokens-copy`:	Moving between Unicode and tokens
	`unicode-tokens-fraktur-font-face`:	Special layout
	`unicode-tokens-list-shortcuts`:	Finding available tokens shortcuts and symbols
	`unicode-tokens-list-tokens`:	Finding available tokens shortcuts and symbols
	`unicode-tokens-list-unicode-chars`:	Finding available tokens shortcuts and symbols
	`unicode-tokens-paste`:	Moving between Unicode and tokens
	`unicode-tokens-sans-font-face`:	Special layout
	`unicode-tokens-script-font-face`:	Special layout
	`unicode-tokens-serif-font-face`:	Special layout
	`unicode-tokens-symbol-font-face`:	Selecting suitable fonts

	Index Entry	Section

C
	`coq-compile-auto-save`:	Customizing Coq Multiple File Support
	`coq-compile-before-require`:	Customizing Coq Multiple File Support
	`coq-compile-command`:	Customizing Coq Multiple File Support
	`coq-compile-ignored-directories`:	Customizing Coq Multiple File Support
	`coq-compile-keep-going`:	Customizing Coq Multiple File Support
	`coq-compile-parallel-in-background`:	Customizing Coq Multiple File Support
	`coq-compile-second-stage-delay`:	Customizing Coq Multiple File Support
	`coq-confirm-external-compilation`:	Customizing Coq Multiple File Support
	`coq-kill-coq-on-opam-switch`:	Opam-switch-mode support
	`coq-load-path`:	Customizing Coq Multiple File Support
	`coq-load-path-include-current`:	Customizing Coq Multiple File Support
	`coq-lock-ancestors`:	Customizing Coq Multiple File Support
	`coq-max-background-compilation-jobs`:	Customizing Coq Multiple File Support
	`coq-max-background-second-stage-percentage`:	Customizing Coq Multiple File Support
	`coq-mode-hooks`:	Syntax highlighting
	`coq-project-filename`:	Changing the name of the coq project file
	`coq-use-project-file`:	Disabling the coq project file mechanism

E
	`easycrypt-load-path`:	EasyCrypt customizations
	`easycrypt-prog-name`:	EasyCrypt customizations
	`easycrypt-web-page`:	EasyCrypt customizations

P
	`PA-completion-table`:	Support for completion
	`PA-one-command-per-line`:	User options
	`PA-prog-args`:	User options
	`PA-prog-env`:	User options
	`PA-script-indent`:	User options
	`pg-input-ring-size`:	User options
	`proof-assistant-home-page`:	Tweaking configuration settings
	`proof-auto-action-when-deactivating-scripting`:	User options
	`proof-auto-raise-buffers`:	Display customization
	`proof-autosend-enable`:	Automatic processing
	`proof-colour-locked`:	Display customization
	`proof-delete-empty-windows`:	Display customization
	`proof-disappearing-proofs`:	Visibility of completed proofs
	`proof-electric-terminator-enable`:	User options
	`proof-follow-mode`:	User options
	`proof-full-annotation`:	Document centred working
	`proof-general-debug`:	User options
	`proof-goal-with-hole-regexp`:	Imenu and Speedbar
	`proof-goal-with-hole-result`:	Imenu and Speedbar
	`proof-keep-response-history`:	User options
	`proof-multiple-frames-enable`:	Display customization
	`proof-next-command-insert-space`:	User options
	`proof-omit-proofs-option`:	User options
	`proof-output-tooltips`:	Display customization
	`proof-prog-name-ask`:	User options
	`proof-prog-name-guess`:	User options
	`proof-query-file-save-when-activating-scripting`:	User options
	`proof-rsh-command`:	User options
	`proof-script-indent`:	Script editing commands
	`proof-shrink-windows-tofit`:	Display customization
	`proof-splash-enable`:	User options
	`proof-strict-read-only`:	Document centred working
	`proof-terminal-string`:	Script editing commands
	`proof-three-window-enable`:	Display customization
	`proof-tidy-response`:	User options
	`proof-toolbar-enable`:	User options

U
	`unicode-tokens-font-family-alternatives`:	Selecting suitable fonts
	`unicode-tokens-highlight-unicode`:	Moving between Unicode and tokens

	Index Entry	Section

C
	`C-c C-.`:	Script editing commands
	`C-c C-a`:	Script editing commands
	`C-c C-a C-)`:	Coq-specific commands
	`C-c C-a C-a`:	Coq-specific commands
	`C-c C-a C-b`:	Coq-specific commands
	`C-c C-a C-c`:	Coq-specific commands
	`C-c C-a C-c`:	EasyCrypt specific commands
	`C-c C-a C-i`:	Coq-specific commands
	`C-c C-a C-o`:	Coq-specific commands
	`C-c C-a C-p`:	Coq-specific commands
	`C-c C-a C-p`:	EasyCrypt specific commands
	`C-c C-a C-s`:	Coq-specific commands
	`C-c C-b`:	Script processing commands
	`C-c C-BS`:	Script processing commands
	`C-c C-c`:	Proof assistant commands
	`C-c C-e`:	Script editing commands
	`C-c C-f`:	Proof assistant commands
	`C-c C-h`:	Proof assistant commands
	`C-c C-n`:	Script processing commands
	`C-c C-p`:	Proof assistant commands
	`C-c C-r`:	Script processing commands
	`C-c C-RET`:	Script processing commands
	`C-c C-t`:	Proof assistant commands
	`C-c C-u`:	Script processing commands
	`C-c C-v`:	Proof assistant commands

M
	`M-n`:	Editing features
	`M-p`:	Editing features

Proof General

Preface

News for Version 4.5

News for Version 4.4

News for Version 4.3

News for Version 4.2

News for Version 4.1

News for Version 4.0

Future

Credits

1 Introducing Proof General

1.1 Installing Proof General

1.2 Quick start guide

1.3 Features of Proof General

1.4 Supported proof assistants

1.5 Prerequisites for this manual

1.6 Organization of this manual

2 Basic Script Management

2.1 Walkthrough example in Isabelle

2.2 Proof scripts

2.3 Script buffers

2.3.1 Locked, queue, and editing regions

2.3.2 Goal-save sequences

2.3.3 Active scripting buffer

2.4 Summary of Proof General buffers

2.5 Script editing commands

2.6 Script processing commands

2.7 Proof assistant commands

2.8 Toolbar commands

2.9 Interrupting during trace output

3 Advanced Script Management and Editing

3.1 Document centred working

3.2 Automatic processing

3.3 Visibility of completed proofs

3.4 Switching between proof scripts

3.5 View of processed files

3.6 Retracting across files

3.7 Asserting across files

3.8 Automatic multiple file handling

3.9 Escaping script management

3.10 Editing features

4 Unicode symbols and special layout support

4.1 Maths menu

4.2 Unicode Tokens mode

4.3 Configuring tokens symbols and shortcuts

4.4 Special layout

4.5 Moving between Unicode and tokens

4.6 Finding available tokens shortcuts and symbols

4.7 Selecting suitable fonts

5 Support for other Packages

5.1 Syntax highlighting

5.2 Imenu and Speedbar

5.3 Support for outline mode

5.4 Support for completion

5.5 Support for tags

6 Subterm Activation and Proof by Pointing

6.1 Goals buffer commands

7 Graphical Proof-Tree Visualization

7.1 Starting and Stopping Proof-Tree Visualization

7.2 Features of Prooftree

7.3 Prooftree Customization

8 Customizing Proof General

8.1 Basic options

8.2 How to customize

8.3 Display customization

8.4 User options

8.5 Changing faces

8.5.1 Script buffer faces

8.5.2 Goals and response faces

8.6 Tweaking configuration settings

9 Hints and Tips

9.1 Adding your own keybindings

9.2 Using file variables

9.3 Using abbreviations

10 Coq Proof General

10.1 Coq-specific commands

10.2 Using the Coq project file

10.2.1 Changing the name of the coq project file

10.2.2 Disabling the coq project file mechanism

10.3 Proof using annotations