Emacs HOL mode

This page attempts to describe how to use the Emacs hol-mode that is distributed with HOL.

A note on key-combination notation

C-x is notation for “control-x”, which stands for hitting the x key at the same time as holding down the Control key. Similarly, M-h stands for “meta-h”, which means doing the same but with the meta key. On PC keyboards, the ALT key often stands in for a meta key. If this doesn’t work, you can get a meta effect by first hitting ESC and then the next key (h in this case). If you can get the proper, modifier-key meta working, it’s definitely worthwhile, as having to hit ESC all the time is tedious in the extreme.

Installing the emacs mode

Put

   (autoload 'hol "<holdir>/tools/hol-mode"
     "Runs a HOL session in a comint window.
   With a numeric prefix argument, runs it niced to that level
   or at level 10 with a bare prefix. " t)

into your .emacs file, where <holdir> is where you installed HOL. This approach has the disadvantage that you have to start HOL using M-x hol; you can't use the key sequence M-h h. If you want that, you can use

   (load "<holdir>/tools/hol-mode")

in the .emacs file.

Alternatively, if you just want to try it once, type

   M-x load-file

and type <holdir>/tools/hol-mode.el in response to the prompt.

Using the emacs mode

My usual way of starting is:

   C-x C-f fooScript.sml   (* find my file *)
   M-h h                   (* start my hol; it takes over the window *)
   C-x b fooScript.sml     (* go back to my script file *)
   C-x 5 b *HOL*           (* go to the HOL buffer in a separate window *)

If you are using an old Emacs (older than Emacs 23), I also recommend that you enable transient-mark-mode. (With newer versions of Emacs, this mode is on by default.) This mode makes it more obvious what you have selected. You can enable this for all sessions by putting (transient-mark-mode 1) in your .emacs file, or as a one-off, by typing M-x transient-mark-mode (and typing the same again will turn it back off).

To select text:

use the “standard” method: hold down the shift key while moving the cursor; or
use the old emacs method: move the cursor in your source buffer to one end or other of the text to be sent and hit C-SPC. This starts text selection. Then move the cursor to the other end of the text to be sent.

With transient-mark-mode on, you will see the text highlight. This is useful visual feedback that what you’re doing makes sense. Of course, you don’t need to just move one character at a time to select text; other movement commands work as well. For example:

use the up and down cursor keys to select lines at a time;
use Home (or C-a) and End (or C-e) to move to the starts and ends of lines, and
use C-Left (or M-b) and C-Right (or M-f) to move backwards and forwards over words.

Once you’re happy that you’ve highlighted the right bit of text, hit

M-h M-r: to send the region to be evaluated as is by the interpreter; or
M-h e: to send the region to be applied as a tactic, i.e., as if wrapped in e(...).

Both of these will analyse the text being sent to pre-emptively load modules that the text depends on. (This is an extremely useful feature, and saves you having to start every session by issuing load instructions to the interpreter.)

Aside: Two more things about text selection in emacs:

You can flip your cursor to be at the other end of the selected region by hitting C-x C-x. The end of the text where you were then becomes the anchor point for further selection.
If you find yourself highlighting something and don’t want to be in "highlight-mode", you can hit C-g. Also, if you are highlighting by holding down the shift key, then simply moving the cursor without also having the shift key down will stop highlighting.

Finally, if you find you don’t like the text-highlighting that you get with transient-mark-mode on, you can do all of the above without it, but you don’t get the highlighting and you need to be aware that the region between the cursor and where you last hit C-SPC is always available to be sent. (With transient-mark-mode on, but nothing highlighted, an attempt to do M-h M-r will just make Emacs beep and say “The mark is not active now”.) I find the absence of high-lighting off-putting myself, but this is the way Emacs used to be and I guess some people may still like it.

Sending a goal is even easier, because goals just about always appear between two backquote symbols. If you put your cursor in such a position (i.e. somewhere on a goal in your script file, but not on the backquote characters themselves), all you need to do is hit M-h g, and the text between the backquotes will be sent to be set up as a goal in the goalstack package.

These are the basic commands. See the section below for even more, and learn how to control the HOL session entirely from your original text buffer.

HOL mode commands

To issue one of these commands, type M-h followed by the given key-combination, or type M-x followed by the long name of the command, given between quotes (``...''). If a command mentions a dependency on a prefix argument, this can be supplied by hitting C-u, typing in a number, and then continuing with the rest of the commend.

h ``hol''

Starts the HOL session.

C-a ``hol-toggle-show-assums''

Toggles the value of the show_assums variable, affecting whether or not assumptions are printed as dots or full terms.

C-c ``hol-interrupt''

Interrupts the HOL session. Useful for those tactics that don’t always return.

C-f ``hol-toggle-goalstack-fvs''

Toggles the display of the goal’s free variables every time the goal is printed. This can be useful when a goal picks up multiple variables of different types.

C-l ``hol-recentre''

Recentres the screen that HOL is running in, so that the most text is visible with the bottom of the text at the bottom of the screen.

C-o ``hol-toggle-goalstack-print-goal-at-top''

When this flag is true (the default), the goal-stack manager prints goals with the goal first, a line of hyphens and then the assumptions. When the flag is false, the goal is at the bottom of the presentation, with assumptions above it.

C-v ``hol-scroll-up''

Scrolls the HOL window.

C-t ``hol-toggle-show-types''

Toggles the value of the show_types variable, affecting how terms are printed.

M-a ``hol-toggle-goalstack-num-assums''

With a prefix argument, sets the number of assumptions that should be printed with each goal. The default value is 10000. If the limit is n, and there are more than n assumptions, then the goal will be printed with its n most recent assumptions. Without a prefix argument, this will toggle from n ≠ 0 to n = 0, and from n = 0 to n = 1.

M-b ``backward-hol-tactic''

Moves the cursor back over the previous tactic in the source text in the current buffer. With a prefix argument, moves back that many tactics.

M-f ``forward-hol-tactic''

Moves the cursor forward over the next tactic in the source text in the current buffer. With a prefix argument, moves that many.

M-r ``send-region''

Sends the region to the HOL process, where it is evaluated at the top level. Can be used both to define new ML bindings, and to evaluate expressions. With a single C-u prefix argument wraps the thing being sent:

   (<region>) handle e => Raise e

This is useful when running with Moscow ML, where HOL_ERR exceptions don’t get their arguments printed out. With a “double” prefix argument (i.e., hit C-u twice before hitting M-h M-r), toggle “quietness” so that output associated with your region is not displayed in the *HOL* buffer.

M-s ``hol-subgoal-tactic''

Sends term at point (delimited by backquote characters) as a subgoal. Will usually create at least two sub-goals; one will be the term just sent, and the others will be the term sent STRIP_ASSUME’d onto the assumption list of the old goal. (Loads the Q module if not already loaded.)

M-v ``hol-scroll-down''

Scrolls the HOL window.

b ``hol-backup''

Backs up one stage in the goalstack.

d ``hol-drop-goal''

Drops the current goal, removing it from the goal-stack entirely.

D ``hol-drop-all-goals''

Drops all goals.

e ``expand-hol-tactic''

Sends the region to the HOL process as a tactic, where it is applied to the current goal.

g ``hol-goal''

Sets the current goal. Sends the term at point (delimited on both sides by back-quotes) to the HOL process. With a prefix argument, or if in transient mark mode with an active region, sends the selected region as the goal instead.

l ``hol-load-file''

Loads a HOL library. If there is a region marked, uses that string as the library to load. Otherwise, if the cursor (point) is over a likely name, it uses that for the library to load. As a last resort (or in all situations, if there is a prefix argument), prompts for the name of the library.

m ``hol-db-match''

Prompts for a term (don’t put it in quotes) that is then used as an argument to a call to DB.match []. Very useful for finding pertinent theorems.

n ``hol-name-top-theorem''

Prompts for a name to give to the ``top theorem'' (i.e., the theorem just proved in the goalstack). With a prefix argument also drops the goal.

o ``hol-open-string''

Opens HOL modules, prompting for the name of the module to load. With prefix ARG, toggles the “quiet declarations” variable before and after opening, potentially saving a great deal of time as tediously large modules are printed out. (That’s assuming that quietdec is false to start with.)

p ``hol-print''

Prints the top goal in the goalstack.

r ``hol-rotate''

Rotates goals in the goalstack. With a numeric prefix argument rotates that many out of the way, instead of just one.

R ``hol-restart''

Restarts the current proof.

s ``send-string-to-hol''

Prompts for a string to be evaluated by SML, like ``M-r''.

t ``mark-hol-tactic''

Marks the tactic at point, putting mark at the start of the tactic, and point at the end. Useful as a prelude to applying the tactic with ``expand-hol-tactic''.

u ``hol-use-file''

Prompts for a file-name to be use-d at the top level.