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 'hol98 "<holdir>/tools/hol-mode"
  "Runs a HOL98 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 hol98; 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 *)

I also recommend that you enable transient-mark-mode. This 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 once-off, by typing M-x transient-mark-mode (and typing the same again will turn it back off).

To select text, 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 should 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; use the up and down cursor keys to select lines at a time, C-a and C-e to move to the starts and ends of lines, and M-b and 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. Further, if you find yourself highlighting something and don't want to be in "highlight-mode", hit C-g. This stops 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 (``...'').

h ``hol98'': 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-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-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 epxressions.
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 quietdec 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.