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
(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)
<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
Alternatively, if you just want to try it once, type
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
(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.
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.
- 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
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.
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
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
- 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
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
- 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
onto the assumption list of the old goal. (Loads the
Q module if not
- 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.