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!

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 section Unicode symbols and special layout support and a short-cut for enabling three window mode, see section 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.

This document was generated on April 18, 2024 using texi2html 1.82.