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

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 isar-mode-map and evaluate after the library isar 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 options: project files (Using the Coq project file). Actually, project files are intended to be included in the distribution of a library (and included in its repository), so the Coq options specified in project files are supposed to work for all users. In contrast, user-defined options such as coq-prog-name should preferably be specified in a directory-local-variables file (see below).

For example, in Coq projects involving multiple directories, it is necessary to set the variable coq-load-path (Customizing Coq Multiple File Support). Here is an example: Assume the file ‘.../dir/bar/foo.v’ depends on modules in .../dir/theories/. Then you can put the following at the end of ‘foo.v’:

 
(* 
*** Local Variables: ***
*** coq-load-path: ("../theories") ***
*** End: ***
*)

This way, the right command line arguments are passed to the invocation of coqtop when scripting starts in ‘foo.v’. Note that the load path "../theories" is project or even file specific, and that therefore a global setting via the configuration tool would be inappropriate. With file variables, Emacs will set coq-load-path automatically when visiting foo.v. Moreover, the setting of coq-load-path in different files or buffers will not be affected. (File variables become buffer local.)

Extending the previous example, if the makefile for ‘foo.v’ is located in directory ‘.../dir/’, you can add the right compile command. You can also specify a "-R" command. And if you want a non standard coq executable to be used, here is what you should put in variables:

 
(* 
*** Local Variables: ***
*** coq-prog-name: "../../coqsrc/bin/coqtop" ***
*** coq-load-path: (("../util" "util") "../theories") ***
*** 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. 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.

One can also specify file variables on a per directory basis, See (emacs)Directory Variables. For instance, assume you have a Coq project with several subdirectories and you want to put each subdirectory into coq-load-path for every file in the project. You can achieve this by storing

 
((coq-mode . ((coq-load-path . (("../util" "util") "../theories")))))

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.

Regarding the configuration of the coq-prog-name variable, the .dir-locals.el file should contain something like:

 
((coq-mode . ((coq-prog-name . ".../path/to/coqtop"))))

Note: if you add such content to the .dir-locals.el file you should restart Emacs to take this change into account (or just run M-x proof-shell-exit RET yes RET and M-x normal-mode RET in the Coq buffer before restarting the Coq process).


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.

Coq Proof General has a special experimental feature called "Holes" which makes use of the abbreviation mechanism and includes a large list of command abbreviations. See section Holes feature, for details. With other provers, you may use the standard Emacs commands above to set up your own abbreviation tables.


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

This document was generated by Erik Martin-Dorel on June 2, 2019 using texi2html 1.82.