README

"HOL mode" for Vim.

Send the visually selected region of a Vim buffer to a HOL interactive session.

Feedback to: Ramana Kumar <firstname.lastname@gmail.com>

== Dependencies ==

HOL4, PolyML, Vim, and a POSIXly correct tail.

Uses the Thread structure from PolyML, and Unix and Posix structures from the
standard basis. Could be ported to another ML providing similar functionality.

== Contents ==

All files are located under tools/vim

Filename       Description
----------     ------------------------------------------------------------------
vimhol.sml     The extra code loaded with the prelude for a Vimhol session.
hol.vim        Vim script to prepare a Vim buffer for sending to HOL.
*src           Used to generate the above during the HOL build process.
holabs.vim     Vim abbreviations for Unicode characters. (Optional.)
hol-config.sml Template hol-config file for automatically loading Vimhol when hol starts.
filetype.vim   Template filetype.vim for automatically running hol.vim when vim starts.
README         Documentation. (This file.)

== Quickstart ==

1. Add the contents of hol-config.sml to your ~/.hol-config.sml file
2. Add the contents of filetype.vim to your ~/.vim/filetype.vim
3. Run hol to start the HOL session
4. Run vim and open a HOL script
5. Select some SML value or declaration and type hs to send it to the HOL session
   See below for more key mappings

If you don't have filetype on in vim, then this won't work. In that case, you
should forget step 2 and source hol.vim manually in step 3. To turn filetype
on, you can add "filetype on" to your ~/.vimrc.

== WARNING ==

Use of HOL mode may cause your Vim to appear frozen and unresponsive. This
happens when the plugin is trying to write to a fifo that is not being read.
The remedy is to read the fifo: either start hol (if everything is set up
correctly) or simply cat $(HOLDIR)/tools/vim/fifo (or $(HOLDIR)/$(VIMHOL_FIFO)
if you are using a custom fifo path).

== Key mappings ==

(These are all set up at the bottom of hol.vim)

The following commands work in visual mode:

hs          Send region to HOL.
hu          Send region to HOL in quiet mode.

hL          Send region to be split into words and each word "load"ed.
hl          Same as above, but also send the region as a command afterwards.

hg          Send region (should be a quotation) to g, to start a new proof.
he          Send region (should be a tactic) to e, to expand a tactic.
hS          Send region (should be a quotation) as a new subgoal.
hF          Send region (should be a quotation) to be proved sufficient then proved.

If a visual mode command above is given in normal mode, the region will be the
line containing the cursor.

The following commands work in normal mode (only):

<count>hR   Rotate subgoals <count> times (default 1).
<count>hb   Back up proof <count> times (by calling b) (default 1).
<count>hd   Drop <count> proof attempts (by calling d) (default 1).
hp          Print the proof manager status (by calling p).
hr          Restart the current proof (by calling restart).
hv          Save the proof state (by calling save_proof).
<count>hB   Back up to the <count>th last save point (by calling Backup) (default 1).

hc          Interrupt execution (of whichever of the things sent is running).

ht          Select a quotation, including the ` delimiters.
            Find ` left of (or under) cursor and select to next `.
hT          Select a term: same as above, but with `` delimiters.

hh          A normal h (usually means move cursor left).
            This one works in both normal and visual modes.

hj          Toggle HOL's show types trace.
hn          Toggle HOL's Unicode trace.

=== Automatic stripping ===

hL and hl don't "load" these words: local open in end.

hg strips commas from the end of the region.

hS strips everything including and after the first "by" in the region, if any.
hF strips everything including and after the first "suffices_by" in the region, if any.

he strips these tokens from the ends of the region
  start: ) ] [
  end:   ( [
  both:  , THEN THENL THEN1 << >> ++ \\ by

== Leading string ==

Vimhol uses <LocalLeader> as the leading string for all commands.
We have assumed above that <LocalLeader> is set to "h".
You can change the key sequence used to signal the start of a Vimhol command by
setting the variable maplocalleader before loading hol.vim.
See filetype.vim for an example (by default, it is set there to "h").

== Unicode ==

An alternative to the abbreviations described below are built-in Vim digraphs.
See :help digraph. Briefly, type CTRL-K <char1><char2> to get a special
character. If you set the 'digraph' option, you can enter them with
<char1><BS><char2> too. Digraphs have the advantage of being acceptable in
normal mode for the 'f' (and related) commands.

The codes for common HOL Unicode characters are listed in holabs.vim as
comments. NOTIN (∉) doesn't seem to be built in to Vim, but you can add a
mapping with :digraph (+ 8173 (this is done in holabs.vim too).

Abbreviations:
- The holabs.vim file contains abbreviations from ASCII strings to Unicode strings.
- Examples: <> to ≠, and UNION to ∪. Generally, we use the ASCII name of the HOL constant.
- When you type the ASCII, you get the Unicode.
- To turn unicode on, source holabs.vim.
- You can source holabs.vim automatically by uncommenting the line copied from filetype.vim.
- Sometimes might need CTRL-] or ESC or space after an abbreviation to make it happen.
- To avoid an abbreviation at one point, type CTRL-V after it
- During an editing session, use :abc to stop all abbreviation key maps.
  (Removes non holabs.vim stuff too.)
- Undo abbreviations in selected text with :call HOLUnab() in visual mode.

== Multiple sessions via different fifos ==

As explained in the next section, communication between HOL and Vim is done via
a fifo that is by default located in $HOLDIR/tools/vim/fifo. If you run
multiple HOL sessions sharing the same fifo, then the session that receives
input from Vim (sending to that fifo) is unpredictable, and hence not
recommended.

However, a custom fifo path can be used by setting the environment variable
$VIMHOL_FIFO with an absolute path to a fifo (it will be created if it does not
exist). This environment variable instructs both HOL and Vim. Set $VIMHOL_FIFO
to one path when you start one pair of a HOL and a Vim session, and in another
environment set it to a different path, then you can run two instances of
Vimhol in parallel without interference.

== Architecture, and the Vimhol structure ==

Vim sends short commands to tools/vim/fifo (or $VIMHOL_FIFO) containing the names of temporary files.
Vim writes the real code to be run to those temporary files.
Vimhol "use"es and deletes the temporary files in the order that their names were received.

Vimhol runs four threads in total.
1. Main thread, which accepts input from stdIn and displays output in the terminal.
2. Tail thread, which is just tail following the end of tools/vim/fifo for commands from Vim.
3. Polling thread, which waits for and reads the output of the tail thread.
   The polling thread automatically starts the tail thread and the running thread when it needs to.
4. Running thread, which runs the code from Vim.
   The running thread is the one interrupted by Hc.

In the main thread, the Vimhol structure will be in scope, containing the following values.
They're probably not useful except for debugging.
Value                          Description
-----------------------------  ------------------------------------------
pActive      : unit -> bool    whether the polling thread is active
rActive      : unit -> bool    whether the running thread is active
stopTail     : unit -> unit    kill the tail thread
restartTail  : unit -> unit    restart the tail thread
stop         : unit -> unit    stop the polling and running threads
restart      : unit -> unit    restart the polling thread
keepFiles    : bool ref        don't delete temporary files (default: false)
quiet        : bool ref        don't print warn/info messages (default: false)
queue        : Vimhol.Queue.t  queue containing names of temporary files
removeQueue  : unit -> unit    delete all the files in the queue (respects keepFiles)
fifoPath     : string          the fifo path being used by this session

tools/vim/fifo (or $VIMHOL_FIFO) is generated by vimhol whenever it doesn't exist.
Temporary files are generated and should be automatically removed when keepFiles is false.